1 Charakterisierung der Schnittstelle
Die Schnittstelle entspricht dem Typus "Informationsweitergabe bei sequentieller Abfolge". Die Methodenkategorie DVER dient dem Nachweis, daß eine formale Spezifikation eine Verfeinerung einer anderen formalen Spezifikation ist. Eingang für DVER ist also eine formale Spezifikation, je nach ausgewählter Methode von DVER eventuell auf zwei verschiedenen Ebenen (bei "klassischer Designverifikation" und "Verification while Development"). Abhängig von der ausgewählten Methode aus DVER ist das Ergebnis wiederum eine formale Spezifikation (bei "formaler Transformation") oder das Prüfungsergebnis.
Die Methode FS dient also der Beschreibung des Systems, die Methode DVER dagegen wird für den Nachweis eingesetzt, daß diese Beschreibungen konsistent sind.
2 Beispiel
Die folgende Abbildung 4.10 verdeutlicht den Zusammenhang zwischen Spezifikation auf zwei unterschiedlichen Abstraktionsebenen:
Abbildung 4.10: Hilfsmittel zur Erstellung einer korrekten Verfeinerung
Vgl. Beispiel in FS - PVER in Abschnitt 4.13.
3 Werkzeugunterstützung
Aufgrund der Komple"ität der Methode DVER ist eine Werkzeugunterstützung unbedingt notwendig. Der Beweiser (bzw. die verwendeten Regeln) muß an die ausgewählte Spezifikationssprache angepaßt sein.
Literatur
/ Brock, 90 / Handbuch für die formale Spezifikationssprache RAISE, eine Weiterentwicklung der formalen Spezifikationssprache VDM, erweitert um algebraische Spezifikationsmöglichkeiten und Parallelität
/ Jones, 90 / Beschreibt VDM und seine Grundlagen.
/ Kersten, 90 / Mehrere Beiträge zum Thema "Formale Spezifikation und Verifikation"
/ Nicholls, 90 / Beiträge auf dem Z User Worshop 1989, hauptsächlich betreffend Z