Verifying cyber-physical systems by combining software model checking with hybrid systems reachability.

Cyber-physical systems (CPS) span the communication, computation and control domains. Creating a single, complete, and detailed model of a CPS is not only difficult, but, in terms of verification, probably not useful; current verification algorithms are likely intractable for such all-encompassing models. However, specific CPS domains have specialized formal reasoning methods that can successfully analyze certain aspects of the integrated system. To prove overall system correctness, however, care must be taken to ensure the interfaces of the proofs are consistent and leave no gaps, which can be difficult since they may use different model types and describe different aspects of the CPS. This work proposes a bridge between two important verification methods, software model checking and hybrid systems reachability. A contract automaton (CA) expresses both (1) the restrictions on the interactions between the application and the controller, and (2) the desired system invariants. A sound assume-guarantee style compositional proof rule decomposes the verification into two parts - one verifies the application against the CA using software model checking, and another verifies the controller against the CA using hybrid systems reachability analysis. In this way, the proposed method avoids state-space explosion due to the composition of discrete (application) and continuous (controller) behavior, and can leverage verification tools specialized for each domain. The power of the approach is demonstrated by verifying collision avoidance using models of a distributed group of communicating quadcopters, where the provided models are software code and continuous 2-d quadcopter dynamics.