Verifikation nebenläufiger Programme

Basis: Vordiplom
Zielgruppe: Studierende im Hauptstudium

Vorlesung

Übung

Organisatorisches

Downloads

diverse Folien

Übungsaufgaben

Inhalt

Es ist mittlerweile klar, daß die meisten Spezifikations- und Verifikationsmethoden die Grenzen ihrer Anwendbarkeit erreicht haben. Algorithmische Methoden können endliche Systeme nur bis zu einer bestimmten Größe überprüfen, während deduktive Methoden nur für Systeme geringer Komplexität geeignet sind, weil sie von intensiver Benutzerinteraktion abhängig sind. Die einzige Hoffnung, formale Verifikation für Probleme von industrieller Größe einzusetzen, baut auf die Anwendung zweier wichtiger Prinzipien: Kompositionalität und Abstraktion.

Kompositionelle Verifikationsmethoden ermöglichen es, Eigenschaften eines zusammengesetzten Systems aus den Spezifikationen seiner Teile herzuleiten, ohne interne Details der Komponenten zu verwenden. Die zwei Hauptfragen für kompositionelle Verifikationsmethoden sind also:

1. Wie zerlegt man eine globale Spezifikation in Teilspezifikationen der Komponenten?
2. Wie schließt man aus der Erfülltheit der Teilspezifikationen auf die Erfülltheit der globalen Spezifikation?

References