 |
 |
 |
|
| 4.10 Methodenkategorie "Designverifikation" (DVER) |
4.10 Category of Methods "Design Verification" (DVER)
1 Identifikation/Definition der Methode
Bei der Designverifikation (DVER) handelt es sich um eine Methodenkategorie. Die einzelnen anwendbaren Methoden (formale Verifikationsverfahren) werden in 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 ZweckEine 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):
- Bei der klassischen Designverifikation wird mit dem Nachweis begonnen, wenn die Verfeinerung einer Ausgangsspezifikation abgeschlossen ist.
- Bei Verifikation during Development wird jeder Verfeinerungsschritt einer Aussage der Ausgangsspezifikation sofort verifiziert.
- Die formale Transformation ist eine Umwandlung der Ausgangsspezifikation nach vorgegebenen Regeln und der Nachweis, daß die Bedingungen erfüllt sind, unter denen die Regeln gültig sind. Für die Transformationsregeln muß mathematisch nachgewiesen sein, daß sie gemäß dem verwendeten logischen Kalkül korrekt sind.
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, | 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
|
|
|
This page online • GDPA Online • Last Updated 08.Oct.2002 by C. Freericks |