Formale Methoden in der Softwareentwicklung Heute und Morgen

Sergio Montenegro (.)

GMD-FIRST (http://www.first.fhg.de)

(2.0)

In der letzten Zeit wird viel von formalen Methoden in der Softwareentwicklung gesprochen. Meistens können sich die Ingenieure, Software-Entwickler und Projektleiter nur wenig darunter vorstellen. Wenn sie einen Spezialisten fragen, dann wird ihnen das Blaue vom Himmel erzählt. Wenn sie einen Praktiker fragen, der formale Methoden schnell für seine aktuellen Probleme anwenden will, bekommen sie eine Horror-Geschichte zu hören. Selten hat man das Glück, beide Seiten der Medallie zu hören. Dieser Artikel erklärt, was formale Methoden sind, wo sie helfen, wo sie nicht helfen, ihre Vorteile, Nachteile, Anwendung und Alternativen.

Die Rolle der Sicherheit in der Software

Unser tägliches Leben ist geprägt durch Maschinen, denen wir blind unser Leben anvertrauen. So nützlich diese Maschinen auch sind, sie stellen oftmals eine potentielle Gefahr dar und können zu Katastrophen führen, die es ohne sie nicht geben würde. Zum Beispiel : Wir hätten ohne Autos nicht so viele Verkehrsopfer.

Um sich vor diesen Gefahren zu schützen, werden wiederum technische Mittel eingesetzt, die ebenfalls ein Risiko in sich bergen. So sollen z.B. die Ampeln Verkehrsunfälle verhindern; wir vertrauen ihnen blind. Wenn die Ampel grün ist, geht der Fußgänger über die Straße und schaut oftmals weder nach links noch nach rechts. Eine Fehlfunktion der Ampelanlage führt dann sogar zu einer höheren Unfallgefahr, als wenn es keine Ampel geben würde, weil man ohne sie vorsichtiger die Straße überqueren würde. Um einer Fehlfunktion vorzubeugen, wird in jede Ampel eine Sicherheitsvorrichtung eingebaut, die die Sicherheit der Anlage garantieren soll. Für diese Sicherheitsvorrichtung könnte wieder eine Sicherung eingebaut werden, und so weiter. Dadurch kann die Anlage beim Nutzer noch mehr Vertrauen erlangen, und um so schlimmer ist dann eine Fehlfunktion, mit der keiner gerechnet hat. Die Sicherheit kommt nicht aus dem Vertrauen in die Technik, sondern aus Mißtrauen.

In diesen Fällen muß sowohl die primäre Anlage als auch die Sicherheitseinrichtung einen hohen Sicherheitsstandard erfüllen. Die Sicherheit einer Anlage baut auf zwei Aspekten auf:

1. Die Entwicklung war korrekt, so daß das System macht, was es machen soll.

2. Die Laufzeitfehler, Ausfälle und Ausnahmen (z.B. aus der Hardware, Mechanik und/oder Bedienung) werden erkannt und richtig behandelt.

Während die Zuverlässigkeit von einfachen Maschinen sich durch Prüfungen und Tests ermitteln läßt, ist die Beurteilung der Sicherheit von softwaregesteuerten Maschinen mit komplexem Verhalten äußerst schwierig. Hier können Tests nur das Vorhandensein von Fehlern zeigen, nicht aber deren Abwesenheit beweisen. Fehler in Softwarekomponenten können zu den verschiedensten Zeitpunkten im Verlauf des Entwicklungsprozesses entstehen - angefangen bei einer inadäquaten Spezifikation über Fehler im Entwurf bis hin zu Implementierungs- und Integrationsfehlern, alle stellen eine potentielle Gefahr im späteren Betrieb des Systems dar. Es gibt verschiedene Ansätze, um die Zuverlässigkeit von Software zu erhöhen. Einerseits muß man versuchen, Fehler zu vermeiden, andererseits muß man Fehler, die man nicht vermeiden konnte, beseitigen, was voraussetzt, daß man sie bis dahin erkannt hat (z.B. durch Tests). Aber viele Entwicklungsfehler werden unentdeckt bleiben und stellen eine latente Gefahr dar. Mit diesen Fehlern muß man leben (oder sterben) deswegen muß die Steuerung darauf vorbereitet sein, beim Auftreten möglicher Gefahren wie beispielsweise beim Ausfall einer Hardwarekomponente aber auch bei einem Steuerungsfehler selbst, richtig zu reagieren, so daß das System in einem sicheren Zustand verbleibt. Das fehlertolerante Verhalten eines Systems sollte sich auch auf die Software erstrecken z.B. durch Plausibilitätsprüfungen, Timeouts und Software-Redundanz.

Während man Laufzeitfehler durch Redundanz und Fehlertoleranz-Techniken halbwegs in den Griff bekommen hat, bleiben die Entwicklungsfehler ein offenes Problem. Das Einsetzen von formalen (mathematischen) Methoden ist hier eine Hoffnung, bringt aber einen enormen Aufwand mit sich. Eine Alternative ist z.B. die diversitäre Entwicklung. Dabei entwickeln z.B. zwei Teams unabhängig voneinander das gleiche System. Während der Laufzeit laufen beide Versionen gleichzeitig (parallel) und die Ergebnisse werden verglichen, um Fehler zu entdecken. Die diversitäre Entwicklung bringt höhere Kosten mit sich, Spezifikationsfehler bleiben weiterhin unentdeckt und sehr oft ist das Vergleichen der Laufzeit-Ergebnisse schwierig, da ein unterschiedliches Verhalten auch korrekt sein könnte. Außerdem impliziert das Erkennen eines Steuerungsfehlers noch lange nicht Sicherheit. Eine andere Alternative wäre eine selbst-checkende Software mit eingebauter Plausibilitätsprüfung. Wenn die Kontrollsoftware eine eigene Fehlfunktion entdeckt, ruft sie eine Ausnahmebehandlungsfunktion auf, um ein Recovery durchzuführen. Diese Methode kann keine Sicherheit garantieren. Sehr oft hat die Plausibilitätsprüfung die selben Fehler wie die Kontrollsoftware und so bleiben diese deswegen unerkannt. Die formalen Methoden scheinen langfristig eine bessere Lösung zu sein.

Formale Methoden

Die formalen Methoden bestehen aus einer Menge von Techniken und Werkzeugen, die auf mathematischer Modellierung und formaler Logik aufbauen. Sie werden benutzt, um Software zu spezifizieren und zu prüfen. Mit formalen Methoden kann man von einem (selbst entworfenen) mathematischen Modell ausgehend durch logische Berechnungen die logischen Eigenschaften eines Systems voraussagen. Dieses ist nur insoweit wahr, als das Modell der Realität entspricht. Der Abgleich des Modells mit der Realität geht nur durch Erfahrungen und durch Probieren (eine Schwachstelle !).

Mit formalen Methoden kann berechnet werden, ob eine Systembeschreibung (Spezifikation) in sich konsistent ist, ob bestimmte Eigenschaften garantiert werden können und ob die Anforderungen richtig entworfen und implementiert worden sind (z.Z. nur theoretisch). Weiterhin kann die Spezifikation für Simulation/Animation, zur Codegenerierung, zur Testgenerierung und Testauswertung benutzt werden.

Diese Methoden entsprechen der Rolle der Mathematik in der Elektrotechnik, im Maschinenbau und Aerodynamik. Die Mathematik stellt Methoden zur Modellierung der Objekte bereit, um ihr Verhalten durch Berechnung voraussagen zu können. Z.B. kann vor dem Bau einer Flugzeugtragfläche deren Luftwiderstand ermittelt werden. Bei der Elektrotechnik können mittels mathematischen Modellen, magnetische Feldern, Refektionen u.a. vorausberechnet werden.

Die Anwendung von formalen Methoden in der Softwareentwicklung ist aber noch nicht so reif wie in der Elektrotechnik und im Maschinenbau. Z.Z. ist sie immer noch sehr experimentell. Es gibt viele Erfolgsberichte, aber es gibt auch Berichte über das Scheitern ihrer Anwendung. Sie sind keine magischen Formeln zum Erfolg! Ihre Anwendung ist noch sehr aufwendig und benötigt besonders geschultes Personal. Ihr Aufwand wächst (erfahrungsgemäß) sogar exponentiell zur Komplexität. Deshalb ist es sinnvoll, den sicherheitsrelevanten Teil so klein und einfach wie möglich und frei von für die Sicherheit irrelevanten Teilen zu halten.

Der zusätzliche Aufwand, etwas formal zu beschreiben, muß eine Rechtfertigung haben. Nur zu formalisieren, um eine formale Spezifikation zu erhalten, ist keine Rechtfertigung. Eine formale Spezifikation ist auch nicht um jeden Preis und für alle Teile eines Systems sinnvoll. Nicht-sicherheitskritische Teile müssen nicht unbedingt formal beschrieben werden. Zu jedem formalen Bestandteil muß klar sein, in welchen Analysen und Konstruktionen die Formalisierung benutzt wird, oder wenn es als Dokumentation gedacht ist, soll klar sein, wer es lesen soll (kann er es lesen?). Ist das nicht klar definiert, lohnt sich der Aufwand für eine formale Spezifikation nicht.

Eine Entwicklung mit formalen Methoden unterscheidet sich von einer traditionellen Entwicklung in mehreren Punkten. Um diese Punkte zu erläutern, muß man zuerst zwei Sorten von formaler Spezifikation unterscheiden: operational und axiomatisch.

In einer operationalen Spezifikation passiert nur das, was explizit spezifiziert wurde (wie in einer imperativen Programmiersprache). In einer axiomatischen Spezifikation kann alles eintreten, was nicht explizit ausgeschlossen wurde. Eine operationale Spezifikation beschreibt die Funktion des Systems, während eine axiomatische Spezifikation die Eigenschaften beschreibt. Ein Teil einer operationalen Spezifikation könnte z.B. sagen: "Wenn die Temperatur zu hoch ist, schalte die Flamme aus!". In einer axiomatischen Spezifikation würde es so lauten: "Immer wenn die Temperatur zu hoch ist, muß die Flamme aus sein". Meistens können axiomatische Spezifikationen nicht animiert (simuliert) sondern nur verifiziert werden. Auf der anderen Seite können operationale Spezifikationen meistens animiert werden, aber nicht alleine verifiziert werden.

Das kleinste Beispiel

Einige Problemklassen lassen sich sehr gut und einfach mit formalen Methoden ausdrücken. Andere dagegen, die unregelmäßig und nicht algorithmisch sind, lassen sich nur sehr umständlich ausdrücken. Um die formalen Methoden zu verdeutlichen, nehme ich natürlich die am besten geeignete Problemklasse als Beispiel: eine mathematische Berechnung. Wörtlich heißt die Aufgabe "Die Quadratwurzel einer Zahl berechnen" (einfacher geht es nicht). Die Aufgabe wird in "Z" axiomatisch spezifiziert. Diese Spezifikation beschreibt nur die Eigenschaften der Ergebnisse, ohne zu sagen, wie die Aufgabe zu lösen ist. Diese Eigenschaften werden später zum Beweisen von anderen Eigenschaften benutzt:

--- sqrt ------------  ; Name der Operation 
| x?  : Realzahl       ; "?" gekennzeichnet eine Input Variable
| a!  : Realzahl       ; "!" gekennzeichnet eine Output Variable
-----------
| x? >= 0              ; Vorbedingung: Die Input Variable x? 
|                      ;               darf nicht negativ sein.
| a! * a! = x?	       ; Die Output Variable a! multipliziert
|                      ;     mit sich selbst ergibt die Input Variable x?
-------------------------

Dagegen besteht die C Funktion sqrt(x) aus ca. 100 Zeilen und ist kaum verständlich.

Als Beispiel für eine Verifikationsaufgabe nehmen wir "Die Wurzel jedes Wertes größer 1 soll kleiner als der Wert sein". Aus dem C Programm können wir das nicht verifizieren. Wir können nur das Programm viele Male laufen lassen und zeigen, daß wir kein Gegenbeispiel gefunden haben. Alle reellen Werte werden wir nicht testen können und ob es immer klappt, können wir auch nicht sagen. Mathematisch können wir die Verifikationsaufgabe folgendermaßen ausdrücken:

x >1 ^ a*a=x -> a<x
In Worten: (x>1 UND a*a = x ) Impliziert a<x.

Ein mathematischer Beweis für diese Formel besteht aus ca. einer halben Seite cryptischer Mathematik. Aber dann weiß man, daß es immer stimmt, ohne ein Programm schreiben und testen zu müssen - obwohl das Programm sowieso geschrieben und getestet werden muß.

Eigenschaften einer Entwicklung mit formalen Methoden

1. Der Spezifizierer muß das System besser kennen

Der mit der Spezifikation beauftragte Systementwickler ist gezwungen, sich mehr Gedanken über das zu entwickelnde System zu machen und er muß es besser verstehen als sonst. Der Detaillierungsgrad und die Genauigkeit seiner Spezifikation ist dadurch höher. Sein Zeitaufwand wird wesentlich höher sein als sonst. Dadurch jedoch, daß er genauer denkt, was zu implementieren ist, werden die folgenden Schritte (Entwurf, Implementierung, Integration) weniger experimenteller Natur sein, weniger Fehler verursachen und Zeit einsparen.

 

Bei der Spezifikation werden Erfahrungen gesammelt, die viel Zeit bei der Implementierung sparen können. Die Implementierung in einer Programmiersprache ist auch eine formale Spezifikation, aber mit dem höchsten Detaillierungsgrad. Wenn man davor eine andere formale Spezifikation erstellt hat, dann ist das Programm eine zweite Implementierung des Systems. Es ist zu erwarten, daß die zweite Implementierung besser ausfällt, als die erste, weil man aus der ersten gelernt hat. Das ist ein Gewinn gegenüber dem, wo die erste Implementierung das endgültige Programm darstellt.

Eine weitere verbreitete Methode, um das gleiche ohne formale Methoden zu erreichen, ist die Erstellung von Strukturprototypen. Ein Strukturprototyp wird benutzt, um die geplante Programmstruktur zu erproben, ob sie ausreichend und adäquat ist.

2. Validierung

Mit formalen Methoden kann das System durch Animation (Simulation) validiert werden, bevor es fertig gebaut ist. Dies ist oft, aber nicht immer der Fall. Nur wenige operationale Formalismen unterstützten eine Animation. Wenn der Detaillierungsgrad der Spezifikation zu abstrakt ist, ist eine Ausführung auch nicht möglich. Die Validierung ist eine prototypische Ausführung (z.B. durch Simulation) einer operationalen Spezifikation, um zu prüfen, ob das Spezifizierte den Erwartungen entspricht. Dies kann meistens nur der Auftraggeber beurteilen.

Eine weitere verbreitete Methode, um das gleiche zu erreichen, ist die Erstellung von Funktionsprototypen. Ein Funktionsprototyp wird benutzt, um die geplante Funktionalität mit den Erwartungen des Auftraggebers zu vergleichen. Die Validierung trägt dazu bei, Verständnisfehler schon in frühen Phasen der Entwicklung zu finden. Wenn diese Fehler erst beim Betrieb erkannt werden, ist ihre Korrektur extrem aufwendig. Die Ausführung hilft auch dem Entwickler, ein besseres Problemverständnis zu gewinnen. Auf diese Weise wird das sogenannte Rush-to-code-Syndrom vermieden, wonach Entwickler dazu tendieren, zu früh mit der Implementierung zu beginnen, um möglichst schnell die Ergebnisse ihrer Arbeit anhand eines lauffähigen Programms zu sehen und demonstrieren zu können.

Die Validierung arbeitet auf einer Seite mit formalen Dokumenten (Spezifikation, Prototyp) und auf der anderen Seite mit Gedanken und Gefühlen (z.B. die Meinung des Auftraggebers). Deswegen kann die Korrektheit des Systems nur anhand von Beispielen gezeigt, aber nicht bewiesen werden.

 

3. Verifikation

Durch Verifikation kann überprüft werden, ob die Spezifikation in sich konsistent (frei von Widersprüchen) ist, ob bestimmte Eigenschaften (z.B. Sicherheitsanforderungen) garantiert werden können und ob die Anforderungen richtig entworfen und implementiert worden sind (theoretisch).

Verifikation kann nur innerhalb und zwischen formal geschriebenen Dokumenten erfolgen. Dadurch können Spezifikationsfehler entdeckt werden. Aber ob die Spezifikation der Realität entspricht, kann nur durch Validierung gezeigt werden.

Beispiele von verifizierbaren Eigenschaften einer Spezifikation sind: Typ Check, Vollständigkeitsanalyse, Totalität von Operationen, Konsistenz, Undeterminismus, Zeitconstraints, Deadlocks, Lebendigkeit (liveliness), Erreichbarkeit von Zuständen (z.B. verbotene oder gefährliche Zustände), Erfüllung der Sicherheitsanforderungen, das Einhalten von Randbedingungen und Restriktionen der Technik und Sprache.

 

Die Verifikation ist z.Z. noch äußerst aufwendig. Es gibt zwar einige Werkzeuge für ihre Unterstützung wie z.B. Modellchecker und Theorembeweiser, aber sie können in der Regel nur mit großem Aufwand und nur von Spezialisten benutzt werden. Deswegen werden meistens nur kleine Teile des Systems punktartig verifiziert.

5. Automatische Code-Generierung

Manche (operationale) Formalismen erlauben bei einem genügend hohen Detaillierungsgrad eine automatische Code-Generierung aus der Spezifikation. Der Code ist nicht optimal und meistens kann es nur als Funktionsprototyp verwendet werden. Code-Generierung und Animation sind sehr ähnlich. Wenn das eine möglich ist, ist das andere auch möglich.

 

Normalerweise können die Code-Generatoren keine Entwurfs-/Implementierungsentscheidungen treffen. Deswegen muß die (operationale) Spezifikation den höchsten Detaillierungsgrad haben. Keine Details dürfen offen sein. Offene Details werden auch im Code offen sein. Dann ist aber die Frage gerechtfertigt: "Was ist der Unterschied zwischen Spezifikation und einem Programm?" Nur aus der Spezifikation kann man Analysen durchführen, die aus einem (C/C++, ADA, JAVA) Programm nicht möglich sind.

Einige Code-Generatoren erlauben eine gewisse Abstraktion, so daß nicht alle Details spezifiziert (programmiert) werden müssen. Die Abstraktion ist aber nur für vordefinierte Konstrukte in der Spezifikationssprache möglich. Dies ist auch nicht viel anders als das Benutzen von Bibliotheken aus einer Programmiersprache.

Andere (experimentelle) Code-Generatoren sind in der Lage, selbst Implementierungsentscheidungen zu treffen, so daß sie die fehlenden Details selbst generieren können. Dies ist aber sehr schwierig zu realisieren und birgt ein gewisses Risiko, da man nicht wissen kann, was der Generator entschieden hat und warum.

In jeden Fall, wenn man bereits eine formale Spezifikation hat, ist eine automatische Code-Generierung zu empfehlen, da sie schnell und (hoffentlich) ohne Fehler geht.

6. Test-Generierung und Auswertung

Bei jedem Entwicklungsschritt können Fehler unterlaufen, deswegen muß jedes Produkt gegen die an es gestellten Anforderungen verifiziert werden. Dies kann durch formale Verifikation (mit Theorembeweisern oder durch Deduktion) geschehen, ist aber äußerst aufwendig. Einfacher ist es, aus den Anforderungen ein Test-Programm zu generieren, systematisch (und vollständig) zu testen und die Testergebnisse gegen die Anforderungen auszuwerten. Insbesondere sollen die Sicherheitsanforderungen durch vollständige Tests nachgewiesen werden.

Ähnlich wie bei der Code-Generierung kann aus manchen Formalismen unter gegebenen Voraussetzungen ein Testprogramm generiert werden und die Testergebnisse können automatisch gegen die Anforderungen evaluiert werden.

 

Es wäre ein Fehler, sich nur auf diese Tests zu verlassen. Spezifikationsfehler würden unentdeckt bleiben. Das Testen unter Real-Bedingungen ist unersetzbar. Wenn man einen automatischen Code-Generator benutzt hat, wären diese Tests eigentlich nur Tests für den Code-Generator und nicht für Ihr System.

7. Systematisierung

Die Benutzung formaler Methoden von Anfang an hilft dabei, die nachfolgenden Entwicklungsschritte zu systematisieren. Das Einsetzen von formalen Methoden durch den gesamten Entwicklungsweg ist allerdings sehr aufwendig und teuer.

Grob gesprochen sind die Entwicklungsphasen: Anforderungsspezifikation, (System, DV, Software), Entwurf, Implementierung, Integration und Betrieb. Die formalen Methoden kann man von der Anforderungsspezifikation bis hin zur Integration anwenden, aber:

Von allen Fehlern, die bei der Inbetriebnahme und im Betrieb gefunden werden, kommen die meisten und die teuersten aus der Anforderungsspezifikation. Die Fehler aus der Implementierung sind nicht so viele und sind einfacher (billiger) zu korrigieren. Die Spezifikationsfehler können sich durch die ganze Implementierung ziehen und große Änderungen nötig machen. Die Implementierungsfehler sind häufig lokal in einem Modul (z.B. eine 3 anstatt einer 4) und deswegen einfacher zu korrigieren. Die schlimmsten Fehler bestehen darin, daß nicht das gewünschte spezifiziert wurde. Dies kann durch Validierung als ersten Schritt geprüft werden. Der nächst-schlimmste Fehler besteht darin, daß der Entwurf die Anforderungen nicht erfüllt.

Der Aufwand bei der Benutzung von formalen Methoden bei der Anforderungsspezifikation ist relativ niedrig und die Anzahl der Fehler, die dabei gefunden werden können, ist relativ hoch. Bei der Implementierung ist ihre Anwendung sehr aufwendig, und die Anzahl der Fehler die sie aufdecken können, ist relativ niedrig. Ihre Anwendung bis zur Implementierung hin (z.B. als Programm-Verifikation, Programm-Verfeinerung und Deduktion) ist das Aufwendigste und Teuerste.

Das beste Kosten/Nutzen - Verhältnis liegt in den Anfangsphasen. Danach wird das Verhältnis extrem schlecht und die Anwendung formaler Methoden kann nur durch zu erfüllende Sonderauflagen gerechtfertigt werden.

 

Die Praxis Heute

In der Regel werden formale Methoden nicht flächendeckend in einer Entwicklung benutzt, sondern nur punktweise bei kleinen, besonders kritischen Aspekten. Es gibt kaum dokumentierte durchgehende Vorgehensmodelle für die Verwendung von formalen Methoden, sondern es wird eher ein traditionelles Vorgehensmodell (z.B. V-Modell, Spiralmodell, Wasserfallmodell, u.a.) verwendet, welches an verschiedenen Stellen (nach Gefühl) durch formale Techniken ergänzt wird.

Ein "normaler" Ingenieur oder Software-Entwickler, der mit formalen Methoden anfangen will, wird mit vielen Problemen und Hindernissen konfrontiert, so daß er sehr schnell aufgeben wird, es sein denn, er muß diese benutzen. Die ersten Schritte sind immer die schwierigsten, und hier sind sie besonders schwierig. Das erste Hindernis ist die Auswahl der Methode. Es gibt viele Methoden und alle behaupten, die beste zu sein, z.B: 19 Varianten von Statecharts, mindestens 10 Varianten von Petri-Netzen, mehr als 10 Varianten von temporaler Logik, viele Varianten von Algebra, Lotos, SAO, ESTEREL, SIGNAL, LUSTRE, RSL, SDL, Z, VDM, B, CSP, EA, SPILL, HOL, FDM, RAISE, ACT I & II, Prospectra, CSL, TLT, SDL, HHDs, LCM, MCM, Deduktive Synthese, plus mindestens eine neue Methode aus jeder Forschungseinrichtung weltweit, die sich mit der Thematik beschäftigt. Dazu kommen die Kombinationen aus 2 oder mehreren Methoden.

Oft werden folgende Kriterien für die Entscheidung angeboten: Komplexität der Spezifikation, Komplexität des Korrektheitsbeweises, Abstraktionsgrad der Modellierung, Entwicklungsaufwand, Wiederverwendbarkeit von Spezifikation und Entwicklung und Skalierbarkeit. Aber der Entwickler hat nicht die Zeit (und Lust), um solche Studien durchzuführen, außerdem kennt er sich nicht mit allen diesen Methoden aus und kann sie deswegen nicht bewerten.

Hinzu kommt, daß keine Methode gut für alle Fälle ist (es gibt keine Methode wie die C-Sprache) und meistens unterstützt eine Methode nur wenige der obengenannten Analysen. Unter Umständen (oft) ist grade das, was man braucht, nicht dabei (und man weiß es nicht einmal)

Ist diese Entscheidung gefallen, kommt die nächste Hürde: ihre Anwendung. Diese Methoden sind schwierig zu benutzen, man braucht eine lange Einarbeitungszeit und der Ingenieur kann kaum eine Unterstützung oder Führung erwarten. Nicht jeder Entwickler kann mit diesen Methoden und ihren Werkzeugen umgehen. Der Benutzer muß sich mit vielen Methoden-Details auskennen, die für ihre Applikation irrelevant sind. Ergebnis: ein besonders geschultes Personal ist nötig und der Aufwand ist groß.

Eine Zukunftsvision

Der Weg zu sicheren verifizierbaren korrekten Systemen scheint lang und schwierig zu sein. Doch zur Zeit laufen weltweit viele Projekte, um Techniken und formale Methoden zugänglicher, effektiver und attraktiver für "normale" Ingenieure und Software-Entwickler zu machen.

Eine (noch weit entfernte) Zukunftsvision wäre, daß der Entwickler sich keine Gedanken über Formalismen machen muß. Er könnte sein Ziel-System in seiner natürlichen Sprache beschreiben. Das Entwicklungssystem soll diese (schriftliche) Sprache verstehen und an den Stellen nachfragen, wo es Ungenauigkeiten, Zweideutigkeiten oder Widersprüche findet. Die Bearbeitung findet in einer internen Repräsentation statt, die der Entwickler nicht zu kennen braucht. Die interne Repräsentation enthält Beschreibungen zu Funktions-, Sicherheits-, Fehlertoleranz-, Real-Zeit-, Kommunikations- und Struktur-Anforderungen. Ausgehend von dieser internen Repräsentation könnten (semi-) automatisch Validationsprototyp-Generierung, Verifikation, Code-Generierung, Testprogramm-Generierung, und Testauswertung durchgeführt werden. Nach wie vor müssen Validierung und Test vom Entwickler zusammen mit dem Auftraggeber selbst durchgeführt werden. Wichtig ist auch eine Konvertierung aus der internen Repräsentation in die natürliche Sprache des Entwicklers für Nachfragen und Ausgaben. Eine Ausgabe mit Referenzen zur (dem Entwickler unbekannten) internen Repräsentation ist nutzlos.

Weitere Referenzen

Mein Buch: Sichere und Fehlertolerante Steuerungen

http://www.first.fhg.de/~espress
ESPRESS: Ingenieurmäßige Entwicklung sicherheitsrelevanter eingebetteter Systeme.
Das Vorhaben ESPRESS zielt auf eine breite Verbesserung der Produktivität bei der Entwicklung komplexer, sicherheitsrelevanter, eingebetteter Systeme und auf eine Steigerung der Verläßlichkeit der Systeme selbst. Dies wird durch die Entwicklung einer durchgängigen, methodischen und werkzeugunterstützten Software-Technologie für spezifische Anwendungsgebiete erreicht.

http://www4.informatik.tu-muenchen.de/proj/korsys/all/index.html
Korrekte Software für sicherheitskritische Systeme
The aim of the KorSys project is to improve the applicability of formal methods for the specification and verification of complex software systems in practice. To achieve this challenging goal partners from industry and university work together.

http://www.informatik.uni-bremen.de/~uniform/
Universal Formal Methods Workbench
Academic and industrial partners are developing a universal development environment for formal methods. The Project UniForM Workbench is sponsored by the BMBF from 1995 until 1998.

http://www.dcs.rhbnc.ac.uk/research/formal/safefm.html
The Practical Application of Formal Methods to Safety Critical Systems.
The project aims to devise a methodology and calculus for constructing provably correct system specifications, and to provide guidelines on a cost effective approach to using formal methods in the development and assessment of high integrity software systems.

http://www.csr.ncl.ac.uk/projects/FME/InfRes/applications/index.html
The FME applications database.
This page gives access to the latest edition of the FME applications database. At present, the database contains questionnaires completed by commercial and academic users of formal methods describing industrial or industry-related application of formal techniques

http://www.comlab.ox.ac.uk/archive/formal-methods.html
The World Wide Web Virtual Library: Formal Methods.
This document contains some pointers to information on Formal Methods available around the world on the World Wide Web (WWW), a global hypermedia system providing worldwide information.

http://www.cs.tcd.ie/FME/
Formal Methods Europe (FME) is a European organization supported by the Commission of the European Union, with the mission of promoting and supporting the industrial use of formal methods for computer systems development.

http://eis.jpl.nasa.gov/quality/Formal_Methods/
NASA Formal Methods Guidebook - Formal Methods Specification and Verification
Guidebook for Software and Computer Systems: Planning and Technology Insertion Written for project decision makers, including managers, engineers, and assurance personnel, who are considering the use of Formal Methods on their project. Easily understood overview of important issues associated with the use of formal specifications. Useful guide to planning and implementing Formal Methods on a project