Seite 3: Software ohne Fehl und Tadel

Inhaltsverzeichnis

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