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.
close

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
close

16 Class schedule

Regular appointments

Mon, 2014-10-13 14:00 - 16:00

Lecturers:
Prof. Dr. Marcel Kyas

Location:
049/T9 Seminarraum (Takustr. 9)

Mon, 2014-10-20 14:00 - 16:00

Lecturers:
Prof. Dr. Marcel Kyas

Location:
049/T9 Seminarraum (Takustr. 9)

Mon, 2014-10-27 14:00 - 16:00

Lecturers:
Prof. Dr. Marcel Kyas

Location:
049/T9 Seminarraum (Takustr. 9)

Mon, 2014-11-03 14:00 - 16:00

Lecturers:
Prof. Dr. Marcel Kyas

Location:
049/T9 Seminarraum (Takustr. 9)

Mon, 2014-11-10 14:00 - 16:00

Lecturers:
Prof. Dr. Marcel Kyas

Location:
049/T9 Seminarraum (Takustr. 9)

Mon, 2014-11-17 14:00 - 16:00

Lecturers:
Prof. Dr. Marcel Kyas

Location:
049/T9 Seminarraum (Takustr. 9)

Mon, 2014-11-24 14:00 - 16:00

Lecturers:
Prof. Dr. Marcel Kyas

Location:
049/T9 Seminarraum (Takustr. 9)

Mon, 2014-12-01 14:00 - 16:00

Lecturers:
Prof. Dr. Marcel Kyas

Location:
049/T9 Seminarraum (Takustr. 9)

Mon, 2014-12-08 14:00 - 16:00

Lecturers:
Prof. Dr. Marcel Kyas

Location:
049/T9 Seminarraum (Takustr. 9)

Mon, 2014-12-15 14:00 - 16:00

Lecturers:
Prof. Dr. Marcel Kyas

Location:
049/T9 Seminarraum (Takustr. 9)

Mon, 2015-01-05 14:00 - 16:00

Lecturers:
Prof. Dr. Marcel Kyas

Location:
049/T9 Seminarraum (Takustr. 9)

Mon, 2015-01-12 14:00 - 16:00

Lecturers:
Prof. Dr. Marcel Kyas

Location:
049/T9 Seminarraum (Takustr. 9)

Mon, 2015-01-19 14:00 - 16:00

Lecturers:
Prof. Dr. Marcel Kyas

Location:
049/T9 Seminarraum (Takustr. 9)

Mon, 2015-01-26 14:00 - 16:00

Lecturers:
Prof. Dr. Marcel Kyas

Location:
049/T9 Seminarraum (Takustr. 9)

Mon, 2015-02-02 14:00 - 16:00

Lecturers:
Prof. Dr. Marcel Kyas

Location:
049/T9 Seminarraum (Takustr. 9)

Mon, 2015-02-09 14:00 - 16:00

Lecturers:
Prof. Dr. Marcel Kyas

Location:
049/T9 Seminarraum (Takustr. 9)

Subjects A - Z