inf455 - Model Checking (Vollständige Modulbeschreibung)

Nützliche Vorkenntnisse: 

Mengenlehre, Aussagen- und Prädikatenlogik, endliche Automaten 

Model Checking ist eine Technik der automatischen Verifikation für Hardware und Software Systeme. Die Studierenden erhalten in der Vorlesung Kenntnisse und Fähigkeiten in der Anforderungsspezifikation mittels temporaler Logik und der automatischen Überprüfung des Systems bezüglich der Anforderungen durch algorithmische Verfahren. 
 

Fachkompetenzen 
Die Studierenden:

• benennen die Operatoren in temporalen Logiken und die Unterschiede zwischen linear-temporalen und branching-time Logiken
• spezifizieren Anforderungen in LTL und CTL
• übersetzen LTL-Formeln in Büchi-Automaten
• konstruieren BDDs für boole‘sche Funktionen
• können CTL Formeln in Fixpunktform darstellen
• wenden Modelchecking Algorithmen auf Kripkestrukturen an
• kennen die Unterscheidungskraft von Bisimulation

Methodenkompetenzen 
Die Studierende:

• wenden formale Modellierung an
• beweisen Eigenschaften von temporalen Logiken
• wenden Modelchecking Werkzeuge zur Verifikation von Systemen an

Sozialkompetenzen 
Die Studierenden:

• bearbeiten in Gruppen Übungsaufgaben, diskutieren Ergebnisse
• entwickeln gemeinsam Beschreibungen von Systemen und interpretieren die Resultate von Werkzeugen

Selbstkompetenzen 
Die Studierenden:

• organisieren sich selber bei der Arbeit an den Aufgabenstellungen des Moduls

• Temporale Logiken LTL und CTL
• Büchi Automate
• Explizites Model Checking
• Binary decision diagrams
• Verbände, Fixpunkte, CTL als Transformer
• Symbolisches Model Checking
• Bisimulation

am Ende des Semesters

Klausur oder mündliche Prüfung