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 (DVER) 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:
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
4.1 DVER in den Aktivitäten
- SE 2.5 "Schnittstellen
beschreiben",
- SE 4.1-SW "SW-Architektur entwerfen" und
- SE 4.2-SW "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.
4.2 DVER in Aktivität SE 5.1-SW "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.
5 Schnittstellen
5.1 Schnittstelle 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.
6 Weiterführende Literatur
/
Brock,
90 /,
/
Jones,
90 /,
/
Kersten,
90 /,
/
Nicholls,
90 /