|
Der Informatiker Helmut Veith von der TU Wien erhielt den prestigeträchtigen CAV-Award
für computergestützte Verifikation.
San Francisco/Wien (tu) - Computer machen Fehler, und Fehler sind ärgerlich. Weil kein Mensch ein kompliziertes
Programm vollständig analysieren kann, wird diese Aufgabe heute automatisiert: Computerprogramme untersuchen,
ob andere Computerprogramme (oder abstrakter ausgedrückt: logische Systembeschreibungen) korrekt sind. Prof.
Helmut Veith vom Institut für Informationssysteme der TU Wien forscht seit Jahren mit großem Erfolg
auf dem Gebiet Computer Aided Verification (CAV) und Model Checking. Nun erhielt er bei der internationalen CAV-conference
gemeinsam mit sieben anderen Forscherinnen und Forschern mit dem CAV-Award, der als international angesehenste
Auszeichnung auf diesem Gebiet gilt.
Hält sich das Modell an die Regeln?
Ein Computerprogramm kann sich in vielen verschiedenen Zuständen befinden. Variablen können unterschiedliche
Werte annehmen, und abhängig davon wechselt das Programm in einen neuen Zustand. Überprüft werden
soll, ob bestimmte mathematisch formulierte Qualitätsanforderungen in jedem möglichen Zustand und jeder
möglichen Programmausführung erfüllt werden. Solche Regeln können beispielsweise darin bestehen,
dass das Programm niemals in einer unendlichen Schleife gefangen sein soll, aus der man nicht mehr herauskommt,
oder dass bestimmte Werte der Variablen, die das Programm zum Absturz bringen würden, niemals angenommen werden
dürfen.
Das System, das man untersuchen möchte, kann man sich wie ein riesiges Netz vorstellen. Jeder Knotenpunkt
steht für einen bestimmten Zustand des Programms, und von jedem möglichen Zustand kann man eine bestimmte
Anzahl weiterer Zustände erreichen. „Die einfachste Verifikationsmethode wäre es, die Zustände nacheinander
zu durchlaufen und zu analysieren, ob es irgendwo zu Fehlern kommt.“, erklärt Helmut Veith. „Doch meistens
ist die Anzahl der möglichen Zustände so groß, dass das völlig unmöglich ist.“ Mit dem
verfügbaren Speicherplatz wächst die Anzahl der möglichen Zustände exponentiell an, daher können
solche naiven Testverfahren nur Programme mit sehr kleinem Speicher analysieren. Man muss sich für die Praxis
kluge Vereinfachungsstrategien überlegen.
Abstrahieren und verfeinern
Gemeinsam mit einigen Kollegen entwickelte Helmut Veith vor etwa 15 Jahren das sogenannte „Counterexample-Guieded
Abstraction Refinement“ (CEGAR). Dabei wird das Computerprogramm, das untersucht werden soll, zunächst abstrahiert
und vereinfacht, und dort wo es nötig ist, wird diese Abstraktion dann Schritt für Schritt verfeinert.
„Wenn dann ein Zustand entdeckt wird, der gegen die Qualitätsanforderungen verstößt, muss man zunächst
überprüfen, ob es sich tatsächlich um einen Fehler des Programms handelt, oder ob es bloß
ein Artefakt aufgrund der Abstraktion ist“, erklärt Helmut Veith. Ein echter Fehler wird gemeldet, ist bloß
die Abstraktion am vermeintlichen Problem schuld, wird die Darstellung des Systems verfeinert und die Analyse geht
weiter.
Model Checking spielt heute in der Industrie eine wichtige Rolle – sowohl im Bereich der Software als auch der
Hardware-Erzeugung. Die CEGAR-Methode gilt als wichtiger Schritt, der die praktische Anwendung von automatisiertem
Model Checking in der Industrie erst möglich gemacht hat.
Neben Helmut Veith wurden noch sieben weitere WissenschaftlerInnen mit dem CAV-Award ausgezeichnet – der Turing-Preisträger
Edmund Clarke (Carnegie Mellon University), Orna Grumberg (Technion), Ronald H. Hardin, Somesh Jha (University
of Wisconsin), Yuan Lu (Atrenta), Robert P. Kurshan (Bell Laboratories) und Zvi Harel (Technion). Übergeben
wurden die Preise am 22. Juli.
Helmut Veith studierte an der TU Wien, wo er 1998 auch promovierte (Sub auspiciis praesidentis). Danach ging er
an die Carnegie Mellon University in Pittsburgh (USA) und wechselte dann nach Deutschland – zunächst an die
TU München, dann an die TU Darmstadt. Seit 2005 ist er Adjunct Full Professor an der Carnegie Mellon University
(Pittsburgh, USA), und seit 2009 ist er Professor an der TU Wien.
|
