2018/06/20 by Nima Roohi, Ramneet Kaur, Roohi, Nima +7
Computer Science · Engineering · #FOS: Computer and information sciences #FOS: Electrical engineering #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Model-Driven Software Engineering Techniques #Robotics (cs.RO) #Safety Systems Engineering in Autonomy #Systems and Control (eess.SY) #electronic engineering #information engineering
paper · pdf · doi:10.48550/arxiv.1806.08810
openalex publication_date 2018/06/20 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Industrial cyber-physical systems are hybrid systems with strict safety requirements. Despite not having a formal semantics, most of these systems are modeled using Stateflow/Simulink for mainly two reasons: (1) it is easier to model, test, and simulate using these tools, and (2) dynamics of these systems are not supported by most other tools. Furthermore, with the ever growing complexity of cyber-physical systems, grows the gap between what can be modeled using an automatic formal verification tool and models of industrial cyber-physical systems. In this paper, we present a simple formal model for self-deriving cars. While after some simplification, safety of this system has already been proven manually, to the best of our knowledge, no automatic formal verification tool supports its dynamics. We hope this serves as a challenge problem for formal verification tools targeting industrial applications.