C2E2 Verification Tool

Abstract:

Combining simulations with formal analysis can improve the design, verification, and validation processes for embedded and cyberphysical systems. In this poster presentation, I will present an overview of the algorithms we have developed to derive bounded-time formal guarantees from numerical simulations and static analysis of models. These algorithms are targeted for hybrid models of distributed and cyberphysical systems and they require either implicit or explicit annotations. They are always sound and also complete for robust safety and temporal precedence properties. For large networked models, the annotations can be derived compositionally. I will mention the lessons learned and the outstanding challenges in applying them to verify a parallel landing protocol and a cardiac cell-pacemaker network.