Auto-SAFE: Development of a modular verification tool for the integration of automated safety analyses into the design process of software-intensive systems
Project Members: Tim Gonschorek, Ludwig Bedau
Project Time: Februar 2021 - April 2022
Funded By: MW/ IB Sachsen-Anhalt, Europäische Union (EFRE)
Goal of the Auto-SAFE project is to foster the transfer of scientific verification algoirhtms for model-based, safety-critical, software-intensive systems into an industrial context. Therefore, the project scope is to define a semantically sound transformation from one to two different, in industrial scenarios broadly used, modeling languages (e.g. Matlab Simulink) into the input language domain of state-of-the-art model verification tools and provide safety-relevant analysis algorithms. In general, this will enable system designers to already validate their system design against roboustness and safety targets during the modeling rather than in a far later step of the system development.
Project Description:
Clever software, sophisticated algorithms and artificial intelligence allow a multitude of new application potentials - often specifically for (safety) critical applications. For example, energy can be distributed more efficiently in the grid, modern vehicles can be made safer and, if necessary, collisions can be avoided autonomously. The basis for this is always increasingly complex control software.
Especially for safety-critical systems, where the focus in this context is on avoiding harm to people and the environment, the necessary safety analysis represents an ever greater challenge. In order to be able to guarantee this, the system developer must consider the system holistically in its entire complexity. This concerns not only the actual software components, but in particular the system to be controlled as well as the system environment and its behaviour. This is becoming increasingly difficult or even impossible for the aforementioned software-intensive, safety-critical systems. This is due, among other things, to the fact that software and system descriptions are designed on different with different execution semantics. Therefore, they are currently only analysed in an integrated manner at a high abstraction level. During further development, however, deviations can arise that violate previously verified safety goals.
In science, there are already techniques and approaches to verify the combination of software and(!) system behaviour with regard to safety-relevant properties in the further course of the design. However, these are only applicable in practice to a limited extent. The background is that modelling formalisms and languages used in practice cannot be combined with the mostly academic verification tools. For this, an algorithm would have to be defined and implemented that is compatible with the modelling formalisms used in practice.In this project, the partners want to create precisely such a prototype together. For this purpose, we select one or two modelling languages that are widely used in practice and transfer known algorithms from the field of formal verification in such a way that they can also be applied to these modelling languages used in practice. The result is a prototypical system that is able to automatically analyse software-intensive systems - as described above - and thus provide the central arguments for a security proof or uncover corresponding weaknesses in the system design. This can drastically shorten the development time of such systems and increase their functional safety.
Project Partner: METOP GmbH
Funded by the European Union (ERDF, dt. EFRE)
