Deductive Verification Of Hybrid Control Systems Modeled In Simulink With Keymaera X
FORMAL METHODS AND SOFTWARE ENGINEERING, ICFEM 2018(2018)
摘要
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 timecontinuous 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 multiobject distance warner.
更多查看译文
关键词
Hybrid systems, Formal verification, Model-driven development
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络