We investigate the feasibility of computer-aided deductive verification of hybrid systems. Hybrid systems are modeled by phase transition systems, in which activities specify the bounds on the derivatives of the continuous variables. We present a method for invariant generation based on static analysis of the phase transition system. The invariants produced can be used as auxiliary properties in the verification of temporal properties. We show that in some cases the invariants thus produced suffice to prove the main safety property.
In Hybrid Systems: Computation and Control, Lecture Notes in Computer Science 1386, Springer-Verlag, 1998.
Postscript, PDF. © 1998, Springer Verlag.