TY - GEN
T1 - A Component-Based Hybrid Systems Verification and Implementation Tool in KeYmaera X (Tool Demonstration)
AU - Müller, Andreas
AU - Mitsch, Stefan
AU - Schwinger, Wieland
AU - Platzer, André
N1 - Publisher Copyright:
© Springer Nature Switzerland AG 2019.
PY - 2019
Y1 - 2019
N2 - Safety-critical cyber-physical systems (CPS) should be analyzed using formal verification techniques in order to gain insight into and obtain rigorous safety guarantees about their behavior. For practical purposes, methods are needed to split modeling and verification effort into manageable pieces and link formal artifacts and techniques with implementation. In this paper we present a tool chain that supports component-based modeling and verification of CPS, generation of monitors, and systematic (but unverified) translation of models and monitors into executable code. A running example demonstrates how to model a system in a component-based fashion in differential dynamic logic (dL), how to represent and structure these models in the syntax of the hybrid systems theorem prover KeYmaera X (which implements dL), and how to prove properties in KeYmaera X. The verified components are the source for translation into executable C code, which can be run on controlled components (e.g., a robot). Additionally, we demonstrate how to generate monitors that validate the behavior of uncontrolled components (e.g., validate the assumptions made about obstacles).
AB - Safety-critical cyber-physical systems (CPS) should be analyzed using formal verification techniques in order to gain insight into and obtain rigorous safety guarantees about their behavior. For practical purposes, methods are needed to split modeling and verification effort into manageable pieces and link formal artifacts and techniques with implementation. In this paper we present a tool chain that supports component-based modeling and verification of CPS, generation of monitors, and systematic (but unverified) translation of models and monitors into executable code. A running example demonstrates how to model a system in a component-based fashion in differential dynamic logic (dL), how to represent and structure these models in the syntax of the hybrid systems theorem prover KeYmaera X (which implements dL), and how to prove properties in KeYmaera X. The verified components are the source for translation into executable C code, which can be run on controlled components (e.g., a robot). Additionally, we demonstrate how to generate monitors that validate the behavior of uncontrolled components (e.g., validate the assumptions made about obstacles).
UR - http://www.scopus.com/inward/record.url?scp=85069197392&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-23703-5_5
DO - 10.1007/978-3-030-23703-5_5
M3 - Konferenzbeitrag
SN - 9783030237028
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 91
EP - 110
BT - Cyber Physical Systems. Model-Based Design - 8th International Workshop, CyPhy 2018, and 14th International Workshop, WESE 2018, Revised Selected Papers
A2 - Chamberlain, Roger
A2 - Taha, Walid
A2 - Törngren, Martin
PB - Springer
T2 - 8th International Workshop on Model-Based Design of Cyber Physical Systems
Y2 - 4 October 2019 through 5 October 2019
ER -