Modul CS4138 T

Modulteil: Model Checking (ModelCha14)

Dauer:

1 Semester

Angebotsturnus:

Jedes Wintersemester

Leistungspunkte:

Studiengang, Fachgebiet und Fachsemester:

Master Informatik 2019 (Modulteil eines Wahlmoduls), Modulteil, Beliebiges Fachsemester
Master Medizinische Ingenieurwissenschaft 2020 (Modulteil eines Wahlmoduls), Informatik/Elektrotechnik, Beliebiges Fachsemester
Master Entrepreneurship in digitalen Technologien 2020 (Modulteil eines Wahlmoduls), Modulteil, Beliebiges Fachsemester
Master Entrepreneurship in digitalen Technologien 2014 (Modulteil eines Wahlmoduls), Modulteil, Beliebiges Fachsemester
Master Medizinische Ingenieurwissenschaft 2014 (Modulteil eines Wahlmoduls), Informatik/Elektrotechnik, 1. Fachsemester
Master Informatik 2014 (Modulteil eines Pflichtmoduls), Modulteil, Beliebiges Fachsemester

Lehrveranstaltungen:

CS4138-Ü: Model Checking (Übung, 1 SWS)
CS4138-V: Model Checking (Vorlesung, 3 SWS)

Workload:

20 Stunden Prüfungsvorbereitung
100 Stunden Selbststudium und Aufgabenbearbeitung
60 Stunden Präsenzstudium

Lehrinhalte:
Qualitätsaspekte von Softwaresystemen Analyse- und Verifikationstechniken für Softwaresysteme Grundlegende Model Checking Techniken Fortgeschrittene Techniken zum Model Checking

Qualifikationsziele/Kompetenzen:

Die Studierenden können Analyse- und Verifikationstechniken beschreiben und vergleichen.
Sie können Spezifikationen von Korrektheits- und Sicherheitseigenschaften erstellen, analysieren und bewerten.
Sie können verschiedene Systemmodelle charakterisieren und Systeme in geigneten Modellen formal darstellen.
Sie können verschiedene Techniken zum Model Checking von Hard- und Softwaresystemen erläutern sowie geeignete Techniken auswählen und einsetzen.
Sie können den Aufbau von Model Checkern erklären und Model Checker anwenden.
Sie können die Möglichkeiten und Grenzen von Model Checking kritisch beurteilen.

Vergabe von Leistungspunkten und Benotung durch:

Prüfungsform hängt vom übergeordneten Modul ab

Modulverantwortlicher:

Siehe Hauptmodul

Lehrende:

Institut für Softwaretechnik und Programmiersprachen

Prof. Dr. Martin Leucker

Literatur:

C. Baier, J.-P. Katoen: Principles of Model Checking - MIT Press, 2008

Sprache:

Englisch, außer bei nur deutschsprachigen Teilnehmern

Bemerkungen:

(Ist gleich CS4138SJ14)
(Ist Modulteil von CS4507)

Zulassungsvoraussetzungen zum Modul:
- Keine

Zulassungsvoraussetzungen zur Prüfung:
- Erfolgreiche Bearbeitung von Übungsaufgaben während des Semesters