Change and Delay Contracts for Hybrid System Component Verification

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

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

9 Citations (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.

Original languageEnglish (American)
Title of host publicationFundamental 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
EditorsMarieke Huisman, Julia Rubin
Pages134 - 151
Number of pages18
Publication statusPublished - Apr 2017

Publication series

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


  • Component-based development
  • Formal verification
  • Hybrid systems


Dive into the research topics of 'Change and Delay Contracts for Hybrid System Component Verification'. Together they form a unique fingerprint.

Cite this