@TECHREPORT{R-95-30,
PSURL = {/publications/cgi-bin/tr-fetch.pl?r-95-30+ps},
NUMBER = {R-95-30},
INSTITUTION = ida,
ADDRESS = idaaddr,
YEAR = {1995},
AUTHOR = {Nadjm-Tehrani, Simin},
TITLE = {A Study of Decompositional Verification of Hybrid Systems},
ABSTRACTURL = {/publications/cgi-bin/tr-fetch.pl?r-95-30+abstr},
ABSTRACT = {This paper is a study of decompositional proof techniques applied to the verification of a model of a real world hybrid system, an aircraft landing gear. We present a formal description of these techniques (taken from Halwbachs et.al. [5]) and look at two ways of applying them. We discover, and correct, a flaw in the theory, but conclude ultimately that when dealing with a plant-controller combination there is often little to be gained by adopting a decompositional approach to verification. Moreover we argue that in these cases the composed system can be even simpler than its components, and thus it is most expedient to prove properties of the system directly.}