Model Checking (Sommersemester 2017)

Vorlesung: Prof. Dr. Markus Müller-Olm

Übungen: Prof. Dr. Markus Müller-Olm, Sebastian Kenter

Eintrag für diese Veranstaltung im HIS/LSF

Learnweb-Kurs zu dieser Veranstaltung

Hinweise

  • Aktuelle Informationen und Übungsblätter zu dieser Veranstaltung werden im zugehörigen Learnweb-Kurs veröffentlicht. Zum Login auf der Learnweb-Plattform genügt Ihre ZIV-Benutzerkennung mit Passwort; der Einschreibeschlüssel zum Zugriff auf diesen Kurs wird in der ersten Vorlesung bekannt gegeben.

Ort und Zeit

  • Vorlesung + Übungen: Di 10:15-12:00 Uhr, M5 und Fr 10:15-12:00 Uhr, M5.
  • Beginn: Dienstag, 18.4.2017, 10:15 Uhr, M5.

Vorlesungsinhalt

Eine zunehmend auch von der Industrie eingesetzte Technik zur Aufdeckung versteckter Fehler in Hard- und Softwaresystemen ist das sogenannte Model-Checking. Ein Model Checker überprüft automatisch, ob ein Modell eines Systems eine gewünschte, typischerweise in einer temporalen Logik spezifizierte Eigenschaft besitzt. Die Vorlesung behandelt die verschiedenen Ansätze zur Konstruktion von Model-Checkern sowie theoretische und praktische Fragestellungen im Umfeld dieser Methode.

Literatur

Alle drei Bücher befinden sich im Semesterapparat in der Bibliothek.

  1. C. Baier und J.-P. Katoen, Principles of Model Checking, MIT Press, 2008.
  2. B. Berard, M. Bidoit, A. Finkel, F. Larroussinie, A. Petit, L. Petrucci, Ph. Schnoebelen, Systems and Software Verification, Springer-Verlag, 2001.
  3. E. M. Clarke, O. Grumberg, D. A. Peled, Model Checking, MIT Press, 1999