Model-Checking II | WS 2008/09

Neuigkeiten | Termine | Inhalt | Folien

Bemerkung: Der Kurs kann auf deutsch oder englisch stattfinden, je nach Präferenz der Zuhörer. Kenntnisse in Automatentheorie und eine vorige Teilnahme am Kurs Model-Checking I sind nützlich, aber nicht unabdingbar.

Model-Checking ist eine automatische Technik, die feststellt, ob ein Hardware- oder Software-System korrekt arbeitet. In der Vorlesung Model-Checking wurden bereits die Grundlagen des Model-Checkings für Systeme mit endlichem Zustandsraum eingeführt.

Schon einfache Software-Systeme haben jedoch meist einen unendlichen Zustandsraum und sind Turing-mächtig, so dass es i.A. unentscheidbar ist, ob ein gegebenes Programm irgendeine Spezifikation erfüllt. Dennoch hat die Forschung in den letzten 10-15 Jahren bedeutende Fortschritte erzielt, entscheidbare Sonderfälle identifiziert und Methoden entwickelt, mit denen sich viele Programme trotzdem analysieren lassen. Diese basieren auf einfachen, aber wirkungsvollen mathematischen Ideen kombiniert mit cleveren algorithmischen Ideen. Darauf basierende Verifikationstools halten nach und nach Einzug in die Software-Industrie.

Die Vorlesung stellt einige dieser Techniken vor, von den theoretischen Grundlagen bis hin zu Anwendungen. Die betrachteten Analysetechniken behandeln unterschiedliche Kategorien von unendlichen Zustandsräumen, d.h. Systeme mit unendlichem Kontrollfluss (rekursive Prozeduren und dynamische Thread-Erzeugung), unendlichen Daten (ganze und reelle Zahlen, Zeit, Listen und andere Zeigerstrukturen) sowie parametrisierte Systeme, bei denen die Teilnehmerzahl nicht a priori feststeht. Wo dies möglich ist, werden entsprechende Verifikationswerkzeuge vorgestellt.