CSR: Small: From Simulations to Proofs for Cyberphysical Systems

点击翻译按钮获取中文摘要

The widespread presence of embedded controllers in vehicles, medical devices, and water, power, and gas supply systems, makes the problem of ensuring their reliability critically important. The two most popular methods of achieving this in the context of cyberphysical systems, namely simulation and verification, suffer from serious drawbacks. Simulation, while being scalable and efficient, is incomplete. Verification, on the other hand, is computationally difficult and does not scale to large systems. This project explores a third approach where system-level correctness guarantees are derived from algorithmic analysis of finitely many, carefully chosen simulations or tests. The techniques developed in this project could enable more reliable and safe Cyber Physical Systems which are critically important class of systems. This project will develop algorithms for finding the relationship between executions that start within close proximity of some initial state, techniques for verifying temporal properties involving non-linear propositions, and develop the foundations for compositional simulation-based verification. These ideas will be embodied in a software tool which will drastically reduce the effort required to verify cyberphysical models created using the Simulink/Stateflow environment. In addition to these research goals, the PIs plan on teaching a class on verifying hybrid systems that will introduce undergraduates and graduate students in engineering to the use of formal methods in embedded system design. The scientific ideas discovered, the tools built and the repository created will all be publicly disseminated.