Mit
der formalen Spezifikation werden (perspektivisch) vor allem zwei Zielvorstellungen
verbunden: - Erbringen des Beweises, daß eine formulierte Spezifikation bestimmten
Anforderungen tatsächlich gerecht wird. - Nutzung der formalen Spezifikation als
Ausgangspunkt für die Generierung einer lauffähigen Software-Version. Das erste Ziel
(Validation) ist gegenwärtig nur in sehr kleinen Teilbereichen erreichbar, und dies auch nur mit
ganz erheblichem Aufwand. Beim zweiten Ziel stehen die Chanchen etwas besser: Für
bestimmte Aufgaben ist durchaus die Erzeugung von lauff-higem Code aus einer Spezifikation
heraus möglich. Dieses Vorgehen wird auch als Rapid Prototyping bezeichnet. Erzeugt wird ein
Software-Prototyp, der meist nur einige wesentliche, aber nicht alle geforderten Eigenschaften
des Endprodukts aufweist. Experimente mit dem Prototyp ermöglichen es - im
Zusammenwirken mit den künftigen Nutzern des Software-Produkts - frühzeitig
Spezifikationsfehler aufzudecken. Forbrig [Forb 90] schlägt den folgenden, in der Zukunft
anzustrebenden, Lebenszyklus vor:
+----------------+ verbale
| ANALYSIEREN |<--------Aufgabenstellung
+----------------+
|
|
+----------------+ +--------------+
|
|
|
|
formale Spezifikation --------------------
|
|
|
+----------------+
|--------------------| IMPLEMENTIEREN | (automatische Synthese)
|
+----------------+
|
|
|
Programm
|
|
|
+----------------+
|
| TESTEN |
|
+----------------+
|
|
| +----------------+ |
|<---| WARTEN |<--- Softwareprodukt
| +----------------+
|
WISSENSBASIS
-----------------------------------------------------
|
|
|
+----------------+ +----------------+ +----------------+
| Beschreibung | | vorgefertigte | |
Methoden- |
| vorgefertigter | | Bausteine | |
wissen |
| Bausteine | |
| |
|
+----------------+ +----------------+ +----------------+
Der
Ansatz setzt auf die Verwendung vorgefertigter Software-Bausteine, die entsprechend der
speziellen Anforderungen wissensgestützt ausgewählt und verknüpft werden. Voraus- setzung
ist natürlich, das nicht nur die Software-Bausteine vorhanden sind, sondern auch die zu ihnen
gehörende formale Spezifikation.
[HoPi
89]
Die formale Spezifikation größerer Softwareprodukte wird sich wahrscheinlich auf
Basissoftware und Software, die hohe Sicherheitsanforderungen erfüllen muß, konzentrieren.
Dazu wird sich im Proze+ der Arbeitsteilung der Spezialist für formale Spezifikation, der in den
entsprechenden theoretischen Grundlagen ausgebildet und in den Spezifikationstechniken
geschult werden mu+, herausbilden. Bei der Spezifikation von Anwendersoftware wird
erwartet, daß wissensbasierte Methoden und Rapid Prototyping in die ingenieurmäßige Praxis
Einzug halten.
[BrLM
85]
Bei der Programmverifikation sind zwei Zielrichtungen zu unterscheiden: 1) Prüfung, ob das
Verhalten des Programms mit seiner Spezifikation vertr-glich ist, 2) Prüfung, ob das Programm
endet. Die Durchführung des Beweises der Verifikationsbedingungen für ein Programm
erfordert in der Regel grö+ere Anstrengungen als die Programmierung selbst.
1. 6. Die Phasen im Software-Lebe...
