Software ohne Fehl und Tadel
Fehlerfreie Programme gibt es nicht, sagen Entwickler. Diese Aussage ist überholt, behaupten Wissenschaftler und arbeiten an Tools, die streng mathematisch Fehlerfreiheit beweisen
- Karlhorst Klotz
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!"
