19304101
Vorlesung
WiSe 14/15: Modelchecking
Marcel Kyas
Kommentar
- Unterschied zwischen Programmieren und Modellieren
- Modellieren reaktiver Systeme in SPIN und Promela
- Spezifizieren von Anforderungen in temporalen Logiken
- Automatentheoretische Modelle von Systemen und Spezifikationen
- Entscheidungsverfahren für temporale Logiken
- Symbolisches Modelchecking und Binäre Entscheidungsdiagramme
- Modelchecking mit NuSMV
- Automatenmodelle mit Zeit
- Modellchecking von Zeitautomaten mit Uppaal
- Formale Methoden zur Abstraktion und dem Nachweis der erhaltenen Eigenschaften.
Literaturhinweise
- Christel Baier und Joost-Pieter Katoen, Principles of Model Checking, The MIT Press, 2008
- Mordechai Ben Ari, Principles of the SPIN Model Checker, Springer Verlag, 2008
- Gerard Holzmann, The SPIN Model Checker, Addison-Wesley, 2004
- Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled, Model Checking, MIT Press, 1999
16 Termine
Regelmäßige Termine der Lehrveranstaltung
Mo, 13.10.2014 14:00 - 16:00
Mo, 20.10.2014 14:00 - 16:00
Mo, 27.10.2014 14:00 - 16:00
Mo, 03.11.2014 14:00 - 16:00
Mo, 10.11.2014 14:00 - 16:00
Mo, 17.11.2014 14:00 - 16:00
Mo, 24.11.2014 14:00 - 16:00
Mo, 01.12.2014 14:00 - 16:00
Mo, 08.12.2014 14:00 - 16:00
Mo, 15.12.2014 14:00 - 16:00
Mo, 05.01.2015 14:00 - 16:00
Mo, 12.01.2015 14:00 - 16:00
Mo, 19.01.2015 14:00 - 16:00
Mo, 26.01.2015 14:00 - 16:00
Mo, 02.02.2015 14:00 - 16:00
Mo, 09.02.2015 14:00 - 16:00