Ganz entspannt auf Fehlersuche

Manchmal hat er Alpträume von seinen Problemen. Aber Amir Pnueli leidet nicht unter Depressionen. Er sucht nur nach Softwarefehlern.

Sein längst zur Leidenschaft gewordener Beruf ist der Hauptgrund, warum Amir Pnueli, Professor für Informatik am Weizmann Institute of Science in Rehovot, Israel, und neuerdings auch an der New York University, hin und wieder eine Reise nach Kiel unternimmt. Er ist ein Freund des Gründers der Kieler Informatik, Professor Hans Langmaack, und auch mit dem erst kürzlich pensionierten Professor Willem-Paul de Roever verbinden ihn sowohl eine langjährige Freundschaft als auch etliche gemeinsame Publikationen und Projekte. Der Kern all dieser Projekte berührt stets das Thema, das Pnueli den auch als inoffiziellen Nobelpreis der Informatik bekannten Turing Award des Jahres 1996 eintrug: die Entwicklung gültiger mathematischer Methoden, um zu beweisen, dass ein System von Programmen korrekt arbeitet.

Das klingt so, als ob weder Laien noch Experten sich wirklich dafür begeistern könnten. Und Pnueli, der zu den Pionieren dieses Wissenschaftszweiges gehört, bestätigt, dass dies in der Tat eine Zeit lang der Fall war und anfangs nur die wenigsten Zeitgenossen seiner Tätigkeit die angemessene Bedeutung zuerkannten.

Heute ist Pnueli 67 Jahre alt und zumindest mit der Haltung der Experten zufrieden. »Das Verständnis dafür, dass man Programme nur dann als korrekt bezeichnen kann, wenn dies mathematisch zu beweisen ist, hat sich immer mehr durchgesetzt«, bilanziert der Wissenschaftler. Allein die Argumente von Pnueli und anderen Experten reichten dazu allerdings nicht aus. Die Wirklichkeit erwies sich als grimmige Lehrmeisterin für all jene, die mögliche Software- und Hardwarefehler nicht präzise genug analysierten. Ein defekter Intel-Prozessor bescherte dem Hersteller in den Neunziger Jahren einen Verlust von 500 Millionen Dollar. Auch die Katastrophe des Ariane-Fluges 501, der 1996 mit einer Explosion nur 40 Sekunden nach dem Start endete, wurde durch einen Softwarefehler verursacht, oder genauer gesagt durch einen in der Entwicklungsphase unerkannt gebliebenen Konflikt zwischen Software und Hardware. Allein der materielle Schaden betrug bei diesem Unglücksfall eine halbe Milliarde Euro.

»Fehler im fertiggestellten Produkt sind sehr teuer«, resümiert Pnueli, der zudem einige kostspielige Pannen bei Autoherstellern und anderen verbraucherorientierten Industrien aufzählen kann. Deshalb ist er sicher, dass es allein schon aus ökonomischen Gründen keine bessere Methode gibt, als mögliche Fehler im Programmdesign so früh wie möglich aufzuspüren.

Der Wissenschaftler aus Israel wurde besonders für seine Analysen paralleler und nebenläufiger Systeme bekannt. Diese Systeme existieren sowohl im Internet als auch in großen Unternehmen mit einer hohen Anzahl vernetzter Computer. Und sie sind sogar Standard in jedem häuslichen Arbeitszimmer. »Auf einem gewöhnlichen PC laufen stets mehrere Applikationen gleichzeitig«, erklärt Pnueli.

Aber wie kann man Systeme mit millionenfacher Interaktion überprüfen? Pnueli und seine Kollegen verwenden die Technik der Abstraktion. Sie stellen Systeme und die Programme, die sie kontrollieren, durch ein mathematisches Modell dar, das einige unwichtige Details ausblendet, aber dennoch die wesentlichen Elemente beizubehalten versucht. Die Analyse dieses vereinfachten Modells kann oft vollkommen automatisiert durch den Computer vorgenommen werden. Dabei wird die Genauigkeit des abstrakten Modells ständig verfeinert, bis die Methode den Beweis für einen Fehler im ursprünglichen Design offenlegt oder aber die Fehlerlosigkeit des Designs bestätigt. Manchmal findet diese wiederholte Prozedur kein Ende. In solchen Fällen ist selbst ein alter Hase wie Pnueli am Rande der Verzweiflung: »Das größte Problem ist, den tiefer liegenden Grund wirklich zu verstehen«, erklärt er die intellektuelle Herausforderung.

Manchmal träumt Pnueli dann tatsächlich von einem dieser ungelösten Rätsel. Und oft kommt die Erleuchtung spontan beim Duschen oder Abwaschen. Denn »Denken funktioniert am besten, wenn man vollkommen entspannt ist und den Geist mühelos wandern lässt.«

Martin Geist

Zuständig für die Pflege dieser Seite: Pressestelle der Universität, presse@uv.uni-kiel.de