Eine "Formale Spezifikation" ist eine Spezifikation in einer formalen Notation, deren Semantik eindeutig (formal) definiert ist.
Nachfolgend werden Kriterien zur Auswahl von Einzelmethoden aufgeführt.
Die Methodenkategorie FS kann 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 FS-Einzelmethoden ist identisch. Man verzichtet auf eine leicht verständliche Sprache (wie bei der informellen Spezifikation) und erreicht durch die formale Sprache eine Eindeutigkeit in der Aussage (Beispiel für eine Mehrdeutigkeit in natürlicher Sprache: "He likes her cooking").
Tabelle 5.3: FS: Unterschiede der Einzelmethoden
1 Identifikation/Definition der Methode
/ Baader, 90 / Abschnitt II, Kapitel 1.2 (hier: "operationelle Spezifikation")
2 Kurzcharakteristik der Methode
Die mathematische Spezifikation ist eine formale Spezifikation, die das Verhalten von Operationen durch die Beschreibung der Vor- und Nachbedingungen spezifiziert.
Die Nachbedingung beschreibt die Zustände, die nach Ausführung der Operation erreicht werden dürfen, wenn vor der Ausführung die Vorbedingung gültig war.
3 Anwendung der Methode im V-Modell
Die mathematische Spezifikation kann zur Beschreibung von Operationen auf allen Abstraktions-ebenen eingesetzt werden.
4 Schnittstellen
Es gibt Schnittstellen zu den Methoden DVER , PVER und AVK .
5 Weitere Hinweise
- entfällt -
6 Literatur
/ Baader, 90 / Grundlagen der formalen Methoden und Bestandsaufnahme von Werkzeugen und Konzepten
/ Björner, 90 / Tagungsband der Konferenz VDM '90; Schwerpunkt sind aktuelle Themen bezüglich der formalen Spezifikationssprachen VDM und Z
/ Gehani, 86 / enthält mehrere Artikel zur formalen Spezifikation. Diskutiert werden Prinzipien und Eigenschaften einer guten Spezifikation, verschiedene Spezifikationsmethoden, Verwendung formaler Spezifikationstechniken in der Praxis
/ Hayes, 87 / Spezifikationen in Z
/ Jones, 90 / beschreibt VDM und seine Grundlagen
/ Kersten, 90 / mehrere Beiträge zum Thema "Formale Spezifikation und Verifikation"
/ Kröger, 87 / behandelt temporale Logik und Verifikation von Aussagen in temporaler Logik
1 Identifikation/Definition der Methode
/ Baader, 90 / Abschnitt II, Kapitel 1.2
2 Kurzcharakteristik der Methode
Die axiomatische Spezifikation ist eine formale Spezifikation, die die Semantik der Funktionen und Objekte durch eine Beschreibung der Beziehungen zwischen verschiedenen Objekten und Funktionen definiert. Die Beschreibung erfolgt durch Axiome (prädikatenlogische Formeln).
Bei algebraischen Spezifikationen werden Funktionen in Form einer Algebra beschrieben. Eine Algebra besteht aus Signatur und den Axiomen. Die Signatur wiederum besteht aus einer Familie von Objektmengen (Trägermengen) und einer Anzahl von Operationen auf diesen Trägermengen mit ihrer Funktionalität. Die Axiome beschreiben die Eigenschaften dieser Operationen durch algebraische Gleichungen.
3 Anwendung der Methode im V-Modell
Die axiomatische Spezifikation kann zur Beschreibung von Operationen auf allen Abstraktionsebenen eingesetzt werden. Sie ist aber insbesondere für die ersten Phasen geeignet (z. B. auch für das formale Sicherheitsmodell).
4 Schnittstellen
Es gibt Schnittstellen zu den Methoden DVER , PVER und AVK .
5 Weitere Hinweise
- entfällt -
6 Literatur
/ Baader, 90 / Grundlagen der formalen Methoden und Bestandsaufnahme von Werkzeugen und Konzepten
/ Björner, 90 / Tagungsband der Konferenz VDM '90; Schwerpunkt sind aktuelle Themen bezüglich der formalen Spezifikationssprachen VDM und Z
/ Gehani, 86 / enthält mehrere Artikel zur formalen Spezifikation. Diskutiert werden Prinzipien und Eigenschaften einer guten Spezifikation, verschiedene Spezifikationsmethoden, Verwendung formaler Spezifikationstechniken in der Praxis
/ Hayes, 87 / Spezifikationen in Z
/ Jones, 90 / beschreibt VDM und seine Grundlagen
/ Kersten, 90 / mehrere Beiträge zum Thema "Formale Spezifikation und Verifikation"
/ Kröger, 87 / behandelt temporale Logik und Verifikation von Aussagen in temporaler Logik
1 Identifikation/Definition der Methode
/ Baader, 90 / Abschnitt II, Kapitel 1.2 (hier: "konstruktive Spezifikation")
2 Kurzcharakteristik der Methode
Die algorithmische Spezifikation ist eine formale Spezifikation, die das Operationsverhalten durch die Angabe einer Berechnungsvorschrift beschreibt. Das Abstraktionsniveau ist also sehr niedrig. Der Vorteil dafür ist, daß die Spezifikation interpretierbar ist. Eine vollständige algorithmische Spezifikation heißt auch funktionales Programm.
3 Anwendung der Methode im V-Modell
Die algorithmische Spezifikation kann zur Beschreibung von Operationen auf allen Abstraktions-ebenen eingesetzt werden. Sie ist aber insbesondere für die letzten Phasen geeignet (z. B. Feinspezifikation).
4 Schnittstellen
Es gibt Schnittstellen zu den Methoden DVER , PVER und AVK .
5 Weitere Hinweise
- entfällt -
6 Literatur
/ Baader, 90 / Grundlagen der formalen Methoden und Bestandsaufnahme von Werkzeugen und Konzepten
/ Björner, 90 / Tagungsband der Konferenz VDM '90; Schwerpunkt sind aktuelle Themen bezüglich der formalen Spezifikationssprachen VDM und Z
/ Gehani, 86 / enthält mehrere Artikel zur formalen Spezifikation. Diskutiert werden Prinzipien und Eigenschaften einer guten Spezifikation, verschiedene Spezifikationsmethoden, Verwendung formaler Spezifikationstechniken in der Praxis
/ Hayes, 87 / Spezifikationen in Z
/ Jones, 90 / beschreibt VDM und seine Grundlagen
/ Kersten, 90 / mehrere Beiträge zum Thema "Formale Spezifikation und Verifikation"
/ Kröger, 87 / behandelt temporale Logik und Verifikation von Aussagen in temporaler Logik
1 Identifikation/Definition der Methode
/ Hoare, 85 /
2 Kurzcharakteristik der Methode
Die Spezifikation mittels Traces ist eine formale Spezifikation, die die Abläufe eines Programms beschreibt, das heißt die Reihenfolge verschiedener Zustände oder die Ablaufreihenfolge verschiedener Operationen. Die Spezifikation erfolgt dann über die Eigenschaften dieser Traces.
3 Anwendung der Methode im V-Modell
Die Spezifikation mittels Traces kann zur Beschreibung des Operationsverhaltens auf allen Abstraktionsebenen eingesetzt werden. Auch ist diese Spezifikation ideal für die Beschreibung von Abläufen zusammengesetzter Programme oder Automaten (z. B. Parallelität).
4 Schnittstellen
Es gibt Schnittstellen zu den Methoden DVER , PVER und AVK .
5 Weitere Hinweise
- entfällt -
6 Literatur
/ Baader, 90 / Grundlagen der formalen Methoden und Bestandsaufnahme von Werkzeugen und Konzepten
/ Björner, 90 / Tagungsband der Konferenz VDM '90; Schwerpunkt sind aktuelle Themen bezüglich der formalen Spezifikationssprachen VDM und Z
/ Gehani, 86 / enthält mehrere Artikel zur formalen Spezifikation. Diskutiert werden Prinzipien und Eigenschaften einer guten Spezifikation, verschiedene Spezifikationsmethoden, Verwendung formaler Spezifikationstechniken in der Praxis
/ Hayes, 87 / Spezifikationen in Z
/ Hoare, 85 / beschreibt CSP, eine formale Spezifikationssprache mittels Traces zur Beschreibung paralleler Prozesse
/ Jones, 90 / beschreibt VDM und seine Grundlagen
/ Kersten, 90 / mehrere Beiträge zum Thema "Formale Spezifikation und Verifikation"
/ Kröger, 87 / behandelt temporale Logik und Verifikation von Aussagen in temporaler Logik
1 Identifikation/Definition der Methode
/ Kröger, 87 / Kapitel 4
2 Kurzcharakteristik der Methode
Die Spezifikation mittels temporaler Logik ist eine formale Spezifikation, die Programme mittels temporaler Logik beschreibt. Temporale Logik behandelt Aussagen, die von der Zeit abhängen. Mit der temporalen Logik können dann Aussagen über bestimmte Programmzustände, aber auch über den Programmablauf gemacht werden. Jeder Zustand entspricht einem diskreten Zeitpunkt.
3 Anwendung der Methode im V-Modell
Die Spezifikation mittels temporaler Logik kann zur Beschreibung des Operationsverhaltens auf allen Abstraktionsebenen eingesetzt werden. Auch ist diese Spezifikation ideal für die Beschreibung von zeitlichen Zusammenhängen von Programmen.
4 Schnittstellen
Es gibt Schnittstellen zu den Methoden DVER , PVER und AVK .
5 Weitere Hinweise
- entfällt -
6 Literatur
/ Baader, 90 / Grundlagen der formalen Methoden und Bestandsaufnahme von Werkzeugen und Konzepten
/ Björner, 90 / Tagungsband der Konferenz VDM '90; Schwerpunkt sind aktuelle Themen bezüglich der formalen Spezifikationssprachen VDM und Z
/ Gehani, 86 / enthält mehrere Artikel zur formalen Spezifikation. Diskutiert werden Prinzipien und Eigenschaften einer guten Spezifikation, verschiedene Spezifikationsmethoden, Verwendung formaler Spezifikationstechniken in der Praxis
/ Hayes, 87 / Spezifikationen in Z
/ Jones, 90 / beschreibt VDM und seine Grundlagen
/ Kersten, 90 / mehrere Beiträge zum Thema "Formale Spezifikation und Verifikation"
/ Kröger, 87 / behandelt temporale Logik und Verifikation von Aussagen in temporaler Logik