In modern software and systems engineering formal verification gets more and more important to ensure the dependability of (critical) systems. The availability of increasingly powerful and interoperable computer-based modelling tools mean that digital, model-based representations of new designs tend to exist long before the first prototypes are manufactured – from CAD and CAE designs to functional (i.e. behaviour describing) models and information on component reliability and fault modes.
We work on seamlessly integrating formal verification tools and algorithms with MBSE workflows such that formal models and verification objectives are automatically extracted from previously created engineering data. In order to tackle the state space sizes of models on that level of detail and to integrate the MBSE-inherent modularity and reusability of model components, we work on modifying mainstream model checking algorithms to generate artifacts that can be reused to speed up future verification runs.
This topic is under ongoing research. For questions please contact Leon Wehmeier.