RT-proofs: Formale Beweise für Echtzeitsysteme

• Antragsteller: Björn Brandenburg, Ph.D.; Professor Dr.-Ing. Rolf Ernst
• Fachliche Zuordnung: Rechnerarchitektur, eingebettete und massiv parallele Systeme ; Sicherheit und Verlässlichkeit, Betriebs-, Kommunikations- und verteilte Systeme
• Förderung: Förderung von 2017 bis 2022
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 391919384

Echtzeitsysteme, d.h. Rechner, die strengsten Zeitanforderungen genügen müssen, finden sich in nahezu allen modernen sicherheitskritischen Technologien. Sie werden z.B. in der Fahrzeug- und Luftfahrtelektronik, Robotik und Automatisierungtechnik eingesetzt, wo fehlerhaftes Zeitverhalten schwere Unfälle verursachen kann. Um zu gewährleisten, dass kritische Systeme selbst im ungünstigsten Fall unter Maximallast noch rechtzeitig reagieren, sind gründliche Prüfverfahren notwendig. Derartige Prüfungen sind allerdings alles andere als einfach und nur mit anspruchsvollen statischen Analyseverfahren zu bewerkstelligen, da das Zeitverhalten von Software durch die geteilte Nutzung von Ressourcen und Kommunikationswegen komplex und nur schwer berechenbar ist. Leider sind die Grundlagen aktueller Analyseverfahren längst nicht so solide, wie das bei sicherheitskritischen Systemen erforderlich ist.Das Kernproblem ist, dass die aktuell eingesetzten Analysemethoden auf informellen, gelegentlich lückenhaften Beweisen beruhen, die nur schwer nachzuvollziehen sind. Dadurch entsteht ein beträchtliches Risiko, dass subtile, aber schwerwiegende Fehler über lange Zeit unentdeckt bleiben oder versehentlich durch das Kombinieren von Verfahren mit implizit inkompatiblen gemachten Annahmen entstehen. Das zeigt z.B. der Widerruf der Analyse des CAN Datenbusses, der in nahezu allen modernen Fahrzeugen verbaut ist: Erst 13 Jahre nach der Erstveröffentlichung wurde zufällig ein Fehler in der Analyse gefunden. Und dies ist längst kein Einzelfall. Ähnlich schwerwiegende Probleme und eine Vielzahl kleinerer Ungenauigkeiten finden sich zuhauf in der Fachliteratur. Und selbst wenn die eigentlichen Algorithmen fehlerfrei sind, stellt sich immer noch die Frage, ob kommerzielle Analysewerkzeuge sie auch tatsächlich korrekt implementieren. Kurz: das bisherige händische und informelle Vorgehen ist fehleranfällig und mit Hinblick auf sicherheitskritische Echtzeitsysteme schlicht unzureichend.Anzustreben ist stattdessen, Analyseverfahren und deren Ergebnisse formal zu formulieren, so dass Dritte den Nachweis ihrer Korrektheit maschinell nachvollziehen können. Um dies zu ermöglichen, zielt das RT-proofs Projekt darauf ab, die Grundlagen für die rechnerunterstützte Verifikation von Echtzeitanalysen zu schaffen. Dazu werden wir (i) die notwendigen grundlegenden Konzepte mit Hilfe des Coq Beweisassistenten formalisieren und (ii) die industriell wichtigsten Analyseverfahren, die auf der sogenannten "busy window" Methode basieren, maschinengestützt beweisen. Schlussendlich werden wir (iii) eine neue Art von Analysewerkzeug entwickeln, die das Risiko von Werkzeugfehlern kategorisch durch formales Zertifizieren der Ergebnisse, d.h. des "Rechenweges" aber nicht des Programms selbst, ausschließt. RT-proofs wird damit als Vorbild und Muster den Weg zu einer bisher unerreichten (aber benötigten!) Stringenz in der Analyse von kritischen Echtzeitsystemen bahnen.

• DFG-Verfahren: Sachbeihilfen
• Internationaler Bezug: Frankreich
• Kooperationspartnerinnen / Kooperationspartner: Professor Dr. Jean-François Monin; Sophie Quinton, Ph.D.; Dr. Pierre Roux