Medien zu diesem Beitrag

• SIMONE Gleise© FIRST
  
• ConTrain Eisenbahnplatte© FIRST
  

<>

Innovationsgrad

REDAKTION:

7

COMMUNITY:

4

Marktreife2011

Bei Fragen zur Verlässlichkeit eingebetteter Software in sicherheitskritischen Anwendungen geraten traditionelle Testmethoden an ihre Grenzen. Bereits heute beträgt der Anteil der Validierung an den Gesamtkosten bis zu 80 Prozent. Denn es ist in der Regel äußerst aufwendig, eine ausreichend große Menge an Testfällen zu generieren, um die notwendige Testabdeckung zu erreichen. Ein Nachweis der Softwaresicherheit lässt sich (unter Umständen) aber auch mathematisch führen.

Eine natürliche Zahl ist durch drei teilbar, wenn die Summe ihrer einzelnen Ziffern ebenfalls drei oder ein Vielfaches davon ist. Dass dies so ist, lernt jedes Kind in der Schule und jeder Mathematikstudent kennt den exakten mathematischen Beweis dieser Regel. Ähnlich einfach ist die Goldbachsche Vermutung: Jede gerade Zahl größer als zwei lässt sich als Summe zweier Primzahlen schreiben. Ein mathematischer Beweis, dass dies im ganzen unendlichen Zahlenraum auch tatsächlich so ist, konnte hier bisher aber noch nicht gefunden werden. In einem aufwendigen Verteiltes-Rechnen-Projekt wurde die Gültigkeit der Regel bis zur Zahl 2 Trillionen erfolgreich getestet (Stand November 2010). Eine Fehlfunktion der Regel bei nur einer der verbleibenden unendlich vielen Möglichkeiten, kann aber auch nach der Vielzahl erfolgreicher Tests nicht ausgeschlossen werden. Bei der Validierung sicherheitskritischer Software ist dasselbe Problem alltäglich: Mit Softwaretests kann immer nur ein kleiner Teil aller denkbarer Systemzustände erfasst werden. Im Gegensatz zur Theorie der Mathematik kann vom einwandfreien Funktionieren eingebetteter Systeme wie beispielsweise Steuergeräten in einem Auto, einem Flugzeug oder in einem medizinischen Gerät, das Leben von Menschen abhängen. Zu Recht werden deshalb hohe Anforderungen an die Testabdeckung zur Überprüfung der Funktion sicherheitskritischer Software gestellt – auch, wenn der damit verbundene Aufwand im hohen Maße zeit- und geldintensiv ist. Dabei bleibt es jedoch ein grundlegendes Problem, dass jeder Test nur die Wahrscheinlichkeit einwandfreien Funktionierens erhöht, sie aber niemals endgültig belegt. Verschärft wird diese Situation dadurch, dass die Größe und Komplexität eingebetteter Software noch erheblich zunehmen wird.

In einem vom Bundesforschungsministerium und vom Französischen Staat geförderten Gemeinschaftsprojekt von Fraunhofer FIRST und dem französischen Carnot-Institut CEA LIST werden Methoden und Softwarewerkzeuge getestet und weiterentwickelt, mit denen sich die fehlerfreie Funktion von Softwarekomponenten eingebetteter Systeme mathematisch beweisen lässt. Ausgangspunkt eines solchen Beweises ist eine formale Spezifikation der Anforderungen, welche die Software erfüllen soll. Diese Spezifikation und der Quellcode des Programms werden automatisch analysiert und in mathematische Theoreme transformiert. Danach wird mit Theorembeweisen schlüssig nachgewiesen, ob das Programm bei Einhaltung der Vorbedingungen die spezifischen Nachbedingungen erfüllt. Ein wichtiger Knackpunkt dabei ist das Finden einer „passenden“ Beweisführung. Die Forscher am Fraunhofer FIRST verwenden das von ihrem französischen Partner entwickelte Frama-C-Framework und dessen deduktive Verifikations-Plug-Ins. Denn mit diesem System lassen sich die für eine Verifikation benötigten formalen Beweise weitgehend automatisch generieren.

Eine Garantie, dass ein Beweis gefunden werden kann, gibt es allerdings nicht – ebenso wie in anderen Bereichen der Mathematik. Es könnte sein, dass  das Verifikations-Tool nicht in der Lage ist, im speziellen Fall den Beweis zu finden. Oder es ist möglich, dass ein mathematischer Beweis nicht durchführbar ist. Ziel der Projektarbeiten ist es daher, spezifisches Know-how in der Anwendung des Beweisverfahrens zu sammeln und die eingesetzten Methoden und Tools weiter zu verbessern. Als Beispielanwendungen untersuchen die Forscher derzeit vor allem Steuergeräte in der Bahntechnik. Dazu gehört zum Beispiel die in jedem Zug vorhandene Sicherheitsfahrschaltung: Sie bremst automatisch, wenn der Zugführer keine Rückmeldung gibt. Um dies zu verhindern drückt der Bedienstete während der gesamten Fahrt regelmäßig einen Knopf. Geschieht dies in einer voreingestellten Zeitspanne nicht, wird ein Signalton als Erinnerung des Zugführers aktiviert. Gibt er darauf erneut keine Rückmeldung, interpretiert das System dies als möglichen Notfall und leitet die Bremsung ein. Solche und ähnliche unterschiedlich umfangreiche und komplexe Sicherheitssysteme analysieren die Forscher am Fraunhofer FIRST. Sie wollen herausfinden, mit welchen Methoden und ob ein mathematischer Beweis der Funktionsfähigkeit der in den Steuergeräten eingesetzten Software möglich ist.

Die Erfahrungen aus derartigen Modellfällen sind grundlegend, um einschätzen zu können, unter welchen Voraussetzungen eine Anwendung des Beweisverfahrens überhaupt sinnvoll ist. Zu komplexe Softwareanwendungen etwa können (zumindest derzeit) per Beweis nicht belegt werden. Die Forscher am Fraunhofer FIRST konnten im Rahmen der Projektarbeiten aber auch belegen, dass in vielen Anwendungsfällen das Beweisverfahren den für die Validierung erforderlichen Aufwand an Zeit und Kosten verringern kann. Zudem bringt jede erfolgreiche Beweisführung einen eindeutigen Sicherheitsgewinn: Denn das Beweisverfahren belegt eindeutig, dass eine Software innerhalb eines bestimmten Werteintervalls fehlerfrei funktioniert. Testreihen dagegen können dies immer nur mit einer gewissen Wahrscheinlichkeit nahelegen.