19304101
Lecture
WiSe 14/15: Modelchecking
Marcel Kyas
Comments
- 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.
Suggested reading
- 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 Class schedule
Regular appointments
Mon, 2014-10-13 14:00 - 16:00
Mon, 2014-10-20 14:00 - 16:00
Mon, 2014-10-27 14:00 - 16:00
Mon, 2014-11-03 14:00 - 16:00
Mon, 2014-11-10 14:00 - 16:00
Mon, 2014-11-17 14:00 - 16:00
Mon, 2014-11-24 14:00 - 16:00
Mon, 2014-12-01 14:00 - 16:00
Mon, 2014-12-08 14:00 - 16:00
Mon, 2014-12-15 14:00 - 16:00
Mon, 2015-01-05 14:00 - 16:00
Mon, 2015-01-12 14:00 - 16:00
Mon, 2015-01-19 14:00 - 16:00
Mon, 2015-01-26 14:00 - 16:00
Mon, 2015-02-02 14:00 - 16:00
Mon, 2015-02-09 14:00 - 16:00