Tool gegen einfrierende Rechner

Neuer Ausweg aus einem alten Informatik-Problem

Das Problem galt in seiner Zunft lange als besonders tückisch. Anders als bei Fehlern, die zu einem völligen Absturz führen, läuft bei einer Verletzung der Lebendigkeitseigenschaften das Programm weiter - es nimmt aber keine neuen Befehle an und tut nichts Sinnvolles. Für Software-Tester ist mit dieser Art von Bugs besonders schwer umzugehen. "Woher sollen sie wissen, ob sie noch eine Minute warten sollen oder ob nie eine Antwort kommt?" erläutert Andrey Rybalchenko.

Für Informatiker steckte zudem eine besondere akademische Herausforderung in dem Problem. In den 1930er Jahren hatte der Informatik-Pionier Alan Turing es als sogenanntes "Halteproblem" beschrieben und gezeigt, dass es nicht grundsätzlich lösbar sei. Für alle möglichen Eingaben zu beweisen, dass ein Programm sinnvoll reagiert, schien unmöglich.

Andrey Rybalchenko entdeckte nun zusammen mit dem Freiburger Informatik-Professor Andreas Podelski ein neues Prinzip namens "Transitionsinvarianten". Damit sei es möglich, in automatischen Verfahren die Lebendigkeitseigenschaften von Software zu beweisen, erklärt Rybalchenko. Der Kniff der beiden Wissenschaftler: Sie schafften es, den aus vielen Teilgebieten der Informatik bekannten Ansatz "Teile und herrsche" auch auf die Lebendigkeitseigenschaften anzuwenden. Das große Problem wird in viele kleine und lösbare Probleme zerlegt. Die einzelnen Ergebnisse werden anschließend wieder zusammengesetzt.

Tool an Windows-Treibern getestet

Andrey Rybalchenko setzte die Transitionsinvarianten anschließend in die Praxis um. Im Sommer 2005 arbeitete er drei Monate lang bei MicrosoftMicrosoft Research im englischen Cambridge. Dort begann er ein Verifikations-Tool zu entwickeln, dem er den Namen Terminator gab. Mit Byron Cook von Microsoft testete der Informatiker den Terminator an Windows-Gerätetreibern. Immer wenn sie angefordert wurden, reagierten die Abfertigungsroutinen der Treiber nachweisbar auf das Betriebssystem. Die Versuche zeigten, dass die bisher als unmöglich geltenden automatischen Testverfahren von Lebendigkeitseigenschaften sich doch durchführen lassen. Alles zu Microsoft auf CIO.de

Bei Microsoft arbeitet man jetzt auf Grundlage von Rybalchenkos Erkenntnissen weiter. Ansätze des Terminators könnten einfließen in künftige Versionen des Static Driver Verifiers (SDV). Dieses Werkzeug sucht nach Fehlern im Code von Windows-Treibern. Ob und wann die Projektarbeit in einen neuen SDV münden wird, sei derzeit nicht abzusehen, lässt Byron Cook aus Cambridge ausrichten. Er schickt hinterher: Andrey Rybalchenko sei ein fantastischer Wissenschaftler und Dozent. "Er besitzt die wunderbare Gabe, reale Probleme mit tiefschürfender mathematischer Theorie zu verbinden."