1 Identifikation/Definition der Methode
Bei der Programmverifikation (PVER) handelt es sich um eine Methodenkategorie. Die einzelnen anwendbaren formalen Verifikationsverfahren werden in Anlage 1 (PVER) unter Angabe von Auswahlkriterien genauer erläutert. Erst im Rahmen der Operationalisierung wird eine spezifische Methode festgelegt.
Bei der Programmverifikation wird mit den Mitteln der formalen Logik nachgewiesen, daß ein Programm die Verfeinerung einer Spezifikation ist und alle Anforderungen erfüllt, die diese übergeordnete Spezifikation erfüllt.
2 Kurzcharakteristik der Methode
Ziel und Zweck
Die Programmverifikation dient dazu, mathematisch exakt nachzuweisen, daß der Programmcode eine korrekte Implementierung der Spezifikation ist.
Darstellungsmittel
Auf der Seite der Spezifikation werden die Darstellungsmittel eingesetzt, die bei der Methode FS beschrieben sind. Auf Programmseite wird eine Programmiersprache verwendet. Die Semantik der Programmiersprachenkonstrukte muß formal beschrieben sein. Zusätzlich müssen Regeln für die Beweisschritte angegeben werden (z. B. Hoare-Kalkül).
Funktioneller Ablauf
Wie bei der Designverifikation gibt es drei verschiedene Vorgehensweisen zur formalen Programmverifikation:
3 Grenzen des Methodeneinsatzes
Die verwendeten Programmiersprachen sind oft zu umfangreich und zu unpräzise definiert, um die Semantik aller ihrer Konstrukte durch formale Regeln definieren zu können. Für etliche Konstrukte heutiger Sprachen sind keine Regeln bekannt. Das bedeutet, daß, um die Methode PVER durchführen zu können, i. a. die Menge der verwendeten Programmiersprachenkonstrukte eingeschränkt werden muß.
Programmverifikation ist i. a. nicht vollautomatisch möglich. Die Verifikationsbedingungen sollten automatisch generiert werden. Automatisch generierte Verifikationsbedingungen sind aber meist sehr lang und die zugehörigen Beweise sehr umfangreich. Beweise von Hand sind daher oft sehr schwierig und fehleranfällig. Werkzeugunterstützung ist also dringend erforderlich.
Für die Durchführung der Programmverifikation ist eine fundierte, mathematische Ausbildung notwendig. Für die nicht voll automatisierbaren Teile der Beweise (z. B. das Finden der Invarianten) ist viel Erfahrung notwendig. Das Programm sollte entweder von dem Team geschrieben sein, das den Beweis durchführen soll, oder zumindest in einer Form vorliegen, die die Verifikation unterstützt (z. B. Invarianten als Kommentare angegeben).
Unter Beachtung dieser Grenzen bietet sich der IT-Systementwicklung jedoch durch den Einsatz der formalen Methoden eine enorme Chance, qualitativ hochwertigste IT-Systeme zu erstellen.
4 Detaillierung der Methodenzuordnung
4.1 PVER in den Aktivitäten
- SE 6.1-SW "SW-Module codieren",
- SE 6.2-SW "Datenbank realisieren" und
- SE 6.3-SW "Selbstprüfung des
SW-Moduls/der Datenbank durchführen"
Es wird nachgewiesen, daß der Programmcode der formalen Spezifikation entspricht, die als Programmiervorgabe verwendet wurde.
5 Schnittstellen
5.1 Schnittstelle PVER - FS
Die Methode PVER setzt ein Kalkül voraus, das die Semantik der Programmiersprache in der Spezifikationssprache (Methode FS ) beschreibt.
6 Weiterführende Literatur
/
Baader,
90 /,
/
Brix,
86 /,
/
Kersten,
90 /,
/
Kröger,
87 /,
/
Loeckx,
87 /