 | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Wissensbrowser starten | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ||||||
|  | |  | |  | |
| ||||||
| ||||||
|  | | ||||
| ||||||
Verfahren |
|
Wann formale Spezifikationsmethoden verwenden? |
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| Beschreibung | |||||||||
| |||||||||
| Kernfrage für den Einsatz einer formalen Spezifikationsmethode ist die Abwägung von Kosten und Nutzen. Das Hauptargument der formalen Methoden besagt, dass die Einsparungen über früher gefundene Fehler und Inkonsistenzen die zunächst höheren Spezifikations- und Verifikationskosten refinanzieren.
Anwendungsdomänen unterscheiden sich in den Konsequenzen und den Kosten von Fehlern. Fehler in Kraftwerkssteuerungen oder einer Airbag-Elektronik bedeuten Gefahr für Leib und Leben. Rückrufaktionen für PKWs wegen eines Fehlers in einem eingebetteten System sind sehr teuer, während Fehler in betrieblichen Informationssystemen in der Regel leichter und mit weniger wirtschaftlichem Schaden zu beheben sind. Der Hauptanwendungsbereich der formalen Methoden liegt daher vor allem bei Systemen, die in irgendeiner Form kritisch sind, d.h. bei denen Fehler schwere Konsequenzen haben. In kritischen Systemen ist die Testphase in der Regel sehr teuer, sie kann leicht 50% des Gesamtbudgets verbrauchen. Werden zu wenig Tests durchgeführt, ist das Risiko teurer Fehler im Systembetrieb sehr hoch. Über formale Methoden können Kosten in der Testphase und Wartungskosten wegen verminderter Fehler eingespart werden. Viele Referenzprojekte berichten über derartige Ersparnisse [Hal90],[BBFM99] Das Gesamtsystem wird nicht immer vollständig formal spezifiziert, in bestimmten Fällen ist es ausreichend, nur den kritischen Teil der Software formal zu behandeln und den verbleibenden Rest mit informellen Methoden zu entwickeln. Hall und Chapman beschreiben ein Referenzprojekt. | |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
Eintrag kommentieren | ||||
| ||||
| ||||
| ||||
| Wann formale Spezifikationsmethoden... | ||||
| ||||
| ||||
| ||||
| ||||
| Weitere Themen | | ||
| ||||
|
| | ||
|
| | ||
| ||||
| ||||
| | | ||
| ||||||||||||||
|
