Formale Technik für eingebettete Systeme – Sicherheit in nebenläufigen Systemen

Eingebettete Systeme sind komplexe Computer­systeme, die auf bestimme Anwendungen spezialisiert sind – etwa im Automobil­bau, der Luft- und Raumfahrt­technik, der Medizin­technik oder im Anlagen­bau. Sie besitzen in der Regel keine univer­sellen Schnitt­stellen für den menschli­chen Benutzer (Tastatur, Monitor), sondern sind unsichtbar in eine Anwendung „eingebettet“ und kommuni­zieren lediglich mit einer techni­schen System­umgebung.

Eingebettete Systeme nehmen vielfältige Steuerungs­aufgaben in nahezu allen Industrie­branchen wahr. In einem modernen Auto­mobil der Mittel­klasse, beispiels­weise, befinden sich 50 bis 100 Mikro­prozessoren, die in sogenannten „Systems-on-Chip“ (SoC) inte­griert sind und auf denen Programme mit mehreren Milli­onen Zeilen Code ablaufen.

Systeme, in denen zahlreiche Prozessoren mit­einander vernetzt sind und somit mehrere Pro­gramme gleich­zeitig („neben­läufig“) ablaufen, werden zuneh­mend auch in sicher­heits­kritischen Anwen­dungen ein­gesetzt, um die Vielzahl der Steuerungs­aufgaben zu be­wältigen. Dies bedeutet eine grund­legende Abkehr vom kon­ventio­nellen Para­digma, bei dem Steuerungs­programme stets als einzelnes Pro­gramm auf einem einzigen Pro­zessor aus­geführt werden.

Der Einsatz nebenläufiger Archi­tekturen macht es jedoch sehr viel schwieriger, die Sicher­heit eines Systems zu garan­tieren. Es muß eine Vielzahl von zeit­lichen und funktio­nalen Abhängig­keiten zwischen den verschie­denen Pro­zessen korrekt berück­sichtigt werden. Bereits kleinste Fehler können un­überschaubare Folgen haben.

Ein hohes Maß an Sicherheit auch in neben­läufigen Systemen zu er­möglichen, ist das gemein­same Ziel der FORTISSIMO-Projektpartner AbsInt, OneSpin Solutions und TU Kaisers­lautern.

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.