A Component-Based Hybrid Systems Verification and Implementation Tool in KeYmaera X (Tool Demonstration)

Andreas Müller, Stefan Mitsch, Wieland Schwinger, André Platzer

Publikation: Beitrag in Buch/Bericht/TagungsbandKonferenzbeitragBegutachtung

1 Zitat (Scopus)

Abstract

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).

OriginalspracheEnglisch (Amerika)
TitelCyber Physical Systems. Model-Based Design - 8th International Workshop, CyPhy 2018, and 14th International Workshop, WESE 2018, Revised Selected Papers
Redakteure/-innenRoger Chamberlain, Walid Taha, Martin Törngren
Herausgeber (Verlag)Springer
Seiten91-110
Seitenumfang20
ISBN (Print)9783030237028
DOIs
PublikationsstatusVeröffentlicht - 2019
Extern publiziertJa
Veranstaltung8th International Workshop on Model-Based Design of Cyber Physical Systems - Turin, Italien
Dauer: 4 Okt. 20195 Okt. 2019

Publikationsreihe

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Band11615 LNCS
ISSN (Print)0302-9743
ISSN (elektronisch)1611-3349

Konferenz

Konferenz8th International Workshop on Model-Based Design of Cyber Physical Systems
KurztitelCyPhy2018
Land/GebietItalien
OrtTurin
Zeitraum04.10.201905.10.2019

Fingerprint

Untersuchen Sie die Forschungsthemen von „A Component-Based Hybrid Systems Verification and Implementation Tool in KeYmaera X (Tool Demonstration)“. Zusammen bilden sie einen einzigartigen Fingerprint.

Zitieren