Modeling and verification of hybrid systems

A hybrid system models both discrete event and continuous dynamics. We present a modeling formalism, and a verification methodology for hybrid systems. The verification methodology is based on abstracting the continuous dynamics in the hybrid system by simpler continuous dynamics. We present two methods for doing this: 1) the differential inclusion is replaced with a simpler differential inclusion; and 2) we look at the timing information that is relevant to the verification problem, and construct an abstraction of the hybrid system with a timed automaton