Previous Next Methods Allocation  
4.19 Methodenkategorie "Formale Spezifikation" (FS)  

  4.19 Method Category "Formal Specification" (FS)

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

    Eine Formale Spezifikation ist eine in einer formalen Notation geschriebene Spezifikation. Diese Notation baut auf wohl begründeten mathematischen Konzepten auf. Diese Konzepte werden dazu benutzt, um die Syntax und Semantik der Notation und die Prüfregeln zu definieren, die das logische Schließen unterstützen. Formale Spezifikationen müssen aus einer Menge von Axiomen abgeleitet werden können. Die Gültigkeit von Eigenschaften, wie z. B. die Erzeugung einer gültigen Aussage, muß gezeigt werden können (siehe /ITSEC/, 2.76).

    2 Kurzcharakteristik der Methode

    Ziel und Zweck

    Eine Formale Spezifikation stellt ein formales Modell eines Systemteils dar. Dieses Modell kann im allgemeinen auf mehrere Arten implementiert werden. Durch hierarchische Verfeinerung wird die Menge der möglichen Implementierungen eingeschränkt, z. B. durch Präzisieren gültiger Zustände des Systems oder durch Einführung von Zwischenzuständen.

    Eine Formale Spezifikation wird auch für die Beschreibung des formalen Modells benötigt.

    Eingangsinformation ist eine nicht-formale Anforderungsbeschreibung bzw. ein nicht-formaler Entwurf und - wenn bereits vorhanden - eine formale Spezifikation aus der der Verfeinerung vorausgehenden Aktivität. Die nicht-formale Anforderungsbeschreibung ist auch im Hinblick auf die Kommunikation zwischen Entwickler und Nutzer bzw. Anwender unverzichtbar.

    Darstellungsmittel

    Darstellungsmittel der Formalen Spezifikation ist eine formale Notation, die auf einem Kalkül der formalen Logik basiert. Welche Art von Kalkül am geeignetsten ist, ist abhängig von der Art der Anforderungen, deren Erfüllung nachzuweisen ist. Die wichtigsten Klassen formaler Spezifikationen sind:

    Funktioneller Ablauf

    Ausgangspunkt einer formalen Spezifikation sind Angaben über die Funktionen und die geforderten Merkmale des zu realisierenden Produkts in nicht formaler Darstellung. Aus den funktionalen Anforderungen und den davon abgeleiteten Abläufen werden gültige Zustände, Zustandsübergänge, Invarianten und/oder Vor- und Nachbedingungen der einzelnen Operationen abgeleitet und festgelegt. Idealerweise können alle, üblicherweise aber nur ein Teil der Anforderungen formal dargestellt werden.

    Diese Formale Spezifikation wird weiter verfeinert. Grundlage für die Verfeinerung ist die Formale Spezifikation der vorausgehenden Detaillierungsstufe sowie die verfeinerte nicht-formale Spezifikation. Verallgemeinert läuft die Detaillierung einer Spezifikation nach folgendem Schema ab:

    Abbildung FS.1
    Abbildung FS.1: Verfeinerung formaler Spezifikationen

    Wenn durch die Spezifikation die innere Konsistenz eines Entwurfs nachgewiesen werden soll, ist eine Spezifikationsebene evtl. ausreichend. Sonst kann die Formale Spezifikation über mehrere Detaillierungsebenen bis zur Programmiervorgabe verfeinert werden. Ein Übergang auf eine andere Spezifikationsmethode ist nur sinnvoll, wenn die für die Spezifikationen verwendeten Methoden untereinander verträglich sind.

    3 Grenzen des Methodeneinsatzes

    Um Formale Spezifikationen zu erstellen und zu prüfen, sind fundierte mathematische Kenntnisse der Entwickler und der QS notwendig. Syntaxprüfung und statische Semantikprüfung sollten durch Werkzeuge unterstützt werden.

    Um Formale Spezifikationen zu verstehen und weiterzuverarbeiten, ist eine gezielte Ausbildung erforderlich (z. B. Ausbildung für die Programmierer).

    Am meisten verbreitet sind die mathematische, axiomatische und algorithmische Spezifikation. Mit unterschiedlichen formalen Spezifikationsmethoden können verschiedene Aspekte eines Entwurfs dargestellt werden. Hierarchische Verfeinerungen sollten beim heutigen Stand der Technik in einer Spezifikationsmethode durchgeführt werden, da ein Wechsel zu einer anderen Methode im allgemeinen zu Schnittstellenproblemen führt und eine formale Verifikation erschwert.

    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
    Anhand der formalen Vorgaben der Systemarchitektur werden kritische Schnittstellen ausgewählt und präzise und vollständig spezifiziert.

    Die Darstellung ergänzt die informelle Schnittstellenbeschreibung.Beschreibung der Schnittstellen.

    4.2 SE4.1
    SW-Architektur
    entwerfen
    Innerhalb dieser Aktivität wird mit der Methode FS das Zusammenwirken der Prozesse ausgedrückt. Wenn in Aktivität SE 2.2 kein formales Modell erstellt wurde, ist Aktivität SE 4.1-SW ein geeigneter Einstiegspunkt, die Anforderungen zu formalisieren.

    Ferner wird mit der Methode FS das Zusammenwirken der SW-Komponenten, SW-Module und Datenbanken ausgedrückt und mit FS formal definiert (SW-Architektur.Einzelbeschreibungen, SW-Architektur.Dynamisches Ablaufmodell).

    Die Darstellung ergänzt den nicht-formalen Grobentwurf.

    4.3 SE4.2
    SW-interne und -externe
    Schnittstellen entwerfen
    Anhand der formalen Vorgaben der SW-Architektur werden kritische Schnittstellen ausgewählt und präzise und vollständig spezifiziert.

    Die Darstellung ergänzt die nicht-formale Schnittstellenbeschreibung.Beschreibung der Schnittstellen.

    4.4 SE5.1
    SW-Komponente/
    -Modul/Datenbank
    beschreiben
    Die Darstellung ist eine hierarchische Verfeinerung der Spezifikation aus Aktivität SE 4.1-SW, die die Ergebnisse der nicht formalen Entwurfsverfeinerung berücksichtigt.

    Die Darstellung ergänzt den nicht-formalen Feinentwurf.

    FS könte unterstützen bei der generierung von SW-Entwurf (Modul).SW-Komponenten-/SW-Modul-Beschreibung, Datenkatalog.Datenbeschreibung and Datenkatalog.Datenrealisierung.

    5 Schnittstellen

    Nr. Schnittstellen Bemerkung Information (Anhang 1)
    5.1 FS-DVER Eine Formale Spezifikation (FS) ist Voraussetzung für Designverifikation (DVER). 4.8 Interface DVER-FS
    5.2 FS-PVER Eine Formale Spezifikation (FS) ist Voraussetzung für Programmverifikation (PVER). 4.13 Schnittstelle FS-PVER
    5.3 FS-AVK Eine formale Spezifikation (FS) ist Voraussetzung für Analyse verdeckter Kanäle (AVK), falls diese formal erfolgen soll. 4.1 Schnittstelle ACC-FS

    6 Weiterführende Literatur

    /Baader, 1990/ Methoden zur formalen Spezifikation und Verifikation von Software
    /Björner, 1990/ VDM '90: VDM and Z. Formal Methods in Software Development
    /Gehani, 1986/ Software Specification Techniques
    /Hayes, 1987/ Specification Case Studies
    /Jones, 1990/ Systematic Software Development using VDM
    /Kersten, 1990/ Sichere Software (Formale Spezifikation und Verifikation vertrauenswürdiger Systeme)
    /Kröger, 1987/ Temporal Logic of Programs

    7 Funktionale Werkzeuganforderungen

    SSD29 - Formal Specification

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