Computer Science Department
School of Computer Science, Carnegie Mellon University


A Component-based Approach to
Hybrid Systems Safety Verification

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

June 2016


Also appears as JKU-CIS-2016-01**

A conference version of this report appeared in the
Proceedings of the 12th International Conference on integrated Formal Methods (iFM)
Erika Abraham, Marieke Huisman, Editors,
Reykjavik, Island, LNCS. Springer 2016.

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

We study a component-based approach to simplify the challenges of verifying large-scale hybrid systems. Component-based modeling can be used to split large models into partial models to reduce modeling complexity. Yet, verification results also need to transfer from components to composites. In this paper, we propose a component-based hybrid system verification approach that combines the advantages of component-based modeling (e. g., reduced model complexity) with the advantages of formal verification (e. g., guaranteed contract compliance). Our strategy is to decompose the system into components, verify their local safety individually and compose them to form an overall system that provably satisfies a global contract, without proving the whole system. We introduce the necessary formalism to define the structure and behavior of components and a technique how to compose components such that safety properties provably emerge from component safety.

17 pages

*Computer Science Department, Carnegie Mellon University
**Department of Cooperative Information Systems, Johannes Kepler University, Linz, Austria

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by