Computer Science Department
School of Computer Science, Carnegie Mellon University


Change and Delay Contracts
for Hybrid System Component Verification

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

February 2017


Also appears as
Department of Compperative Information Systems, Johannes Kepler University
Technical Report JKU-CIS-2017-01

A conference version of this report appeared at FASE 2017.
Change and Delay Contracts for Hybrid System Component Verification.
20th International Conference on Fundamental Approaches to Software Engineering,
FASE, Uppsala, Sweden, Proceedings, LNCS. Springer, 2017.

Keywords: Component-based development, hybrid systems, formal verification

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 the magnitude of change to describe how current values exchanged between components along ports relate to previous values. We also introduce delay contracts, which characterize the rate of change to describe how change is related to the duration between value exchanges. 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 composed system. 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.

37 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by