Motivation
Eingebettete Systeme sind das technologische Rückgrat der digitalisierten Welt. Dabei übernehmen sie auch Aufgaben in besonders sicherheitskritischen Anwendungen, wie moderne Flugsteuerungscomputer oder die Brems- und Lenksteuerung in Kraftfahrzeugen. In vielen dieser Anwendungen stellt die funktionale Sicherheit eine zentrale Herausforderung dar und legt nicht selten den „ökonomischen Betriebspunkt“ technischer Innovationen fest. Dies betrifft nicht nur die Luftfahrt und Automobilindustrie, sondern auch andere Industriefelder wie die Produktionstechnik (Industrie 4.0) oder die Gebäudetechnik (z.B. Lüftungs- und Brandschutztechnik). Moderne Halbleitertechnologien ermöglichen eine immer höhere Leistung, sind jedoch aufgrund ihrer immer geringeren Strukturgrößen zunehmend anfällig für Hardwarefehler, insbesondere zufällige Fehler, die sich meist durch ungewollte Änderungen (Bitflips) in Speicherzellen und Registern äußern. Sicherheitsstandards betonen eine durchgehende Methodik, bei der vor allem wohldefinierte Sicherheitsfunktionen des Systems durch Entwurfs- und Entwicklungsschritte auf allen Ebenen gewährleistet werden. Entscheidend sind formale Verifikationstechniken, die mit der Gewissheit eines mathematischen Beweises tatsächliche Garantien über ausgewählte Eigenschaften eines Systems geben.
Ziele und Vorgehen
Das Ziel von PROFORMA ist es, die Auswirkungen von Fehlern von der Hardware bis hin zur Anwendungssoftware vollautomatisch auf mathematisch korrekte Weise zu modellieren, um daraus Sicherheitsgarantien ableiten zu können. Bislang sind keine industriellen Werkzeuge verfügbar, die die Mächtigkeit der Analyse formaler Techniken von systematischen Fehlern auch auf zufällige Fehler ausdehnen und dadurch die Wechselwirkung fehlerhafter Hardware mit der Software berücksichtigen. Die Analyse von Hardwarefehlern hinsichtlich ihrer Auswirkungen auf die Software ist bislang Simulationstechniken vorbehalten, die für bestimmte Anwendungsszenarien meist unsichere statistische Daten sammeln, sodass gravierende Sicherheitsrisiken unerkannt bleiben können. Das Projekt hingegen kann den formalen Beweis erbringen, dass unter allen modellierten Fehlern eine zu gewährleistende Sicherheitsfunktion stets ihre definierte Aufgabe erfüllt. Dieser Ansatz verspricht in der industriellen Anwendung eine qualitative Verbesserung der Sicherheitsanalysen gegenüber dem aktuellen Stand der Technik und reduziert durch die Automatisierung gleichzeitig die Kosten.
Innovationen und Perspektiven
Bereits in der Vergangenheit haben die Projektpartner eine Vorreiterrolle bei der Erforschung, Entwicklung und industriellen Einführung formaler Verifikationstechniken gespielt. In diesem Projekt bündeln sie ihre Kompetenzen in den Bereichen Hardware-/Software-Schnittstelle (Technische Universität Kaiserslautern), Software-Analyse (AbsInt Angewandte Informatik GmbH) sowie Modellprüfung und Tests (Verified Systems International GmbH).