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 ein Programm, für das die formale Verfikation durchgeführt wird, spricht man von "Programm Verifikation". Die Methoden unterscheiden sich - analog zur Designverifikation - im Zeitpunkt der Nachweisführung.
Nachfolgend werden Kriterien zur Auswahl von Einzelmethoden aufgeführt:
Die Methodenkategorie Programmverifikation kann nach dem Zeitpunkt der Nachweisführung in
unterschieden werden. Im Rahmen der Einzelbeschreibungen werden diese vorgestellt. Zur leichteren Abgrenzung der Einzelmethoden werden die Einzelmethoden zunächst im Vergleich gegenübergestellt.
Die Zielsetzung der PVER-Einzelmethoden ist identisch. Sie unterscheiden sich lediglich darin, wann der Nachweis für die Korrektheit erbracht wird. Bei der "klassischen Programm Verifikation" wird dies erst nach der Fertigstellung des Programms gemacht. "Verification while Development" beweist jeden Verfeinerungsschritt sofort. Mit der "formalen Transformation" wird eine Spezifikation durch Transformationsregeln in das Programm transformiert. Die Korrektheit der Transformationsregeln ist dabei bereits vor der Transformation mathematisch bewiesen.
Bei der "klassischen ProgrammVerifikation" kann das Programm bereits getestet werden, bevor es bewiesen ist. Kann der Beweis der Korrektheit bei der "klassischen Programm Verifikation" nicht erbracht werden oder stellt sich heraus, daß es kein korrektes Programm 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, das Programm zu optimieren. 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 die Implementierung benötigte, vollständige Menge von Transformationsregeln bereitzustellen.
Tabelle 5.4: PVER: Unterschiede der Einzelmethoden
1 Identifikation/Definition der Methode
/ Baader, 90 / Abschnitt II und III, jeweils Kapitel 2.1
2 Kurzcharakteristik der Methode
In der "klassischen Programm Verifikation" wird bewiesen, daß ein Programm eine korrekte Implementierung einer Spezifikation ist. Der Beweis wird erst geführt, nachdem das Programm fertiggestellt ist.
3 Anwendung der Methode im V-Modell
Die "klassische ProgrammVerifikation" kann im V-Modell zur Selbstprüfung in SE eingesetzt werden. Da der Beweis von dem Team, das das Programm erstellt hat, durchgeführt werden sollte, ist es nicht sinnvoll, diese Methode QS zuzuordnen.
4 Schnittstellen
Es gibt eine Schnittstelle zur Methodenkategorie FS. Die "klassische ProgrammVerifikation" muß auf die verwendete formale Spezifikationssprache und die Implementierungssprache abgestimmt sein.
5 Weitere Hinweise
- entfällt -
6 Literatur
/ Baader, 90 / Grundlagen der formalen Methoden und Bestandsaufnahme von Werkzeugen und Konzepten
/ Brix, 86 / Grundlagen der "Programmverifikation while Development" werden hier am Beispiel des Siemens Verifikationstools CARTESIANA aufgeführt.
/ Kersten, 90 / Mehrere Beiträge zum Thema "Formale Spezifikation und Verifikation".
/ Kröger, 87 / Behandelt temporale Logik und Verifikation von Aussagen in temporaler Logik.
/ Loeckx, 87 / Beschreibt den mathematischen Hintergrund zu verschiedenen formalen Verifikationsmethoden (z. B. Floyd Methode, axiomatische Methode von Hoare, Fixpunktinduktion), aufgezeigt an mehreren Beispielen. Diskutiert werden auch Probleme der Korrektheit und Vollständigkeit
1 Identifikation/Definition der Methode
/ Brix, 86 /
2 Kurzcharakteristik der Methode
In "Verification while Development" wird die Spezifikation schrittweise in einen ausführbaren Code verfeinert.
Jeder Designschritt wird bewiesen bevor der nächste Designschritt vorgenommen wird. Nach dem letzten Designschritt erhält man ein fertiges Programm.
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 bis zu einem ausführbaren Code 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 und die Implementierungssprache abgestimmt sein.
5 Weitere Hinweise
- entfällt -
6 Literatur
/ Baader, 90 / Grundlagen der formalen Methoden und Bestandsaufnahme von Werkzeugen und Konzepten
/ Brix, 86 / Grundlagen der "Programmverifikation while Development" werden hier am Beispiel des Siemens Verifikationstools CARTESIANA aufgeführt
/ Kersten, 90 / mehrere Beiträge zum Thema "Formale Spezifikation und Verifikation"
/ Kröger, 87 / behandelt temporale Logik und Verifikation von Aussagen in temporaler Logik
/ Loeckx, 87 / beschreibt den mathematischen Hintergrund zu verschiedenen formalen Verifikationsmethoden (z. B. Floyd Methode, axiomatische Methode von Hoare, Fixpunktinduktion), aufgezeigt an mehreren Beispielen. Diskutiert werden auch Probleme der Korrektheit und Vollständigkeit
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 und die Implementierungssprache abgestimmt sein.
5 Weitere Hinweise
- entfällt -
6 Literatur
/ Baader, 90 / Grundlagen der formalen Methoden und Bestandsaufnahme von Werkzeugen und Konzepten
/ Brix, 86 / Grundlagen der "Programmverifikation while Development" werden hier am Beispiel des Siemens Verifikationstools CARTESIANA aufgeführt
/ Kersten, 90 / mehrere Beiträge zum Thema "Formale Spezifikation und Verifikation"
/ Kröger, 87 / behandelt temporale Logik und Verifikation von Aussagen in temporaler Logik
/ Loeckx, 87 / beschreibt den mathematischen Hintergrund zu verschiedenen formalen Verifikationsmethoden (z. B. Floyd Methode, axiomatische Methode von Hoare, Fixpunktinduktion), aufgezeigt an mehreren Beispielen. Diskutiert werden auch Probleme der Korrektheit und Vollständigkeit