© Ferrigato/IST Austria

Model Checking

Turing-Preisträger Ed Clarke im Interview

Diese Woche startet das Nationale Forschungsnetzwerk zu „Rigorous Systems Engineering“, welches sich aus neun Wissenschafter aus dem Institute of Science and Technology Austria, der Johannes Kepler Universität Linz, der TU Graz und TU Wien, sowie der Universität Salzburg zusammensetzt. Für eine Laufzeit von vier Jahren stehen dem Projekt 3,75 Millionen Euro Fördergelder des Wissenschaftsfonds zur Verfügung. Ziel ist die Forschung auf dem Gebiet der mathematisch basierten Programmerstellung voranzutreiben. Hauptaugenmerk liegt dabei auf den Bereichen Model Checking und Verifikation von Hard- und Software. Damit können Fehler im Programmcode aber auch in Schaltkreisen von Computerchips gefunden werden, bevor diese in Produktion gehen.

Ed Clarke, der die Keynote zur Eröffnung hielt, leistete zusammen mit seinem Team Pionierarbeit bei dem Einsatz von Model Checking und wurde dafür mit mehreren Auszeichnungen geehrt. 2007 erhielt er sogar, gemeinsam mit Allen Emerson und Joseph Sifakis, den mit 250.000 US-Dollar dotierten Turing Award, der als Nobelpreis der Computerwissenschaften gilt. Die futurezone sprach mit Clarke über seine Arbeit und die Zukunft des Model Checkings.

futurezone: In ihrer Rede sagten Sie, dass mit der weiten Verbreitung von Computersystemen und Chips auch die Programmierung immer schwieriger wird. Wie kann Model Checking helfen?
Clarke: Model Checking ist eine mathematische Methode zur Überprüfung von Schaltkreisen und Programmiercode. Dabei werden alle möglichen Konstellationen von Algorithmen überprüft, um zu verifizieren, ob das Programm fehlerfrei funktioniert. Kommt das Programm jedoch zu stehen, lässt sich mit dem Model Checker genau anzeigen, wie es zu dem Fehler gekommen ist. Menschen als Programmierer machen oft Fehler und so können vor der Veröffentlichung des Produkts diese Fehler gefunden werden. Man kann damit auch Sicherheitsprotokolle überprüfen. Wenn der Model Checker eine Sequenz findet, die das Sicherheitsprotokoll zum Abstürzen bringt, gleicht das einer Attacke.

Und was, wenn solche Fehler nicht gefunden werden?
Software kann man im Nachhinein patchen, deshalb gibt es auch immer noch mehr Soft- als Hardware-Fehler. Bei der Hardware ist es schwieriger. Intel lieferte 1994 den ersten Pentium-Prozessor aus, der wegen drei fehlerhaften Einträgen falsche Ergebnisse lieferte. Intel musste eine Million Prozessoren umtauschen, was dem Unternehmen über 400 Millionen US-Dollar gekostet hat. Intel hat mich später kontaktiert und mich gebeten, ihnen einen meiner Studenten vorbeizuschicken. Der konnte ihnen dann zeigen, dass mit Model Checking der Fehler vor der Auslieferung gefunden worden wäre.

Wenn Model Checking so gut funktioniert, dass sie dafür sogar mit dem Turing Award ausgezeichnet wurden, wieso gibt es dann heute immer noch fehlerhafte Hard- und Software?
Das liegt daran, dass immer neue Hard- und Software designt wird und es deshalb auch immer neue Fehler gibt. Würden wir die Neuentwicklungen einstellen, was nie passieren wird, könnten wir alles Bestehende verifizieren und sicher gehen, dass alles korrekt funktioniert.

Basieren die neuen Fehler, die auftreten, auf alten Fehlern, die in früheren Versionen nicht ausgebessert wurden?
Ich glaube, so etwas wie einen ersten Computer Bug, auf dem alle anderen Bugs basieren, gibt es nicht. Es gibt viele Ursachen die Fehler auslösen, aber es gibt bestimmte Anwendungen, die besonders anfällig dafür sind: parallel-laufende Prozesse. Diese müssen strikte Protokolle erfüllen, um sich nicht gegenseitig zu blockieren. Und sind diese Protokolle falsch programmiert, was leicht passieren kann, da Menschen nur schwer bereits beim Programmieren alle erdenklichen Konstellationen bedenken können, kommt es zu Fehlern. Ein Beispiel: Ein schneller Zug ist gefährlich. Nähert er sich gleichzeitig mit einem anderen Zug einer Schienenkreuzung, bleibt er stehen, um einen Unfall zu vermeiden. Das ist logisch. Folgt der andere Zug aber ebenfalls dieser Logik, stehen beide vor der Kreuzung und keiner bewegt sich.

Sie erwähnten in ihrer Keynote, dass Model Checking einen erheblichen Einfluss auf die Wirtschaft haben kann. Die österreichische IT-Wirtschaft ist aber nicht besonders groß. Was machen wir also mit den Forschungsergebnissen? An große Unternehmen verkaufen?
Ich bin kein Geschäftsmann, diese Entscheidung sollte jemand treffen, der mehr ökonomisches Wissen und Erfahrung hat. Auf jeden Fall kommt aber zuerst die Forschung. Man braucht kein großes Unternehmen wie IBM, um ein wichtiges Überprüfungs-Tool zu entwickeln und auch keine enormen Großrechner oder spezielle Technologie. Österreich kann stolz sein auf dieses Projekt und ist jetzt in den Top-Rängen der Länder, die diese Art von Forschung betreiben.

Wäre ein zuverlässiges Model Checking das Ende der Beta-Tester?
Nein, denn wir brauchen jede Hilfe, die wir kriegen können. Ich vertraue keinem Menschen, meine Software zu testen. Ich vertraue aber auch keinem Model Checker. Ich würde beides zusammen nutzen. Model Checking kann allerdings die Zeit deutlich verkürzen, die rein menschliche Tests in Anspruch nehmen.

Könnte man Model Checking auch auf Menschen anwenden?
Dafür bin ich noch nicht bereit. Der Mensch ist zu kompliziert und ich hoffe nicht, dass das menschliche Verhalten jemals so stark reguliert wird, dass man mit Model Checking verhindert, dass er Fehler macht. Es gab Versuche, Programme zu schreiben, die Menschen befolgen sollten. Die könnte man Model checken. Aber ich halte solche Programme für eine schlechte Idee.

Und wie sieht es mit Robotern aus?
Roboter haben vorgegebene Programme und Protokolle die sie befolgen, da funktioniert Model Checking. Bei der DARPA Grand Challenge, ein vom US-Verteidigungsministerium gesponsertes Roboter-Autorennen, gewann 2005 das Team der Stanford Universität. Die Forscher, die das Roboterauto gebaut haben, haben vor dem Start Model Checking angewandt und über 100 ernste Fehler in der Software gefunden und korrigiert. Das Auto des Teams der Carnegie Mellon Universität, an der ich unterrichte, blieb auf der Strecke liegen und es schaffte es nicht ins Ziel. Sie haben kein Model Checking des Protokolls gemacht.

Das heißt, Model Checking wirkt sich direkt auf die Entscheidungen der Roboter aus.
Ja, es könnte sie davon abhalten Fehler zu machen. Das sollte kein Problem sein, solange man nicht Kreativität von einem Roboter erwartet. Zur jetzigen Zeit sollten nur Menschen kreativ sein, nicht Roboter.

Sie haben ihre ganze Karriere dieser mathematischen Suche nach Fehlern verschrieben. Wieso?
Zu jener Zeit, als ich noch auf der Schule war, waren Computerwissenschaften weit simpler als heute. Entweder man entwickelte einen Algorithmus oder prüfte ob diese korrekt ist. Ich machte Nummer Zwei, denn ein schneller Algorithmus bringt nichts, wenn er nicht korrekt funktioniert.

Ist der Turing-Preis für sie die Auszeichnung ihres Lebenswerkes oder nur ein Zwischenschritt in ihrer Forscher-Laufbahn?
Es ist nur ein Schritt bevor ich weiter gehe. In meinem neuesten Projekt versuche ich Model Checking zu nutzen, um die komplexen, biochemischen Signalwege zu debuggen, die bei Bauchspeicheldrüsenkrebs involviert sind. Die Signalwege bei Krankheiten wie Bauchspeicheldrüsenkrebs sind so komplex, dass sie oft mit Schaltkreisen verglichen werden. Also versuchen wir unsere Erfolge bei der Prüfung von Computer-Schaltkreisen auf die biologischen Schaltkreise umzulegen.

Sie werden also vom Computer-Doktor zum richtigen Doktor?
Da würde mein Sohn widersprechen. Ich habe drei Söhne, zwei haben einen wissenschaftlichen Doktor-Titel und der Jüngste einen medizinischen. Er sagt immer, dass er der einzig echte Doktor in der Familie ist.

Hat dir der Artikel gefallen? Jetzt teilen!

Gregor Gruber

Testet am liebsten Videospiele und Hardware, vom Kopfhörer über Smartphones und Kameras bis zum 8K-TV.

mehr lesen
Gregor Gruber

Kommentare