Spezifikation und Verifikation: Model Checking (A).
Termin: Montag, 10-12 in C-221 (SoSe 2008)
Die Vorlesung unterteilt sich in die Veranstaltung "Model-Checking (A)" am Montag und "Infinite State Systems: Analyse von Systemen mit unendlichem Zustandsraum (B)" am Donnerstag. Beide Teile sind jeweils in sich abgeschlossen, so dass Studierende des Diplomstudiengangs wahlweise auch nur eine der beiden Veranstaltung besuchen können.
Vorgehen und Inhalt
Zur Einführung werden entsprechende Teile aus FGI 2 / PNL z.T. in modifizierter Darstellung kurz wiederholt. Daran schließen sich weitere und vertiefende Inhalte an (siehe unten). Insbesondere kann auf das neue Buch von Esparza und Heljanko (siehe unten) eingegangen werden. Anders als in FGI 2 / PNL wird - dem Charakter einer kleineren Vorlesung entsprechend - auf die speziellen Wünsche und Bedürfnisse der Teilnehmenden eingegangen.
Aus dem KVV:
Lernziel:
Zu Teil (A):
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.
Zu Teil (B):
Systeme, die keinen endlichen Zustandsraum besitzen, können nicht mehr durch Model-Checking verifiziert werden. Trotzdem ist es möglich, diese Systeme zu analysieren: Das Erreichbarkeitsproblem für unbeschränkte Petrinetze ist ein berühmtes Beispiel für ein entscheidbares Problem.
Die Analyse solcher Systeme weist Bezüge zum Theorembeweisen und damit auch zu funktionalen Programmiersprachen, zum Lamdakalkül und zu Logiken höherer Ordnung auf.
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. Girault, R. Valk: Petri Nets for Systems Engineering , Springer, Berlin, 2003, Part III: Verification
E.M. Clarke et al.: Model Checking, The MIT Press, Cambridge, 1999
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
L. Priese und H. Wimmel. Petri-Netze. Springer. 2003
Y. Bertot und P. Castéran. Interactive Theorem Proving and Program Development. Spinger-Verlag. 2004
Henk Barendregt. Lambda Calculi with Types.
Morten Heine B. Sorenson and Pawel Urzyczyn. Lectures on the Curry-Howard Isomorphism.
Materialien zur Veranstaltung
- Folien Kapitel 0 : Geschichte und Bedeutung des Model-Checking Model Checking 0
- Folien Kapitel 1 : Die temporalen Logiken CTL und LTL Model Checking 1
- Folien Kapitel 2 : Algorithmen für CTL und LTL Model Checking 2
- Folien Kapitel 3 : Tools für CTL und LTL Model Checking 3
- Folien Kapitel 4 : Binäre Entscheidungsdiagramme (BDD) Model Checking 4
- Folien Kapitel 5 : Symbolisches Model-Checking (nur als Papierkopie)
- Folien Kapitel 6 - Teil 1 : Model-Checking durch Auffalten 1 Model Checking 5
- Folien Kapitel 6 - Teil 2 : Model-Checking durch Auffalten 2 Model Checking 6
Impressum
Korrekturen, Anmerkungen bitte an:
Rüdiger Valk
