Deductive Verification of Hybrid Control Systems Modeled in Simulink with KeYmaera X

摘要

Hybrid control systems are, due to their ever-increasing complexity, more and more developed in model-driven design languages like Simulink. At the same time, they are often used in safety-critical applications like automotive or medical systems. Ensuring the correctness of Simulink models is challenging, as their semantics is only informally defined. There exist some approaches to formalize the Simulink semantics, however, most of them are restricted to a discrete subset. To overcome this problem, we present an approach to map the informally defined execution semantics of hybrid Simulink models into the formally well-defined semantics of differential dynamic logic (dL). In doing so, we provide a formal foundation for Simulink, and we enable deductive formal verification of hybrid Simulink models with an interactive theorem prover for hybrid systems, namely KeYmaera X. Our approach supports a large subset of Simulink, including time-discrete and time-continuous blocks, and generates compact and comprehensible dL models fully-automatically. We show the applicability of our approach with a temperature control system and an industrial case study of a multi-object distance warner.