Change and Delay Contracts for Hybrid System Component Verification

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

Publikation: Beitrag in Buch/Bericht/TagungsbandKonferenzbeitragBegutachtung

9 Zitate (Scopus)


In this paper, we present reasoning techniques for a component- based modeling and verification approach for hybrid systems comprising discrete dynamics as well as continuous dynamics, in which the components have local responsibilities. Our approach supports component contracts (i.e., input assumptions and output guarantees of interfaces) that are more general than previous component-based hybrid systems verification techniques in the following ways: We introduce change contracts, which characterize how current values exchanged between components along ports relate to previous values. We also introduce delay contracts, which describe the change relative to the time that has passed since the last value was exchanged. Together, these contracts can take into account what has changed between two components in a given amount of time since the last exchange of information. Most crucially, we prove that the safety of compatible components implies safety of the composite. The proof steps of the theorem are also implemented as a tactic in KeYmaera X, allowing automatic generation of a KeYmaera X proof for the composite system from proofs of the concrete components.

OriginalspracheEnglisch (Amerika)
TitelFundamental Approaches to Software Engineering - 20th International Conference, FASE 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings
Redakteure/-innenMarieke Huisman, Julia Rubin
Seiten134 - 151
PublikationsstatusVeröffentlicht - Apr. 2017


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


Untersuchen Sie die Forschungsthemen von „Change and Delay Contracts for Hybrid System Component Verification“. Zusammen bilden sie einen einzigartigen Fingerprint.