• Nachrichten
• >Netzwelt
• >Tech
• >

  Fehler im System: Der Traum von Software ohne Bugs

Fehler im System Der Traum von Software ohne Bugs

Von Karlhorst Klotz

2. Teil: Wie strenge Logik Fehler ausmerzen soll

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.

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

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

© Technology Review, Heise Zeitschriften Verlag, Hannover