Renommierter Preis für Informatiker der TU-Wien
piqs.de/David Shankbone
Der Informatiker Helmut Veith von der TU Wien erhielt den prestigeträchtigen CAV-Award für computergestützte Verifikation.
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 deren logische Systembeschreibungen korrekt sind.
Helmut Veith vom Institut für Informationssysteme der TU Wien forscht seit Jahren auf dem Gebiet Computer Aided Verification (CAV) und Model Checking. Nun erhielt er bei der internationalen CAV-Conference gemeinsam mit sieben anderen Forschern den CAV-Award, eine der international renommiertesten Auszeichnungen auf diesem Gebiet.
Das Modell und 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.
Von Knotenpunkten und Vereinfachungsstrategien für die Praxis
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 zu untersuchende Computerprogramm 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 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 industriell im Bereich Soft- und Hardware eine wichtige Rolle. Die CEGAR-Methode gilt als wichtiger Schritt, der die praktische Anwendung von automatisiertem Model Checking in der Industrie erst möglich gemacht hat.
