Vorlesung
Programmverifikation

Prof. Dr. Uwe Petermann
FB IMN HTWK Leipzig 04251 Leipzig (Germany)
uwe@imn.htwk-leipzig.de

Zusammenfassung:

Software ist zum Herzstück vieler technischer Systeme geworden. Dadurch werden Fragen der Zuverlässigkeit technischer Systeme immer mehr zu Fragen der Korrektheit von Software. Spektakuläre Computerpannen der letzten Zeit bestätigen das eindrucksvoll. Weil das durch fehlerhafte Software verursachte Schadensrisiko oftmals unkalkulierbar ist, entsteht ein zunehmender ökonomischer Zwang, korrekte Software zu benutzen. Produzenten, die solche Software herstellen können, werden einen Wettbewerbsvorteil erlangen.

Den derzeit besten Schutz vor Software-Fehlern bieten formale Spezifikation und Verifikation (vgl. Wolfgang Reif, FMG Uni Augsburg: Risikofaktor Software ).

Intelligente Werkzeuge zur Unterstützung dieser Methoden ermöglichen heute deren praktischen Einsatz. Mit Hilfe von Verifikationssystemen kann die Korrektheit eines Programms bezüglich seiner Spezifikation nachgewiesen werden. Erfolgreiche Systeme (z.B. KIV) nutzen Spezifikationssprachen, um hierarchisch strukturierte Softwaresysteme zu beschreiben.

Die Vorlesung behandelt die Methoden der Spezifikation und Verifikation von informationstechnischen Systemen. Die Methoden werden durch Spezifikations- und Verifikationsexperimente, die mit dem Verifikationssystem KIV bearbeitet werden, illustriert.

Dieses Dokument als .pdf-Datei



Uwe Petermann 2006-06-13