Algorithms for Software Model Checking

• Applicant: Professor Dr. Javier Esparza, until 3/2007
• Subject Area: Theoretical Computer Science
• Term: from 2004 to 2009
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 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 Programme: Research Grants
• Participating Person: Dr. Stefan Schwoon