Modelchecking

Präsenzstudium: ca. 60 Std., Eigenstudium: ca. 90 Std.

Programmierkenntnisse, Theoretische Informatik

• Die Studierenden beschreiben die verschiedenen Ansätze des Modelcheckings und ordnen sie bzgl. ihrer Anwendungsdomänen ein
• Die Studierenden wenden verschiedene Modelchecker auf praxisrelevante Beispiele an und analysieren die Ergebnisse und Gegenbeispiele.
• Die Studierenden formulieren Systemeigenschaften anhand von Spezifikationen überprüfen diese mittels Modelchecking und korrigieren bzw. verbessern die analysierten Systeme.
• Die Studierenden beurteilen unter Berücksichtigung der Anwendungsdomäne die Möglichkeiten und Voraussetzungen zum Einsatz von Modelcheckern.

Softwareintensive Systeme sind in immer mehr Bereichen auch für sicherheitskritische (safety) Funktionen verantwortlich. Modelchecking hat sich mittlerweile als gut anwendbare Methode für automatisierte formale Analysen etabliert. Die Anwendungsgebiete reichen von Hardwaresystemen, über reaktive Softwaresysteme, C und Java Programmen bis zu verteilten, nebenläufigen kommunikationsbasierten Systemen.

In dieser Vorlesung lernen Sie unterschiedliche Analysemethoden für die verschiedenen Anwendungsgebiete kennen. In der Vorlesung werden u.a. folgende Themen behandelt:

• Grundlagen der Logik, Temporallogik und der Entscheidungsprobleme
• Formale Spezifikation von Systemen und deren Eigenschaften
• Zustandsübergangssyteme wie Kripkestrukturen und labelled transition systems
• Kodierung von Erreichbarkeitseigenschaften als Constraint Probleme

Tafel, Folien oder Beamer, Livecoding, Moodle, Anwendung von realen Modelcheckern

• Clarke, Grumberg, Kroening, Peled, Veith: Model Checking 2nd Edition, MIT Press, 2018
• Strichman, Kroening: Decision Procedures, Springer, 2016
• Baier, Katoen: Principles of Model Checking, MIT Press 2008
• Clarke, Henzinger, Veith, Bloem: Handbook of Model Checking, Springer 2018

Zusätzlich: Aktuelle Online-Quellen und Dokumentationen.