Hybrid system verification using discrete model approximations.

摘要

This dissertation presents a computational technique for verifying properties of hybrid systems with continuous dynamics described by ordinary differential equations. The approach is based on the computation of finite-state conservative approximations, called quotient transition systems, of the infinite-state transition system representing the semantics of the hybrid system. For universal specifications, positive verification for a quotient transition system implies the same result for the hybrid system. The fundamental computation in the generation of quotient transition systems is the mapping of sets of continuous states to the boundaries of the convex polyhedral switching surfaces. This mapping is computed by intersecting the sets of reachable states for continuous systems, called flow pipes, with the switching boundaries. Flow pipes are approximated by sequences of overlapping convex polyhedra. The dissertation describes the software verification tool created in MATLAB® based on the above computational technique and presents its applications to some example hybrid systems.