The vast majority of commercial embedded systems are designed with simulation-based tools such as MathWork's Simulink and Stateflow. While simulations are computationally efficient, they are not complete---they cannot be naively used to design systems with provable guarantees. This project aims to build tools and techniques to verify such models. To this end, the project overcomes two key technical hurdles. First, it has been well known that Simulink-Stateflow (SLSF) models do not have any well-defined meaning. The mathematical description of a building block can be different from the simulated behavior that is generated numerically. This problem is addressed by defining semantics of SLSF models in terms of (possibly probabilistic) hybrid automata. Secondly, the class of Simulink models (translated to hybrid automata) that can be verified automatically by currently available techniques is rather restrictive. This second problem is addressed in this project by abstracting SLSF models into hybrid automata with simple dynamics, model checking the abstract models, and then refining the abstractions based on counterexamples generated by the model checker. Such a counterexample guided abstraction refinement framework provides semi-decision procedures to automatically analyze Simulink-Stateflow models. The developed software tools developed in this project translate SLSF models into probabilistic hybrid automata, analyze the formal automata model by abstracting, model checking, and refining, and then translate valid counterexamples back into Simulink to provide the user diagnostic information. Furthermore, the project builds a repository of benchmark SLSF models and their corresponding hybrid automaton models, based on examples from existing hybrid systems literature and drawing on industrial applications. The repository will be publicly disseminated and will be used to evaluate our tool.
A new course will be developed on the verification of hybrid systems that introduces undergraduate and graduate students in engineering at Illinois to the use of formal methods in embedded system design. Successful completion of the research tasks outlined here is likely to more broadly influence the design and verification of probabilistic hybrid systems that arise in application domains such as autonomous vehicles and mixed analog-digital circuits.
