zurück zum Artikel

Fehlerfreie Programme gibt es nicht, sagen Entwickler. Diese Aussage ist überholt, behaupten Wissenschaftler und arbeiten an Tools, die streng mathematisch Fehlerfreiheit beweisen

Ein Desaster, 37 Sekunden nach Zündung der Triebwerke: Am 4. Juni 1996 explodiert die Trägerrakete Ariane 5 auf ihrem Erstflug, weil ein falsch konvertierter Messwert die Steuerungsrechner zum Abschalten zwingt. Die Explosion vernichtet vier Satelliten im Wert von rund 600 Millionen Euro. Ein halbes Jahrhundert Erfahrung mit Computern lehrt: Testen allein hilft nicht. Unzureichende Software-Tests verschlingen nach einer Studie des National Institute of Standards and Technology allein in der US-Wirtschaft rund 59 Milliarden US-Dollar pro Jahr. Und das, obwohl Entwickler oft die Hälfte der Zeit für die Fehlersuche opfern.

Fehlerfreie Software ist überall dort gefordert, wo man sich Ausrutscher nicht leisten kann, beispielsweise im Auto –- ein Absturz bei 180 Sachen kann leicht tödlich enden. Aber wer den Fehlerteufel wirklich zur Strecke bringen will, darf sich nicht auf schlampige Programmierung - oft genug unter extremem Zeitdruck –, unzureichende Dokumentation von Programmcode oder nicht standardisierte Softwareentwicklung allein konzentrieren.

Denn auch die beste Software kann durch unpassende Eingabewerte so aus dem Konzept gebracht werden, dass sie sinnlose oder gar gefährliche Ergebnisse liefert. Intel beispielsweise hatte mit dem so genannten Pentium- Bug Ende 1994 ein eindrucksvolles Beispiel für solche so genannten Laufzeitfehler erlebt. Der Prozessor lieferte in seltenen Fällen für ganz bestimmte Eingabewerte ein falsches Divisionsergebnis. Für alle anderen Zahlen rechnete der Prozessor korrekt.

Fatal, wenn sich beispielsweise in der Flugsteuerungssoftware des Airbus A 380 nur ein Kommando befände, das eine Division durch Null oder einen Überlauf verursacht. Dass Laufzeitfehler auftreten, schließt Patrick Cousot vom École Normale Supérieure in Paris jedoch kategorisch aus. Seine Analysesoftware hat die 500 000 Zeilen des Airbus-Programms untersucht, "vollautomatisch, ohne menschliche Intervention", wie Cousot stolz anmerkt. "Das ist eine Weltpremiere!"

Software ohne Fehl und Tadel

Das Analyseprogramme ASTRÉE (Analyseur statique de logiciels temps-réel embarqués) untersucht den Programmtext, indem es verallgemeinert: Wenn beispielsweise das Airbus-Programm zwei Variable von Null aus gemeinsam um eine Einheit hochzählt, also die Zahlenwerte (0;0), (1;1) et cetera erzeugt, schließt das Analyse-Tool daraus, dass das Programm mit Werten rechnet, die auf einer Geraden durch die Koordinaten (0;0) und (1;1) liegen. Cousots Technik der "abstrakten Interpretation" moniert allerdings eventuell Probleme, die das ursprüngliche Programm gar nicht aufweist. Denn vielleicht würde sich die Airbus-Elektronik an den Werten (0,7;0,7) verschlucken, die tauchen in Wirklichkeit jedoch nicht auf.

Neben der "abstrakten Interpretation" hat eine noch formalere Methode zur Fehlersuche die Schwelle zur industriellen Anwendung auf Software überschritten: das "Model- Checking". Ähnlich wie eine Ampel nicht gleichzeitig für den Straßenverkehr und den Fußgängerüberweg Grün zeigen darf, lassen sich auch für Software-Module kritische Zustände beschreiben, die sie nicht gleichzeitig mit anderen Programmteilen annehmen dürfen. Model-Checking versucht zu beweisen, dass verbotene Kombinationen nie gemeinsam auftreten - oder bricht mit einem solchen Fehlerbeispiel ab.

Intel setzt diese Methode heute zur Überprüfung komplexer Schaltungs-Layouts ein. Auch Microsoft greift für Gerätetreiber zu Model-Checking-Tools, bestätigt Tony Hoare vom Microsoft Research Center in Cambridge. "Die Treiber werden oft von Fremdfirmen geschrieben, aber im Betriebssystemkern ausgeführt, und können ernsthafte Auswirkungen haben, wenn sie fehlerträchtig sind."

Der dritte Weg zu ultrazuverlässiger Software verläuft noch am steinigsten: "Theorembeweiser" genannte Computerwerkzeuge sollen belegen, dass ein Programm seine Anforderungen lückenlos erfüllt. Denn von einer formalen Beschreibung der einzelnen Programmschritte ausgehend, versuchen sie mit Regeln der mathematischen Logik den Beweis zu führen, dass sich ein gewünschtes Ergebnis schlussfolgern lässt. Computer gehen dabei allerdings eher planlos vor, würden also möglicherweise Tausende wahrer, aber irrelevanter Aussagen beweisen. Oft arbeiten daher Spezialisten mit solchen Programmen interaktiv, indem sie sinnvolle Zwischenstationen vorgeben, zu denen die Theorembeweiser dann einen Beweispfad suchen.

Software ohne Fehl und Tadel

Zwei gut dotierte Forschungsprogramme sollen die praktische Anwendung der Verifikation auch in Deutschland vorantreiben: Das vom Bundesministerium für Bildung und Forschung mit über 3,5 Millionen Euro pro Jahr geförderte Verisoft konzentriert sich seit 2003 darauf, Systeme von industrieller Bedeutung vom Mikroprozessor bis zur Anwendung durchgängig zu verifizieren. Seit 2004 fördert zudem die Deutsche Forschungsgemeinschaft mit rund zwei Millionen Euro pro Jahr in ihrem Sonderforschungsbereich "Automatische Verifikation und Analyse komplexer Systeme" ebenfalls die formale Verifikation für hochgradig vernetzte Systeme, wie sie etwa im Transportwesen zu finden sind.

Dass sich heute Aufgaben bislang unerreichbarer Komplexität knacken lassen, will Verisoft mit Industriepartnern wie Infineon, T-Systems und BMW zeigen. "Wir sind ungefähr sechsmal produktiver als frühere Projekte dieser Art", schätzt Wolfgang Paul von der Universität Saarbrücken. Der wissenschaftliche Gesamtprojektleiter von Verisoft nennt als Begründung einerseits bessere Werkzeuge, und andererseits "sind unsere Korrektheitsbeweise viel kürzer als die der Konkurrenz". Nicht zuletzt kann Paul aber auch auf eine respektable Schar an Verifikationsspezialisten zurückgreifen. Einen großen Teil der rund 75 Postdoktoranden oder Doktoranden hat der Ehrendoktor der Technischen Universität von Khabarovsk über eine Kooperation mit der Hochschule in Russland herangezogen. Dennoch: "Formale Verifikation ist derzeit eher Kunst als Handwerk", aber Paul brennt darauf, dies zu ändern. Aus gutem Grund, denn wie Manfred Broy von der TU München anmerkt, "lässt sich die Bereitschaft der Doktoranden zum Tüfteln nur schwer in die Industrie übertragen".

Voraussetzung für die Arbeit des Theorembeweisers ist eine Spezifikation, wie es sie bei heutigen Industrieprojekten in der nötigen Präzision meist nicht gibt, denn oft wird nach einer kurzen Definitionsphase mit dem Programmieren begonnen. "Wenn man stärker strukturiert, merkt man sehr gut, welche Anforderungen nicht sauber sind", erklärt der stellvertretende wissenschaftliche Gesamtleiter Manfred Broy. Erst die formale Darstellung führe in vielen Fällen zur Aufdeckung von Inkonsistenzen, Auslassungen und Ungenauigkeiten: "Die Frage ist allerdings: Wie viel Schärfe muss ich haben?"

Software ohne Fehl und Tadel

Unter dem Strich bleibt die Frage, wie fehlerfrei die angeblich garantiert korrekte Software in der Praxis wirklich arbeitet. Auch Verisoft-Leiter Paul weist immer darauf hin, dass - abgesehen von Hardware-Problemen, fehlendem Verständnis der Physik oder gar höherer Gewalt - immer noch zwei potenzielle Fehlerquellen für verifizierte Software bleiben: Die Spezifikation könnte falsch sein und das Beweissystem selbst einen Fehler haben.

Allen Unwägbarkeiten zum Trotz ist sich Wolfgang Paul aber sicher: "Wir werden kleine industrielle Betriebssysteme, wie sie in Autos oder Zügen vorkommen, in ganz naher Zukunft verifizieren können." Geht damit endlich ein alter Traum der Informatik in Erfüllung? Selbst Paul, der mit 25 Jahren jüngster Professor Deutschlands und mit 36 Jahren jüngster Leibnizpreisträger war, bleibt an dieser Stelle vorsichtig: "Bis zur Verifikation von so etwas wie Unix oder Windows ist es natürlich noch ein sehr weiter Weg." (wst [1])

URL dieses Artikels:
https://www.heise.de/-277431

Links in diesem Artikel:
[1] mailto:wst@technology-review.de

Copyright © 2005 Heise Medien