Wie Fehler bereits beim Schreiben von Programmen systematisch ausgeschlossen werden können, erforschen erstmals österreichische Wissenschafter.
***
"Ich habe das noch nie gemacht" , gesteht Helmut Veith von der TU Wien, "aber würde man den Programmcode des aktuellen Windows-Betriebssystems ausdrucken, ergäbe das als einzelne Zeile die Distanz von Wien nach Salzburg." Das Unangenehme dabei: "Statistisch gesehen fänden wir auf dieser Strecke alle 30 Zentimeter einen Fehler im Code." Der Präsident des Institute of Science and Technology, Thomas Henzinger, verdeutlicht, was das im Alltag bedeutet: "Softwarefehler kosten die US-Wirtschaft 45 Milliarden Euro jährlich - das entspricht immerhin 0,6 Prozent des BIPs."
Allein der Stromausfall vom 14. August 2003 im Nordosten der USA hat einen wirtschaftlichen Schaden verursacht, der zwischen 4,5 und 7,5 Milliarden Euro liegt. Ausgelöst wurde er durch eine Banalität: Mehrere Computer hatten versucht, zeitgleich dieselben Informationen abzurufen, und erhielten die Auskunft: "Leitung besetzt!" Dass dies die häufigste Ursache für Systemabstürze ist, versucht Henzinger anhand eines bekannten Falls zu illustrieren: Wollen zwei Programme auf einen Drucker zugreifen, und die "Vorrangregeln" werden nicht eindeutig in den Programmcodes geklärt, kommt es zum Absturz.
Mit zunehmender Komplexität eines Systems steigen freilich die Chancen, dass einfache Verfügbarkeitsabfragen scheitern: Bei eingebetteten Systemen - etwa in Flugzeugen - muss ein Programm sogar mit der physischen Welt kommunizieren. Die Wahrscheinlichkeit, dass kombinierte Abfragen hier nicht funktionieren und ein System zum Absturz bringen, ist demnach um ein Vielfaches höher. Allerdings ist das zweite Szenario längst auch das realistischere: Nur mehr zwei Prozent der jährlich rund zehn Milliarden verkauften Mikroprozessoren werden im PC eingesetzt - die restlichen 98 Prozent finden sich nahezu unbemerkt von Benutzern in der globalen Infrastruktur.
Immer schneller fehlerhaft
Die rasche Evolution der Hardware nach dem Gesetz des Intel-Mitgründers Gordon Moore (Moores' Law) - alle zwei Jahre verdoppelt sich die Prozessorleistung - entschärft dieses Problem komplexer gewordener Rechenaufgaben aber keineswegs, sondern beschleunigt es sogar: Schnellere Rechnerleistung bedeutet letztlich nur, dass auch Softwarefehler schneller ans Tageslicht kommen.
Für Laien völlig unbegreiflich bleibt also eines: Warum haben es Programmierer bis zum heutigen Tag nicht geschafft, Fehler in Codes weitgehend auszuschließen? Die Erklärung dafür ist zwar simpel, aber auch ernüchternd: Die Ingenieursleistung für Software unterscheidet sich grundsätzlich von jener, mit der etwa Brücken gebaut werden. So ist es bei einer Brücke durch vorausgehende mathematische Berechnungen möglich, eine stabile Konstruktion zu simulieren. Für stabile Software trifft das nicht zu, da sie kein kontinuierliches System darstellt. Das bedeutet: Wird in der Software ein winziges Detail - ein einzelner Buchstabe im Code - verändert, hat das weitreichendere Konsequenzen als das Weglassen einer Schraube an einer Brücke. Die Ursachen für Ein- und Abstürze sind also grundlegend anders.
"Den ersten großen Dämpfer" , so Veith, verpasste der britische Logiker Alan Turing der Informatik als Wissenschaft bereits 1936. Sein mathematisch geführter und daher unverändert gültiger Beweis verdeutlichte die grundsätzliche Schwäche aller selbstreferenziellen Systeme und gipfelte in der Aussage: "Die Programmanalyse durch ein Programm ist unmöglich." Das Unmögliche möglich machen will jetzt ein österreichisches Forschungsnetzwerk, das heute zum ersten Mal der Öffentlichkeit vorgestellt wird.
Dazu wird gerade Arise - als Akronym für "Austrian Rigorous System Engineering" - nach österreichischem Vereinsrecht gegründet. Die Vorstellung, dass ein österreichischer Verein das Potenzial besitzt, mittelfristig ein Problem globalen Ausmaßes zu lösen, ist freilich amüsant. Denn Systemabstürze könnten durch das symbiotische Forschen von Wissenschafterinnen und Wissenschaftern des Institute of Science and Technology Austria, der TU Wien und Graz und der Unis Linz und Salzburg tatsächlich bald der Vergangenheit angehören oder zumindest eingeschränkt werden.
Automatische Analyse
Ihre Methode ist die Erweiterung des etablierten Model-Checking-Ansatzes (Wissen), womit bereits das gemacht wird, was Turing als unmöglich beschrieb: Software wird automatisiert durch Programme analysiert. Turings These ist dennoch nicht aufgehoben - ein Model-Checker kann das Funktionieren eines Systems nicht explizit beweisen, er erkennt nur Fehler im System. Der eigentliche Wert der Methode liegt somit in der Falsifikation.
Wie gut diese Methode funktioniert, kann auch Joseph Sifakis beim heute, Mittwoch, stattfindenden Gründungssymposium zum österreichischen Netzwerk erklären. Gemeinsam mit Allen Emerson und Edmund Clarke hat er 2007 den Nobelpreis der Computerwissenschaften für die Programmanalyse mit Programmen erhalten. Dieser Preis wird seit 1966 vergeben und ist - in diesem Fall absurderweise - nach Turing benannt. Dass in den wissenschaftlichen Arbeiten der Turing-Preisträger Zitate von Henzinger und Veith auftauchen, zeigt schließlich, von welcher wissenschaftlichen Exzellenz dieser neue Forschungscluster künftig profitieren wird. Model-Checking funktioniert bislang nur im Nachhinein - Programme werden also nach der Fertigstellung überprüft. Erklärtes Ziel der Rigorous-System-Engineering-Methode ist es aber, dass der automatisierte Codecheck schon Teil des Entwicklungsprozesses ist. Fehlerfrei generierte Programme wären dann zum ersten Mal in der Geschichte der Computerwissenschaften die neue Realität. (Sascha Aumüller/DER STANDARD, Printausgabe, 5. 5. 2010)