Eine "formale Verifikation" ist eine "Verifikation" mit formalen, d. h. mathematisch exakten Mitteln. Eine "Verifikation" ist eine Nachweisführung, bei der gezeigt wird, daß ein Produkt einer Entwicklungsaktivität die Anforderungen erfüllt, die während vorhergehender Aktivitäten aufgestellt wurden. Handelt es sich bei dem Produkt um eine Spezifikation, für die formale Verifikation durchgeführt wird, spricht man von "Designverifikation". Die Methoden unterscheiden sich im Zeitpunkt der Nachweisführung
Nachfolgend werden Kriterien zur Auswahl von Einzelmethoden aufgeführt:
Die Methodenkategorie Designverifikation kann nach dem Zeitpunkt der Nachweisführung in
unterschieden werden. Im Rahmen der Einzelbeschreibungen werden diese Methoden vorgestellt. Zur leichteren Abgrenzung der Einzelmethoden werden die Einzelmethoden zunächst im Vergleich gegenübergestellt.
Die Zielsetzung der DVER-Einzelmethoden ist identisch. Sie unterscheiden sich lediglich darin, wann der Nachweis für die Korrektheit erbracht wird. Bei der "klassischen Designverifikation" wird dies erst nach der Fertigstellung der verfeinerten Spezifikation gemacht. "Verification while Development" beweist jeden Verfeinerungsschritt sofort. Mit der "formalen Transformation" wird eine Spezifikation durch Transformationsregeln in die Zielspezifikation transformiert. Die Korrektheit der Transformationsregeln ist dabei bereits vor der Transformation mathematisch bewiesen.
Existiert bereits eine verfeinerte informelle Spezifikatikon, ist die "klassische Designverifikation" zu bevorzugen, da die Entwicklungsschritte nicht nochmals nachvollzogen werden müssen. Kann der Beweis der Verfeinerung bei dieser Methode aber nicht erbracht werden oder stellt sich heraus, daß es keine Verfeinerung ist, ist es oft schwierig, den Fehler zu lokalisieren und zu beheben. Bei der "formalen Transformation" und "Verification while Development" dagegen wird jeder Entwicklungsschritt sofort bewiesen. Ein eventueller Fehler ist also leicht behebbar, aber es ist eventuell schwierig, die Entwurfsentscheidungen einer bereits existierenden informellen Spezifikation hier nochmals nachzuvollziehen. Die Beweisverpflichtungen bei der "formalen Transformation" sind am geringsten, da die Beweise bereits verallgemeinert bewiesen worden sind. Es ist auf der anderen Seite aber schwierig, eine für den Verfeinerungsschritt benötigte, vollständige Menge von Transformationsregeln bereitzustellen.
Tabelle 5.2: DVER: Unterschiede der Einzelmethoden
1 Identifikation/Definition der Methode
/ Baader, 90 / Abschnitt II und III, jeweils Kapitel 2.3
2 Kurzcharakteristik der Methode
In der "klassischen Designverifikation" wird bewiesen, daß eine Spezifikation eine Verfeinerung einer anderen ist. Der Beweis wird erst geführt, nachdem die Verfeinerung fertiggestellt wurde.
3 Anwendung der Methode im V-Modell
Die "klassische Designverifikation" kann im V-Modell zur Selbstprüfung in SE eingesetzt werden. Da der Beweis von dem Team, das die Spezifikation verfeinert hat, durchgeführt werden sollte, ist es nicht sinnvoll, diese Methode QS zuzuordnen.
4 Schnittstellen
Es gibt eine Schnittstelle zur Methodenkategorie FS . Die "klassische Designverifikation" muß auf die verwendete formale Spezifikationssprache abgestimmt sein.
5 Weitere Hinweise
- entfällt -
6 Literatur
/ Baader, 90 / Grundlagen der formalen Methoden und Bestandsaufnahme von Werkzeugen und Konzepten
/ 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 Workshop 1989, hauptsächlich betreffend Z
1 Identifikation/Definition der Methode
/ Brix, 86 /
"Verification while Development" kann als ein Spezialfall der "klassischen Designverifikation" angesehen werden. Jeder Designschritt (auch dies ist bereits eine Verfeinerung einer Spezifikation) wird sofort bewiesen.
2 Kurzcharakteristik der Methode
Jeder Designschritt wird bewiesen, bevor der nächste Designschritt vorgenommen wird. Besteht eine Verfeinerung einer Spezifikation nur aus einem Designschritt, so ist diese Methode identisch mit der "klassischen Designverifikation". Nach dem letzten Designschritt erhält man die gewünschte formale Spezifikation.
3 Anwendung der Methode im V-Modell
"Verification while Development" kann im V-Modell zur Selbstprüfung in SE eingesetzt werden. Da der Beweis von dem Team, das die Spezifikation verfeinert hat, durchgeführt werden muß, kann diese Methode nur SE zugeordnet werden.
4 Schnittstellen
Es gibt eine Schnittstelle zur Methodenkategorie FS . "Verification while Development" muß auf die verwendete formale Spezifikationssprache abgestimmt sein.
5 Weitere Hinweise
- entfällt -
6 Literatur
/ Brix, 86 / Grundlagen der "Programmverification while Development" werden hier am Beispiel des Siemens Verifikationstools CARTESIANA aufgeführt
/ 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 Workshop 1989, hauptsächlich betreffend Z
1 Identifikation/Definition der Methode
/ Baader, 90 / Abschnitt II und III, jeweils Kapitel 2.4
2 Kurzcharakteristik der Methode
Bei der "formalen Transformation"" wird eine Spezifikation nach vorgegebenen, mathematisch bewiesenen Transformationsregeln solange umgewandelt, bis man das gewünschte Ergebnis erreicht hat. Sind die Transformationsregeln nur unter bestimmten Bedingungen gültig, muß noch bewiesen werden, daß die Transformationsregel angewendet werden darf.
Da die Transformationsregeln als korrekt bewiesen sind, ist das Ergebnis ebenfalls korrekt.
3 Anwendung der Methode im V-Modell
Da die Entwicklung und der Beweis zusammen erfolgen, muß diese Methode SE zugeordnet werden.
4 Schnittstellen
Es gibt eine Schnittstelle zur Methodenkategorie FS . Die "Formale Transformation" muß auf die verwendete formale Spezifikationssprache abgestimmt sein.
5 Weitere Hinweise
- entfällt -
6 Literatur
/ Baader, 90 / Grundlagen der formalen Methoden und Bestandsaufnahme von Werkzeugen und Konzepten
/ 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 Workshop 1989, hauptsächlich betreffend Z