TGI-Lehre WWW

Kontakt | TGI-aktuell | Suche | Rundgang

Model Checking

Veranstalter: Rüdiger Valk

Termin: Montag, 14:15-15:45 in C-221 (SoSe 2010)

Dieser Modul mit dem Titel "Spezifikation und Verifikation (SuV)" unterteilt sich in die Vorlesungen "Model-Checking " am Montag und "Logik und Typtheorie" am Donnerstag. Beide Teile sind jeweils in sich abgeschlossen, so dass Studenten des Diplomstudiengangs wahlweise auch nur eine der beiden Veranstaltung besuchen können.

Motivation:

Am 4. Juni 1996 explodierte eine Ariane-5-Rakete 40 Sekunden nach dem Start. Die Untersuchungskommission stellte später als Grund eine Ausnahmebehandlung in der Flugleitsoftware fest. Eine fehlerhafte Gleit/Festkomma-Konversion verursachte im Haupt- wie im Backup-Rechner einen Fehler, der zu einer inkorrekten Datenübermittlung an den Bordrechner führte, der seinerseits daraufhin die Selbstzerstörung einleitete. Daraufhin wurde die Software einer umfangreichen Verifikation unterzogen. Model-Checking-Methoden fanden dadurch auch in Europa vermehrt Beachtung. Solche Ereignisse sind keine Einzelfälle, obwohl die Gebiete Programmierung, Softwaretechnik, Systemtechnik und verteilte Systeme in der Informatik relativ gut vertreten sind und vielfältige Methoden, Techniken und Vorgehensweisen entwickelt haben. Als Grund ist unter anderem eine unzureichende Durchdringung der genannten Gebiete mit formal abgesicherten Konzepten, Modellen und Methoden zu nennen.

In dieser Vorlesung sollen vorwiegend solche Methoden der Verifikation durch Model-Checking vorgestellt werden, die für relativ große Systeme tatsächlich angewandt werden und für die effektive Werkzeuge zur Verfügung stehen. So wurden bereits beeindruckend große Systeme erfolgreich verifiziert: beispielsweise Systeme mit mehr als 10exp20 Zuständen.

Lernziel und Vorgehen:

Erlernt werden sollen Methoden der Systemverifikation, die weitgehend unabhängig von der Systemmodellierung sind - im Gegensatz zu solchen, die spezielle Eigenschaften der Modellierung ausnutzen. Dabei sind die entsprechenden Spezifikationstechniken wie CTL, CTL*, LTL einzusetzen. Die Systemmodellierung beruht auf Zustandsdiagrammen, Statecharts, Petrinetzen und Prozessalgebra. Spezielle Methoden sind Binäre Entscheidungsdiagramme (BDDs), symbolische und parametrisierte Methoden, sleep-set- und stubborn-set-Methoden, Reduktionen durch partielle Ordnungen, Symmetrieausnutzung, Verifikation von Sicherheits-, Lebendigkeits und Fairness-Eigenschaften, strukturelle Methoden, deduktive- und prozessalgebra-basierte Methoden. Typische Anwendungsgebiete sind mobile Systeme, kryptografische Protokolle und eingebettete Systeme. Die Studenten lernen die formalen Grundlagen und erarbeiten sich durch ihre ein Gefühl für die Möglichkeiten und Grenzen der formalen Spezifikation. Neben den theoretischen Grundlagen werden exemplarisch einige Computer-Werkzeuge im kleineren Rahmen praktisch vorgeführt. Typische Anwendungsgebiete sind mobile Systeme, kryptografische Protokolle und eingebettete Systeme. Vorgehen: Die Studenten lernen die formalen Grundlagen und erarbeiten sich durch ihre ein Gefühl für die Möglichkeiten und Grenzen der formalen Spezifikation. Neben den theoretischen Grundlagen werden exemplarisch einige Computer-Werkzeuge im kleineren Rahmen praktisch erprobt.

Literatur:

  • C. Baier und J.-P. Katoen: Principles of Model Checking, The MIT Press, Cambridge, 2008
  • E.M. Clarke et al.: Model Checking, The MIT Press, Cambridge, 1999
  • M. Huth, D. Ryan: Logic in Computer Science - Modelling and Reasoning about Systems, Cambridge University Press, 1999
  • C. Girault, R. Valk: Petri Nets for Systems Engineering , Springer, Berlin, 2003, Part III: Verification
  • B. Bérard et al.: Systems and Software Verification, Springer, Berlin, 1999
  • J. Esparza, K. Heljanko: Unfoldings - A Partial-Order Approach to Model Checking, Springer, Berlin, 2008

    • Materialien zur Veranstaltung

    (Benutzername und Passwort wie bei FGI2/PNL)