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