Formal verification of Safety-critical Cyber-Physical Systems modeled in an engineer-friendly notation (SCHU3174/3-1 BA 6655/1-1)

The goal of this project is to bridge the gap between engineering tools for Cyber Physical Systems (CPS) and verification tools, which have their roots in pure software verification. The project aim is to investigate how classical Hybrid Automaton (HA) can be extended, such that first engineers can easily map their Matlab/Simulink models of CPS to this notation and second to work out an approach whether user interaction for finding a proof can be based on this notation (instead of providing the system with the right next calculus rule including correct parameter assignments to be applied on the current proof goal). A second goal is to provide numerous non-trivial case studies to show how big/little the effort for fully verification of CPSs from industry actually is, when modern verification technologies are used.

Further further information in German (English will still be added asap):

In sicherheitskritischen Systemen steigt aufgrund des zunehmenden Automatisierungsgrad der Softwareanteil. Dabei werden die mechanischen Rückfallebenen mehr und mehr durch virtuelle, mittels Software realisierte Redundanzen ersetzt. Umso wichtiger ist es, dass die Korrektheit unter Berücksichtigung des Zusammenspiels mit der Umwelt in Form von motorischen (wie das Einprägen von Kräften, Momenten und Spannungen) und sensorischen Fähigkeiten (wie die Messung von Drehzahlen, Strömen und Temperaturen) und den algorithmisch gestützten Entscheidungen in der Software objektiv nachweisbar ist.

Systeme bei denen die Trennung von klassischen Computersystemen und der Umwelt durch deren Einbettung mittels sensorischer und motorischer Fähigkeiten zunehmend aufgehoben wird, werden cyber-physische Systeme genannt. Die damit verbundene Komplexitätssteigerung erfordert eine Neubewertung und Neuentwicklung von bisherigen Methoden, Arbeitsweisen und Technologien.

In den letzten Jahren sind formale Verifikations- und Analysemethoden für Software in eingebetteten Computersystemen entwickelt worden. Übliche Softwarefehler wie Nulldivisionen, arithmetisches Überlaufen, Null-Zeiger oder unerreichbarer Code können automatisch mit diesen Methoden ermittelt werden. Allerdings muss, um eine vollständige Korrektheit durchführen zu können, bei cyber-physischen Systemen auch domänenspezifisches Wissen über den physikalischen Prozess, mit denen die Computersysteme über die motorischen und sensorischen Einheiten verkoppelt sind, in die Analyse einfließen.

Ziel des Projektes ist das Schließen der Lücke zwischen den Verfahren und Ingenieurwerkzeugen, die zur Simulation und Validierung von cyber-physischen Systemen (CPS) eingesetzt werden und den Werkzeugen und mathematischen Methoden, die bei der reinen Softwareverifikation zum Einsatz kommen. Basierend auf der Erweiterung klassischer hybrider Automaten sollen Ingenieur_innen befähigt werden, deren domänenspezifische Simulationsmodelle in eine mathematische Formulierung zu übertragen, die es ermöglicht, dass ein vollständiger Nachweis der Korrektheit auch von einem Nichtfachmann durchgeführt werden kann.

Das DFG Projekt wird in Kooperation mit russischen Partnern der Universitäten "Polzunov Altai State Technical University", Barnaul und "Kazan Federal University", Kazan sowie dem außeruniversitären Forschungsinstitut "Institute of Automation and Electrometry of the Siberian Branch of the Russian Academy of Sciences", Novosibirsk, durchgeführt.

In der HTW ist das Projekt integriert in die Research School vom Fachbereich 1, die am 1. Oktober 2018 u.a. mit den wissenschaftlichen Schwerpunkten "Safety Systems Engineering" und "Regenerative Energiesysteme" die Arbeit aufnehmen wird.

Projektlaufzeit

1.7.2018 - 30.6.2019

Projektleitung

Kooperationspartner

  • Institute of Automation and Electrometry of the Siberian Branch of the Russian Academy of Sciences, Novosibirsk, Russia

Mittelgeber

Deutsche Forschungsgemeinschaft (DFG)

Förderprogramme

Aufbau internationaler Forschungskooperationen