tr.bib

@TECHREPORT{abrahammumm.hannemann.steffen:verification,
  AUTHOR = {Erika {\'A}brah{\'a}m-Mumm and Ulrich Hannemann and
                  Martin Steffen},
  TITLE = {Verification of Hybrid Systems: Formalization and Proof
                  Rules in {PVS}},
  INSTITUTION = {Lehrstuhl f{\"ur} Software-Technologie,
                    Institut f{\"u}r Informatik und praktische Mathematik,
                    Christian-Albrechts-Universit{\"a}t Kiel},
  YEAR = 2001,
  TYPE = {Technical Report},
  NUMBER = {TR-ST-01-1},
  MONTH = JAN,
  URL = {http://www.informatik.uni-kiel.de/inf/deRoever/techreports/01/tr-st-01-1.ps.gz},
  ABSTRACT = {Combining discrete state-machines with continuous
                  behavior, hybrid systems are a well-established
                  mathematical model for discrete systems acting in a
                  continuous environment. As a priori \emph{infinite} state
                  systems, their computational properties are undecidable
                  in the general model and the main line of research
                  concentrates on model checking of finite abstractions of
                  restricted subclasses of the general model. In our work,
                  we use \emph{deductive methods}, falling back upon the
                  general-purpose theorem prover PVS. 
  
                  To do so we extend the classical approach for the
                  verification of state-based programs by developing an
                  inductive proof method to deal with the parallel
                  composition of hybrid systems. The methods cover shared
                  variable communication, label-synchronization, and
                  especially the common continuous activities in the
                  parallel composition of hybrid automata. Besides hybrid
                  systems and their parallel composition, we formalized
                  their operational step semantics and a number of
                  proof-rules within PVS, for one of which we give also a
                  rigorous completeness proof.  Moreover, the theory is
                  applied to the verification of a number of examples.}
}