Themenmodul Model Checking

Credits Workload Kontaktzeit Selbststudium Dauer
6 CP180 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)

In den Übungen kann es Veranstaltungen mit Anwesenheitspflicht geben (gemäß § 6). Die erfolgreiche Teilnahme an den regelmäßigen Übungen ist Voraussetzung für die Zulassung zur Prüfung.

Lehrveranstaltungen

Veranstaltung/ Lehrform CP SWS Häufigkeit
Vorlesung Model Checking 6 CP 3 SWS jedes 3. Semester
Übung Model Checking   2 SWS jedes 3. Semester

Prüfungsleistung

90- bis 120-minütige Klausur

Note

Die Modulnote ist die Note der Klausur.

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 mindestens 3 der 4 Bereiche sind mindestens 6 CP zu erwerben. In jedem der Bereiche sind höchstens 30 CP zu erwerben. Die Module sollten so gewählt werden, dass im 1. Studienjahr in der Regel 36 CP, im zweiten Studienjahr 24 CP erworben werden.

Angewandte Informatik

Daten und Informationsmanagement

Software und Kommunikation

Theoretische Informatik

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.