Modul CS4138-KP06, CS4138SJ14
Model Checking (ModelChe14)
Dauer
1 Semester
Angebotsturnus
Jedes Wintersemester
Leistungspunkte
6
Studiengang, Fachgebiet und Fachsemester:
- Master Medizinische Ingenieurwissenschaft 2020, Wahlpflicht, Informatik/Elektrotechnik, Beliebiges Fachsemester
- Master IT-Sicherheit 2019, Wahlpflicht, IT-Sicherheit Safety und Reliability, 1., 2. oder 3. Fachsemester
- Master Medizinische Ingenieurwissenschaft 2014, Wahlpflicht, Informatik/Elektrotechnik, Beliebiges Fachsemester
- Master Medizinische Informatik 2014, Wahlpflicht, Informatik, 1. oder 2. Fachsemester
- Master Informatik 2014, Wahlpflicht, Anwendungsfach IT-Sicherheit und Zuverlässigkeit, 1. oder 2. Fachsemester
Lehrveranstaltungen:
- CS4138-Ü: Model Checking (Übung, 1 SWS)
- CS4138-V: Model Checking (Vorlesung, 3 SWS)
Workload:
- 60 Stunden Präsenzstudium
- 100 Stunden Selbststudium und Aufgabenbearbeitung
- 20 Stunden Prüfungsvorbereitung
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:
- Klausur oder mündliche Prüfung nach Maßgabe des Dozenten
Modulverantwortliche:
Literatur:
- C. Baier, J.-P. Katoen : Principles of Model Checking MIT Press, 2008
Sprache:
- Englisch, außer bei nur deutschsprachigen Teilnehmern
Bemerkungen:
Zulassungsvoraussetzungen zur Belegung des Moduls:- Keine
Zulassungsvoraussetzungen zur Teilnahme an Modul-Prüfung(en):
- Erfolgreiche Bearbeitung von Übungsaufgaben gemäß Vorgabe am Semesteranfang
Modulprüfung(en):
- CS4138-L1: Model Checking, mündliche Prüfung, 100% der Modulnote
Letzte Änderungen:
05.08.2021