Fehler im System Der Traum von Software ohne Bugs

Fehlerfreie Programme gibt es nicht, sagen Entwickler. Diese Aussage ist überholt, behaupten Wissenschaftler und arbeiten an Tools, die mit strenger Logik die Fehlerfreiheit von Software beweisen können. Betriebssysteme wie Unix oder Windows sind dafür aber noch eine Nummer zu groß.

Von Karlhorst Klotz


Risiko Software: Im Cockpit des Airbus A380 dominiert die Elektronik
AFP

Risiko Software: Im Cockpit des Airbus A380 dominiert die Elektronik

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!"

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.

Start einer Ariane 5: Satelliten im Millionenwert an Bord
AFP

Start einer Ariane 5: Satelliten im Millionenwert an Bord

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."



© SPIEGEL ONLINE 2005
Alle Rechte vorbehalten
Vervielfältigung nur mit Genehmigung der SPIEGELnet GmbH


Die Homepage wurde aktualisiert. Jetzt aufrufen.
Hinweis nicht mehr anzeigen.