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

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

Research output: Chapter in Book/Report/Conference proceedingsConference contributionpeer-review

2 Citations (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).

Original languageEnglish (American)
Title of host publicationCyber Physical Systems. Model-Based Design - 8th International Workshop, CyPhy 2018, and 14th International Workshop, WESE 2018, Revised Selected Papers
EditorsRoger Chamberlain, Walid Taha, Martin Törngren
PublisherSpringer
Pages91-110
Number of pages20
ISBN (Print)9783030237028
DOIs
Publication statusPublished - 2019
Externally publishedYes
Event8th International Workshop on Model-Based Design of Cyber Physical Systems - Turin, Italy
Duration: 4 Oct 20195 Oct 2019

Publication series

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

Conference

Conference8th International Workshop on Model-Based Design of Cyber Physical Systems
Abbreviated titleCyPhy2018
Country/TerritoryItaly
CityTurin
Period04.10.201905.10.2019

Fingerprint

Dive into the research topics of 'A Component-Based Hybrid Systems Verification and Implementation Tool in KeYmaera X (Tool Demonstration)'. Together they form a unique fingerprint.

Cite this