Model Checking
| Credits | Workload | Kontaktzeit | Selbststudium | Dauer |
|---|---|---|---|---|
| 6 CP | 180 h | 5 SWS (75 h) | 105 h |
Teilnahmevoraussetzungen
- Kenntnis grundlegender Automatenmodelle und regulärer Sprachen (Vorlesung Formale Systeme, Automaten und Prozesse)
- Kenntnis der Aussagenlogik (Vorlesung Mathematische Logik)
- Kenntnis von Datenstrukturen wie Stacks, Bäumen und Graphen und deren elementarer Algorithmen (Vorlesung Algorithmen und Datenstrukturen)
- Grundkenntnisse in Komplexitätstheorie (Vorlesung Berechenbarkeit und Komplexität)
Lehrveranstaltungen
| Veranstaltung/ Lehrform | CP | SWS | Häufigkeit | |
|---|---|---|---|---|
| Vorlesung Model Checking | 6 CP | 3 SWS | SoSe, jährlich | |
| Übung Model Checking | 2 SWS | SoSe, jährlich | ||
Prüfungsleistung
Note
Lernergebnisse / Kompetenzen
Erwerb der folgenden Kenntnisse und Fähigkeiten:
- Modellierung von (nebenläufigen) Programmen
- Kenntnisse über Eigenschaftsklassen
- Verständnis der Konstruktion und Wirkungsweise von Model-Checking-Algorithmen für LTL und CTL
- Verständnis einiger elementarer Abstraktionsmechanismen
- Fähigkeit zum Einsatz eines Model Checkers (Spin)
Inhalte
Folgende Hauptthemen:
- Transitionsysteme
- Nebenläufige und Kanalsysteme
- Eigenschaftsklassen: Safety, Liveness, Invarianten und Fairness
- Linear Temporal Logic (LTL)
- Computation Tree Logic (CTL)
- Model-Checking-Algorithmen für LTL und (fair) CTL
- Abstraktion: (Bi-)Simulation
Alternative Wahlmodule zu diesem Modul
Dieses Modul gehört zur Gruppe "Wahlpflicht Informatik". 9 Module (bestehend aus Vorlesung und Übung) zu wählen aus dem Wahlpflichtprogramm in den vier Bereichen: „Angewandte Informatik“, „Software & Kommunikation“, „Daten- und Informationsmanagement“, „Theoretische Informatik“. In jedem Bereich sind mind. 6, höchstens jedoch 30 ECTS zu erwerben. Die Module sollten so gewählt werden, dass im 1. Studienjahr in der Regel 36 ECTS, im zweiten Studienjahr 24 ECTS erworben werden.
Angewandte Informatik
- Computational Differentiation
- Designing Interactive Systems II
- Einführung in die Computergraphik
- Einführung in High-Performance Computing
- HCI Design Patterns
Daten- und Informationsmanagement
- Datenbanken und Informationssysteme
- Einführung in die künstliche Intelligenz
- Einführung in die Wissensrepräsentation
- Implementation of Databases
- Inhaltsbasierte Ähnlichkeitssuche
- Web Engineering
Software und Kommunikation
- Architekturmodellierung von Softwaresystemen
- Datenkommunikation und Sicherhei
- Einführung in Eingebettete Systeme
- Modellbasierte Softwareentwicklung
- Verteilte Anwendungssysteme und Middleware
Theoretische Informatik
- Angewandte Automatentheorie
- Berechenbarkeit und Komplexität
- Compilerbau
- Einführung in Effiziente Algorithmen
- Funktionale Programmierung
- Logikprogrammierung
Modulzuordnung
Master of Science: Fach Grundlagen der Informatik: Bereich Theoretische Informatik
Disclaimer
Bitte beachten Sie, dass im Zweifel (z.B. sich widersprechende Angaben auf der Website und dem Modulhandbuch) für Ihr Studium immer die Angaben in der aktuellen Bachelorprüfungsordnung mit den entsprechenden Anhängen verbindlich sind. Wenden Sie sich bitte an die Fachstudienberatung, wenn Ihnen Unstimmigkeiten auffallen.
