4.32 Methodenkategorie "Programmverifikation" (PVER)

  4.32 Method Cathegory "Program Verification" (PVER)

Inhalt		1 Identifikation/Definition der Methode 2 Kurzcharakteristik der Methode 3 Grenzen des Methodeneinsatzes 4 Detaillierung der Methodenzuordnung 5 Schnittstellen 6 Weiterführende Literatur 7 Funktionale Werkzeuganforderungen

1 Identifikation/Definition der Methode

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

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:

• Bei der "klassischen Programmverifikation" wird mit dem Nachweis begonnen, wenn der Code einer zu verifizierenden Einheit erstellt ist. Im allgemeinen wird dann zu jeder Aussage der Spezifikation entweder ausgehend von der Vorbedingung die "stärkste Nachbedingung" oder ausgehend von der Nachbedingung die "schwächste Vorbedingung" gesucht.
• Bei "Verification during Development" wird sofort verifiziert, wenn eine Aussage der Spezifikation kodiert wurde. Entsprechend der "klassischen Programmverifikation" werden stärkste Nachbedingungen oder schwächste Vorbedingungen gesucht.
• Die "formale Transformation" ist eine Umwandlung der Spezifikation nach vorgegebenen Regeln und der Nachweis, daß die Bedingungen erfüllt sind, unter denen die Regeln gültig sind. Für die Transformationsregeln muß nachgewiesen sein, daß sie nur zu korrekten Programmkonstrukten führen.

3 Grenzen des Methodeneinsatzes

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

5 Schnittstellen

6 6 Weiterführende Literatur

7 Funktionale Werkzeuganforderungen

This page online  •  GDPA Online  •  Last Updated 08.Oct.2002 by C. Freericks