Go to page
 

Bibliographic Metadata

Title
Tactical contract composition for hybrid system component verification
AuthorMüller, Andreas ; Mitsch, Stefan ; Retschitzegger, Werner ; Schwinger, Wieland ; Platzer, André
Published in
Tactical contract composition for hybrid system component verification, 2018, Vol. 20, Issue 6, page 615-643
PublishedSpringer Berlin Heidelberg, 2018
LanguageEnglish
Document typeJournal Article
Keywords (EN)Component-based development / Hybrid systems / Component-based verification
ISSN1433-2787
URNurn:nbn:at:at-ubl:3-1873 Persistent Identifier (URN)
DOI10.1007/s10009-018-0502-9 
Restriction-Information
 The work is publicly available
Files
Tactical contract composition for hybrid system component verification [2.49 mb]
Links
Reference
Classification
Abstract (English)

We present an approach for hybrid systems that combines the advantages of component-based modeling (e.g., reduced model complexity) with the advantages of formal verification (e.g., guaranteed contract compliance). Component-based modeling can be used to split large models into multiple component models with local responsibilities to reduce modeling complexity. Yet, this only helps the analysis if verification proceeds one component at a time. In order to benefit from the decomposition of a system into components for both modeling and verification purposes, we prove that the safety of compatible components implies safety of the composed system. We implement our composition theorem as a tactic in the KeYmaera X theorem prover, allowing automatic generation of a KeYmaera X proof for the composite system from proofs for the components without soundness-critical changes to KeYmaera X. Our approach supports component contracts (i.e., input assumptions and output guarantees for each component) that characterize the magnitude and rate of change of values exchanged between components. These contracts can take into account what has changed between two components in a given amount of time since the last exchange of information.

Stats
The PDF-Document has been downloaded 4 times.
License
CC-BY-License (4.0)Creative Commons Attribution 4.0 International License