Algorithms for Software Model Checking

• Antragsteller: Professor Dr. Javier Esparza, bis 3/2007
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2004 bis 2009
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5421798

Model-Checking ist eine Technik zur automatischen Verifikation von Rechensystemen, bei der der erreichbare Zustandsraum vollständig untersucht wird, und die sehr erfolgreich auf große Hardware-Systeme angewandt wird. Die Erweiterung und Anwendung auf Software gehört zu den großen Aufgaben der aktuellen Forschung im Bereich formaler Verifikation. Die Schwierigkeit liegt u.a. darin, dass Software-Systeme unendlich viele Zustände annehmen, während Hardware-Systeme endlich sind. In unseren Vorarbeiten haben wir Model-Checking-Algorithmen für Pushdown-Systeme entwickelt. Letztere sind eine Klasse von Systemen mit unendlichem Zustandsraum, die sich zur Modellierung von Programmen mit (womöglich rekursiven) Prozeduren eignen. Diese Algorithmen wurden in dem Programm Moped implementiert. Die Algorithmen bzw. das Programm werden z.Zt. von Forschungsprojekten in Berkeley, an der CMU, in Graz, bei Inria, und in Wisconsin benutzt. Diese Projekte sowie unsere eigenen Experimente zur Verifikation von Treibern in Windows NT zeigen auch einen Bedarf für effiziente Algorithmen für generellere Klassen von Systemen und Spezifikationen. Was Systeme betrifft, werden Verfahren benötigt für Programme, die mit einer Umgebung kommunizieren, sowie für nebenläufige und Echtzeit-Programme. Was Spezifikationen betrifft, sollte die jetzige Logik LTL zu CTL* mit Vergangenheitsoperatoren erweitert werden, und zu Logiken, mit denen man quantitative Eigenschaften ausdrücken kann. Ziel des Projekts ist die Entwicklung solcher Algorithmen, ihre Implementierung in Moped und ihre Erprobung an Fallstudien der o.g. Projekte.

• DFG-Verfahren: Sachbeihilfen
• Beteiligte Person: Dr. Stefan Schwoon