Eingebettete Systeme sind komplexe Computersysteme, die auf bestimme Anwendungen spezialisiert sind – etwa im Automobilbau, der Luft- und Raumfahrttechnik, der Medizintechnik oder im Anlagenbau. Sie besitzen in der Regel keine universellen Schnittstellen für den menschlichen Benutzer (Tastatur, Monitor), sondern sind unsichtbar in eine Anwendung „eingebettet“ und kommunizieren lediglich mit einer technischen Systemumgebung.
Eingebettete Systeme nehmen vielfältige Steuerungsaufgaben in nahezu allen Industriebranchen wahr. In einem modernen Automobil der Mittelklasse, beispielsweise, befinden sich 50 bis 100 Mikroprozessoren, die in sogenannten „Systems-on-Chip“ (SoC) integriert sind und auf denen Programme mit mehreren Millionen Zeilen Code ablaufen.
Systeme, in denen zahlreiche Prozessoren miteinander vernetzt sind und somit mehrere Programme gleichzeitig („nebenläufig“) ablaufen, werden zunehmend auch in sicherheitskritischen Anwendungen eingesetzt, um die Vielzahl der Steuerungsaufgaben zu bewältigen. Dies bedeutet eine grundlegende Abkehr vom konventionellen Paradigma, bei dem Steuerungsprogramme stets als einzelnes Programm auf einem einzigen Prozessor ausgeführt werden.
Der Einsatz nebenläufiger Architekturen macht es jedoch sehr viel schwieriger, die Sicherheit eines Systems zu garantieren. Es muß eine Vielzahl von zeitlichen und funktionalen Abhängigkeiten zwischen den verschiedenen Prozessen korrekt berücksichtigt werden. Bereits kleinste Fehler können unüberschaubare Folgen haben.
Ein hohes Maß an Sicherheit auch in nebenläufigen Systemen zu ermöglichen, ist das gemeinsame Ziel der FORTISSIMO-Projektpartner AbsInt, OneSpin Solutions und TU Kaiserslautern.
Dabei sollen sogenannte formale Verifikationstechniken zum Einsatz kommen. Im Unterschied zur Simulation, die ein System immer nur stichprobenartig untersucht, erbringen formale Techniken den vollständigen mathematischen Beweis, daß bestimmte Eigenschaften für jedes mögliche Verhalten des Systems erfüllt sind.
Die Projektpartner haben bereits in der Vergangenheit eine Vorreiterrolle bei der Erforschung, Entwicklung und industriellen Einführung formaler Verifikationstechniken eingenommen.
Im FORTISSIMO-Projekt bündeln sie nun ihre Kompetenzen auf dem Gebiet formaler Verifikationstechniken für Hardware, Software und für die Hardware/Software-Schnittstelle, um gemeinsam neue Techniken zur Analyse nebenläufigen Verhaltens zu erforschen.
Das Projekt wird durch das Bundesministerium für Bildung und Forschung gefördert.