40 Präsenzstunden Vorlesung, 20 Präsenzstunden Übung, 35 Stunden Vor-/Nachbereitung der Übungen, 55 Stunden Nachbereitung der Vorlesung und Prüfungsvorbereitung

Keine

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.

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

Tafel, Folien oder Beamer

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