Name | Programmverifikation | |||||||||||||||||||||||||||||||||||
Verantwortlich | Prof. Dr. Matthias Guedemann | |||||||||||||||||||||||||||||||||||
SWS | 4 | |||||||||||||||||||||||||||||||||||
ECTS | 5 | |||||||||||||||||||||||||||||||||||
Sprache(n) | Deutsch (Standard) Englisch |
|||||||||||||||||||||||||||||||||||
Lehrform | SU mit Praktikum | |||||||||||||||||||||||||||||||||||
Angebot | im Wechsel mit anderen Fächern der gleichen Fachgruppe | |||||||||||||||||||||||||||||||||||
Aufwand | 40 Präsenzstunden Vorlesung, 20 Präsenzstunden Übung, 35 Stunden Vor-/Nachbereitung der Übungen, 55 Stunden Nachbereitung der Vorlesung und Prüfungsvorbereitung |
|||||||||||||||||||||||||||||||||||
Voraussetzungen | Keine |
|||||||||||||||||||||||||||||||||||
Ziele | Der Studierende ist in der Lage
|
|||||||||||||||||||||||||||||||||||
Inhalt | Für Systeme, deren Versagen menschliches Leben, die Gesundheit oder sehr hohe Vermögenswerte gefährdet (sicherheitskritische Systeme), ist das Vertrauen auf erfolgreiche Tests nicht ausreichend. Verifikation ist der mathematische Beweis, dass ein System gewisse für seine Sicherheit wesentliche Eigenschaften besitzt - vorausgesetzt Programmeigenschaften werden formal spezifiziert. Auf einer gemeinsamen theoretischen Basis werden sowohl die klassische Programmverifikation als auch das sogenannte »Model Checking« betrachtet. Die "Abstrakte Interpretation" wird als gut handhabbareTechnik approximativer Verifikation ergänzt. Im Einzelnen
|
|||||||||||||||||||||||||||||||||||
Medien und Methoden | Tafel, Folien oder Beamer |
|||||||||||||||||||||||||||||||||||
Literatur | Apt/Olderog; Verification of Sequential and Concurrent Programs; Springer, 1997 Loeckx/Sieber; The Foundations of Program Verification; Teubner; 1987 Müller, Peter; Modular Specification and Verification of Object-Oriented Programs; Springer; 2002 ISBN 3-540-00296-0 Schneider; Verification of Reactive Systems; Springer; 2004; ISBN 0-521-54310 X Huth/Ryan; Logic in Computer Science CACM Computing Surveys, Special Issue on Software Verification, Vol.41 No. 4, 2009 |
|||||||||||||||||||||||||||||||||||
Zuordnungen Curricula |
|