| Lerninhalte |
Das Modul führt, von den Grundlagen bis zum aktuellen Stand der Kunst, in
Methoden der automatischen Verifikation von dynamischem Eigenschaften
für Systeme ein. Im Zentrum stehen dabei Technologien zum Model
Checking.
Inhalte
• Transitionssysteme (Beschreibung von Systemen)
• Temporale Logik (Beschreibung von Eigenschaften)
• Explizites Model Checking, Reduktionstechniken (Symmetrie, Partial Order,
Sweep-Line)
• Symbolisches Model Checking (BDD-basiert, SAT-basiert, Automatenbasiert)
• Model Checking für Echtzeitsysteme
• Abstraktion und Abstraktionsverfeinerung
• Model Checking für Software |
