I870 – Formale Verifikation

Modul
Formale Verifikation
Formal Verification
Modulnummer
I870 [I-870]
Version: 1
Fakultät
Informatik/Mathematik
Niveau
Master
Dauer
1 Semester
Turnus
Sommersemester
Modulverantwortliche/-r

Prof. Dr. rer. nat. Boris Hollas
boris.hollas(at)htw-dresden.de
Dozent/-in(nen)

Prof. Dr. rer. nat. Boris Hollas
boris.hollas(at)htw-dresden.de
Lehrsprache(n)
ECTS-Credits

5.00 Credits

Workload

150 Stunden

Lehrveranstaltungen

4.00 SWS (2.00 SWS Vorlesung | 1.00 SWS Übung | 1.00 SWS Praktikum)
Selbststudienzeit

0.00 Stunden

Prüfungsvorleistung(en)
Keine
Prüfungsleistung(en)

Mündliche Prüfungsleistung
Prüfungsdauer: 30 min | Wichtung: 100%
in "Formale Verifikation"
Lehrform

2/1/1  V/Ü/P
Medienform
Keine Angabe
Lehrinhalte/Gliederung
  • Temporale Logik: Syntax und Semantik von LTL, Transitionssysteme.
  • Model Checking mit Spin: Sprachelemente von Promela, nebenläufige Systeme, Kommunikationsprotokolle.
  • Software-Model-Checking durch SAT-Solving.
  • Abstrakte Interpretation: Halbordnungen, Verbände, abstrakte und konkrete Semantik, abstrakte Verbände, Kontrollflussgraphen. Anwendungen mit Microsoft Code Contracts.
Qualifikationsziele

Die formale Verifikation umfasst Verfahren, mit denen Fehler
in Hard- und Software frühzeitig erkannt und die Abwesenheit
von Fehlern garantiert werden kann. Seit einigen Jahren werden
diese Verfahren zur Verifikation von Kommunikationsprotokollen,
integrierten Schaltkreisen und sicherheitskritischer Software
erfolgreich eingesetzt.
Sozial- und Selbstkompetenzen
Keine Angabe
Besondere Zulassungsvoraussetzung
Keine Angabe
Empfohlene Voraussetzungen
Keine Angabe
Fortsetzungsmöglichkeiten
Keine Angabe
Literatur
  • Huth, Ryan: Logic in Computer Science, 2004.
  • Ben-Ari: Principles of the Spin Model Checker, 2007.
Aktuelle Lehrressourcen

-
Hinweise
Keine Angabe
Link zu Kurs/Lernressourcen im OPAL
Detailansicht schließen
© Modulux (Version 4.3)