Abstract
The interaction of software with a physical environment can cause complex, mixed continuous-discrete behavior, also referred to as being hybrid. Formal verification can guarantee the conformance of the system with a specification on a design level. However, the computational cost limits its applicability to relatively simple systems. To enable the verification of larger hybrid systems, we extend two fundamental approaches from the discrete to the hybrid domain: abstraction and compositional reasoning. In an abstraction of a system, details of the behavior are neglected to decrease its complexity. To formally show abstraction we construct a simulation relation between the states of the models. A state simulates another if the same, or more, behavior is possible. A compositional analysis examines parts of the system in such a way that properties of the entire systems can be deduced, and simulation relations are well suited for this task. We extend the classic discrete simulation framework with an enhanced concept of simulation and additional proof rules for compositional reasoning. We show that this framework applies directly to hybrid systems that do not share variables by using well-known labeled transition system semantics. To deal with hybrid systems that share variables we propose a modified semantics that allows us to show compositionality for two fundamental classes of hybrid systems: those with unrestricted inputs, and hybrid automata with piecewise constant bounds on the derivatives and with convex linear constraints. Since any hybrid system can be approximated arbitrarily close with a decidable subset of the latter class, these results enable the algorithmic compositional verification of hybrid systems. Algorithms for checking simulation, compositional reasoning, and reachability analysis were implemented in a formally sound verification tool called PHAVer. It uses exact arithmetic and complexity management, and for some benchmarks outperforms even non-conservative, approximative, reachability tools.
