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 [email protected]