We investigate the feasibilty of computer-aided deductive verification of hybrid systems. Hybrid systems are modeled by phase transition systems, in which activities specify the bounds on the deriva tives 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.
展开▼
