MontiBelle - Toolbox for a Model-Based Development and Verification of Distributed Critical Systems for Compliance with Functional Safety
Hendrik Kausch, Mathias Pfeiffer, Deni Raco, Bernhard Rumpe⋆ · AIAA Scitech 2020 Forum · 2020
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.