OCG Pressemeldungen 2006
Presseinformation, 29. November 2006
Heinz Zemanek-Preis 2006, Kat. A, an Dr. Marko Samer
für seine Disseraton Reasoning about Specifications in Model Checking
Im Alltag sind wir ständig mit automatisierten Systemen konfrontiert, deren mögliche Fehlfunktion mit hohen Kosten verbunden ist oder sogar Menschenleben gefährden kann. Beispiele für derart kritische Systeme sind Flug- und Eisenbahnkontrollsysteme, Automobilelektronik, medizinische Instrumente, Steuerungen von Atomkraftwerken, Finanztransaktionssysteme, Telekommunikationssysteme usw. Aus diesem Grund befassen sich Informatiker auf dem Gebiet der Formalen Methoden mit Verifikationstechniken, die es erlauben, subtile logische Fehler in solchen Systemen mit Hilfe des Computers zu finden.
Dr. Marko Samer verfasste seine Dissertation unter der Betreuung von Prof. Helmut Veith (TU München, Carnegie Mellon) und Prof. Georg Gottlob (Oxford, TU Wien) am Institut für Informationssysteme der TU Wien. Im Zentrum seiner Dissertation steht die praxiserprobte Verifikationstechnik Model Checking. Model Checking ist ein aktuelles
Forschungsgebiet der Informatik im Schnittbereich zwischen Grundlagenforschung und Anwendung und wurde mittlerweile von führenden Industrieunternehmen, wie etwa Intel, IBM, Microsoft und Siemens, als Schlüsseltechnologie erkannt. Wird beim Model Checking ein Fehler gefunden, so liefert der Computer eine Fehlerbeschreibung zurück, mit deren Hilfe das untersuchte System korrigiert und einer erneuten Prüfung unterzogen werden kann. Dieser Vorgang kann so lange wiederholt werden, bis kein Fehler mehr gefunden wird. Dabei kann es passieren, dass das System – obwohl noch fehlerhaft – alle formalen Anforderungen erfüllt, aber nur deshalb, weil diese unvollständig spezifiziert sind und nur erwartete Fehler abdecken. In praktischen Anwendungen kommt dieser Fall relativ häufig vor und ist immer ein Hinweis auf ein ernstzunehmendes Problem.
In seiner Dissertation hat Dr. Samer einen neuartigen Zugang zur Lösung dieser Problematik aufgezeigt und systematisch untersucht. Dazu hat er eine mathematische Beschreibungsmethode und Algorithmen entwickelt, die auf sogenannten temporallogischen Queries basieren. Mit diesen können nicht nur erwartete Eigenschaften des untersuchten Systems nachgewiesen werden, sondern der Computer berechnet „intelligent“ bislang unbekannte Eigenschaften des Systems. Die Resultate der Dissertation wurden bei mehreren internationalen wissenschaftlichen Konferenzen publiziert.
