Previous Next Methods Allocation  
4.10 Methodenkategorie "Designverifikation" (DVER)  

  4.10 Category of Methods "Design Verification" (DVER)

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 Designverifikation (DVER) handelt es sich um eine Methodenkategorie. Die einzelnen anwendbaren Methoden (formale Verifikationsverfahren) werden in Anlage 1 unter Angabe von Auswahlkriterien genauer erläutert. Erst im Rahmen der Operationalisierung wird eine spezifische Methode festgelegt.

    Bei der Designverifikation wird mit den Mitteln der formalen Logik nachgewiesen, daß eine formale Spezifikation (Feinspezifikation) die Verfeinerung einer Ausgangsspezifikation ist und alle Anforderungen an die Ausgangsspezifikation ebenfalls erfüllt.

    2 Kurzcharakteristik der Methode

    Ziel und Zweck

    Eine Spezifikation wird durch Detaillierung und Konkretisierung der Aussagen und Bedingungen verfeinert. Ziel der Designverifikation ist es, mathematisch exakt nachzuweisen, daß die verfeinerte Spezifikation die Aussagen der Ausgangsspezifikation weiterhin erfüllt.

    Die Designverifikation wird auch für die Beweise des formalen Sicherheitsmodells benötigt.

    Darstellungsmittel

    Die Darstellungsmittel entsprechen der Formalen Spezifikation. Zusätzlich müssen Regeln für die Beweisschritte angegeben werden.

    Funktioneller Ablauf

    Es gibt drei verschiedene Vorgehensweisen zur formalen Designverifikation: - Bei der "klassischen Designverifikation" wird mit dem Nachweis begonnen, wenn die Verfeinerung einer Ausgangsspezifikation abgeschlossen ist. There are three different procedures to do the formal Design Verification (DVER):

    3 Grenzen des Methodeneinsatzes

    Es sind nicht immer alle gewünschten Eigenschaften einer Spezifikation beweisbar (z. B. Vollständigkeit, Terminierung).

    Designverifikation ist i. a. nicht vollautomatisch möglich. Die Verifikationsbedingungen sollten automatisch generiert werden. Automatisch generierte Verifikationsbedingungen sind aber meist sehr lang und somit von Hand oft schwierig zu beweisen. Designverifikation ohne Werkzeuge ist daher fehleranfällig.

    Für die Durchführung der Designverifikation ist eine fundierte, mathematische Ausbildung notwendig. Für die nicht voll automatisierbaren Teile der Beweise wird viel Erfahrung benötigt. Die Verfeinerung sollte entweder von dem Team durchgeführt werden, das den Beweis durchführen soll, oder zumindest in einer Form erfolgen, die die Verifikation unterstützt.

    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 SE2.5
    Schnittstellen beschreiben
    ,

    SE4.1
    SW-Architektur entwerfen
    ,

    SE4.2
    SW-interne und
    -externe Schnittstellen
    entwerfen

    Wenn in vorhergehenden Aktivitäten (z. B. in Aktivität SE 2.2) eine formale Spezifikation erstellt wurde, wird nachgewiesen, daß die in dieser Aktivität erstellte formale Spezifikation (z. B. der Schnittstellen oder der SW-Architektur) der Vorgabe (z. B. formales Sicherheitsmodell aus Aktivität SE 2) entspricht. Falls innerhalb der Aktivität weitere Verfeinerungen formal durchgeführt werden, wird nachgewiesen, daß diese konsistent sind.

    In der Aktivität SE2.5 - Schnittstellen beschreiben, Könte DVER unterstützen bei der Prüfung von Schnittstellenbeschreibung.Beschreibung der Schnittstellen.

    In der Aktivität SE4.1 - SW-Architektur entwerfen, Könte DVER unterstützen bei der Generierung von SW-Architektur.Einzelbeschreibungen and SW-Architektur.Dynamisches Ablaufmodell.

    In der Aktivität SE4.2 - SW-interne und -externe Schnittstellen entwerfen, Könte DVER unterstützen bei der Prüfung von Schnittstellenbeschreibung.Beschreibung der Schnittstellen.

    4.2 SE5.1
    SW-Komponente/-Modul/
    Datenbank beschreiben
    Es wird nachgewiesen, daß die formale Spezifikation des Feinentwurfs der SW-Architektur entsprechend und, falls weitere Verfeinerungen durchgeführt werden, daß diese ebenfalls korrekt sind.

    In der Aktivität SE5.1 - SW-Komponente/-Modul/Datenbank beschreiben, Könte DVER unterstützen bei der Prüfung von SW-Entwurf (Modul).SW-Komponenten-/SW-Modul-Beschreibung, Datenkatalog.Datenbeschreibung and Datenkatalog.Datenrealisierung.

    5 Schnittstellen

    Nr. Schnittstellen Bemerkung Information (Anhang 1)
    5.1 DVER-FS Die Methode DVER setzt voraus, daß die zu verifizierende Feinspezifikation und die Ausgangsspezifikation formal spezifiziert sind. Idealerweise sollten diese Spezifikationen in derselben formalen Spezifikationssprache beschrieben sein. 4.8 Schnittstellen DVER-FS

    6 Weiterführende Literatur

    /Brock, 1990/ RAISE METHOD
    /Jones, 1990/ Systematic Software Development using VDM
    /Kersten, 1990/ Sichere Software (Formale Spezifikation und Verifikation vertrauenswürdiger Systeme)
    /Nicholls, 1990/ Z User Workshop

    7 Funktionale Werkzeuganforderungen

    LSE30 - Formal verifizieren

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