MontiBelle - Toolbox for a Model-Based Development and Verification of Distributed Critical Systems for Compliance with Functional Safety

AIAA SciTech Forum

Abstract

The methodology MontiBelle represents a specification formalism designed for the development and verification of cyber-physical safety-critical systems. It allows abstraction and underspecification and provides an extensive set of verification techniques to actually prove specification correctness. An architecture description language for modeling Cyber-Physical Systems is provided and combined with behavioral specifications as well as an environment to formulate desired properties. ADL Models and specifications are translated into an equivalent specification in the theorem prover Isabelle. Counterexamples can also be found by using a simulation execution within the Isabelle prover and letting the counterexample-finder run in an intelligent way through execution paths which are considered erroneous candidates. The most important property making this methodology stand out among alternate approaches is that refinement is fully compositional. The approach is evaluated on a synchronous flight guidance system.

Authors 4

1. Hendrik Kausch Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University

2. Mathias Pfeiffer Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University

3. Deni Raco Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University

4. Bernhard Rumpe⋆ Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University