Model Checking

Worum geht's

Du lernst, wie man Hardware- und Software-Systeme mit formalen Modellen beschreibt und wie man mit Model-Checking-Verfahren automatisch überprüft, ob diese Modelle gewünschte Eigenschaften erfüllen. Am Ende kannst du einfache Systeme modellieren, Eigenschaften in temporaler Logik formulieren und grundlegende Model-Checking-Algorithmen sowie Strategien gegen das Zustandsraum-Explosion-Problem erklären und auf kleine Beispiele anwenden.

Was du danach kannst

• Rolle von Model Checking für Software- und Hardware-Qualität erklären
• formale Modelle einfacher Systeme angeben
• Sicherheits- und Lebendigkeitseigenschaften in temporaler Logik formulieren
• Algorithmen zum Überprüfen von Spezifikationen anwenden
• Techniken zur Eindämmung des Zustandsraum-Problems erläutern

Aus was das Modul besteht

• VorlesungVermittlung der Grundlagen, Vorstellung von Techniken und Tools; während der Vorlesungen werden kleine Übungen online gelöst
• Tutorium/ÜbungBesprechung und Vertiefung der wöchentlichen Aufgabenlösungen

Lehrmethode

• VorlesungEinführung in Theorie, Methoden und Werkzeuge; interaktive Online-Übungen zur Vertiefung
• TutoriumDiskussion und Durchsprache der wöchentlichen Aufgaben
• schriftliche Aufgabenregelmäßige Übungsaufgaben zur praktischen Anwendung und Vorbereitung auf die Prüfung
• Tool-DemonstrationenPraktische Erfahrung im Einsatz von Model-Checking-Tools wie Spin, Blast, CBMC