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 war 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.

• Prof. Dr. Thomas Baar (Projektleitung)
• Prof. Dr.-Ing. Horst Schulte (Projektleitung)

Deutsche Forschungsgemeinschaft (DFG)

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

Aufbau internationaler Forschungskooperationen