Vorlesungs-Folien

    H.P.Gumm: Model Checking

    Vorlesungsfolien für Model Checking, Sommersemester 2007.

    1. Organisatorisches
      • Inhalt
      • Literatur
      • Organisatorisches
      • Software
    2. Einführung
      • Fehler und Konsequenzen
      • Probleme verteilter Systeme
      • Modellierung und temporale Spezifikation
      • Model Checking
    3. Das SMV-System
      • Syntax von NuSMV
      • Prozessmodellierung
      • Temporale Formeln
      • Arbiter und Alternating Bit Protokoll
    4. Kripke-Strukturen und SMV
      • Kripke Strukturen
      • Relationenalgebra
      • Modellierung von Programmen
      • Logische Beschreibungen
    5. Lineare Temporale Logik
      • Lineare Temporale Logik
      • Semantik und Äquivalenzen
      • Fixpunktgleichungen
      • Lineare Äquivalenz
    6. Verzweigungslogik.pdf
      • Computation Tree Logic
      • Semantik und Äquivalenz
      • Bisimulation, Hennessy Milner
      • Ausdrucksstärke, CTL*
    7. CTL Model Checking
      • CTL Model Checking Algorithmen
      • Fixpunkte
      • Tarjan's Algorithmus für SCC
      • Fair-CTL
    8. LTL Model Checking
      • Büchi-Automaten
      • Tableaus
      • Implementierung
      • CTL*-Model Checking
    9. Symbolisches Model Checking
      • Symbolische Repräsentation
      • Entscheidungsbäume
      • BDD-Algorithmen
      • BDD-Semantik
    10. Bounded Model Checking
      • Endliche Gegenbeispiele
      • l-k-Schleifen
      • Rückführung auf SAT-Problem
      • Stalmark-Algorithmus
    11. Safety und Liveness
      • Beobachtkarkeit und Sicherheit
      • Lebendigkeit
      • Satz von Alpern-Schneider
      • Der ultrametrische Folgenraum