Verifying cyber-physical systems by combining software model checking with hybrid systems reachability
Stanley Bak, Sagar Chaki · 2016
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.