Previous Next Methods Allocation  
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 (PVER) handelt es sich um eine Methodenkategorie. Die einzelnen anwendbaren formalen Verifikationsverfahren werden in Anlage 1 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

    Nr. Aktivität Beschreibung
    4.1 SE6.1
    SW-Module codieren
    ,

    SE6.2
    Datenbank realisieren

    SE6.3
    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

    Nr. Schnittstellen Bemerkung Information (Anhang 1)
    5.1 PVER-FS Die Methode PVER setzt ein Kalkül voraus, das die Semantik der Programmiersprache in der Spezifikationssprache (Methode FS) beschreibt. 4.13 Schnittstelle FS-PVER

    6 6 Weiterführende Literatur

    /Baader, 1990/ Methoden zur formalen Spezifikation und Verifikation von Software
    /Brix, 1986/ Rechnergestützte Programmkonstruktion und -verifikation mit formalen Regeln
    /Kersten, 1990/ Sichere Software (Formale Spezifikation und Verifikation vertrauenswürdiger Systeme)
    /Kröger, 1987/ Temporal Logic of Programs
    /Loeckx, 1987/ The Foundation of Program Verification

    7 Funktionale Werkzeuganforderungen

    SSD30 - Formal Verification

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