Inhalte:
Modellieren reaktiver Systeme in SPIN und Promela
Spezifizieren von Anforderungen in temporalen Logiken
Automatentheoretische Modelle von Systemen und Spezifikationen
Verifikation durch Erreichbarkeitsanalyse
Symbolisches Modelchecking und Binäre Entscheidungsdiagramme
Modelchecking mit NuSMV
Automatenmodelle mit Zeit
Modellchecking von Zeitautomaten mit Uppaal