Programmverifikation
Fakultät für Informatik und Mathematik ©
Name Programmverifikation
Verantwortlich Prof. Dr. Ulrich Möncke
SWS 4
ECTS 5
Sprache(n) Deutsch
Lehrform SU mit Übung
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
Ziele

Der Studierende ist in der Lage

  • formalen Verifikationsmethoden zu erläutern.
  • Verifikationsmethoden in kleinen Beispielen »von Hand« anzuwenden
  • den Einsatz und die Voraussetzungen des Einsatzes von formalen Verifikationsmethoden unter Rücksicht auf das Geschäftsfeld abwägend zu beurteilen.
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

  • Grundlagen aus der Logik, Verbände und Fixpunkte
  • Formale Spezifikation von Schnittstellen und Abstrakte Datentypen
  • Axiomatische Verifikation nach Hoare
  • Zustandsübergangssysteme und »Model Checking«
  • Abstrakte Interpretation nach Cousot
  • Begleitung durch Praktikum
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
SPO Fachgruppe Code ab Semester Prüfungsleistungen
IG Version 2010 CGBV: Theoretische Grundlagen IG-TTI-0090 1 benotete schriftliche Prüfung 90 Minuten
IG Version 2010 EC: Theoretische Grundlagen IG-TTI-0090 1 benotete schriftliche Prüfung 90 Minuten
IG Version 2010 SWE: Theoretische Grundlagen IG-TTI-0090 1 benotete schriftliche Prüfung 90 Minuten