Eingebettete Systeme sind das technologische Rückgrat der digitalisierten Welt. Zunehmend übernehmen sie dabei auch Aufgaben in sicherheitskritischen Anwendungen, wie Flugsteuerungscomputern oder Brems- und Lenksteuerungen in Fahrzeugen.
In vielen dieser Anwendungen stellt funktionale Sicherheit eine zentrale Herausforderung dar und legt nicht selten den „ökonomischen Betriebspunkt“ technischer Innovationen fest. Dies betrifft neben der Luftfahrt und der Automobilindustrie viele andere Felder, etwa die Produktions-, Lüftungs- und Brandschutztechnik.
Moderne Halbleitertechnologien ermöglichen hierbei eine immer höhere Leistung. Die immer kleiner werdenden Strukturen sorgen aber auch für immer mehr Hardwarefehler — insbesondere zufällige Fehler, die sich meist durch Bitflips in Speicherzellen und Registern äußern.
Sicherheitsstandards für die Luftfahrt (DO-178B/C) und die Automotive (ISO 26262) betonen eine durchgehende Methodik für die Gewährleistung wohldefinierter Sicherheitsfunktionen des Systems, durch Entwurfs- und Entwicklungsschritte auf allen Ebenen. Formale Verifikation spielt dabei eine wichtige Rolle. Mit der Gewißheit eines mathematischen Beweises können tatsächliche Garantien über ausgewählte Eigenschaften eines Systems gegeben werden.
Bislang sind aber keine industriellen Werkzeuge verfügbar, um die Mächtigkeit der formalen Verifikation von systematischen Fehlern auch auf zufällige Fehler auszudehnen und dadurch die Wechselwirkung fehlerhafter Hardware mit der Software zu analysieren.
Die Analyse von Hardwarefehlern im Hinblick auf ihre Auswirkungen in der Software ist bislang Simulationstechniken vorbehalten. Diese sammeln für bestimmte Einsatzfälle oder Anwendungsszenarien statistische Daten, die meist unsicher sind. Gravierende Sicherheitsrisiken bleiben so unerkannt.
Hingegen kann der im PROFORMA-Projekt vorangetriebene Ansatz den formalen Beweis erbringen, daß eine zu gewährleistende Sicherheitsfunktion unter allen modellierten Fehlern immer ihre definierte Aufgabe erfüllt.
Dazu sehen die Projektpartner vor, die Auswirkungen von Fehlern von der Hardware bis hin zur Anwendungssoftware vollautomatisch auf mathematisch korrekte Art und Weise zu modellieren. Auf diesem Wege können dann Sicherheitsgarantien abgeleitet werden.
Dieser Ansatz verspricht in der industriellen Anwendung eine qualitative Verbesserung der Sicherheitsanalysen gegenüber dem Stand der Technik bei gleichzeitiger Kostenreduktion durch Automatisierung.
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 formalen Verifikationstechniken, Software-Analyse, Modellprüfung und Tests.
Das Projekt wird durch das Bundesministerium für Bildung und Forschung gefördert.