 | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Wissensbrowser starten | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ||||||
|  | |  | |  | |
| ||||||
| ||||||
|  | | ||||
| ||||||
Verfahren |
|
Wie wird formal spezifiziert? |
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| Beschreibung | |||||||||
| |||||||||
| Die Anforderungen an ein Softwaresystem sind häufig in natürlicher Sprache aufgeschrieben. Sie sind in der Regel nicht präzise und enthalten Auslassungen, Redundanzen und Widersprüche.
Bei formalen Spezifikationsverfahren werden die Anforderungen zunächst formalisiert und in der mathematischen Notation der jeweiligen Methode aufgeschrieben. Die Operationen und die Zustände des Systems werden mathematisch definiert, z.B. mit Hilfe von Mengen, und aussagenlogischen Formeln über den Inhalt dieser Mengen. Um Modellierungsfehler zu vermeiden und die Modellierung zu vereinfachen, bieten viele formale Beschreibungstechniken grafische Werkzeuge, die den mathematischen Kern verbergen. Die formalisierten Anforderungen werden zu einer Systemspezifikation zusammengesetzt. Die hier vorgenommene Gruppierung und Aufteilung der Funktionalität ist bereits ein erster Designschritt. Das formale Aufschreiben von Anforderungen deckt offene Fragen sowie Widersprüche und Inkonsistenzen auf. 
Eine Validierung der formalisierten Anforderungen gegen die Originalanforderungen ist ein Mittel der Qualitätssicherung. Dies kann über ein Review der Dokumente oder eine Simulation der Spezifikation geschehen. Maschinell ist diese Validierung offenbar nicht möglich. Auf der formalen Spezifikation lassen sich bestimmte Systemeigenschaften nachweisen, z.B. dass gewisse Ausnahmesituationen niemals auftreten oder dass eine Eigenschaft immer gewährleistet wird. Für eine Fahrstuhlsteuerungs-Software könnte beispielsweise nachgewiesen werden, dass die Fahrstuhltür niemals zwischen zwei Stockwerken aufgeht. Dazu werden Werkzeuge wie ModelChecker oder Theorem-Beweiser verwendet. Die formale Spezifikation wird in der Designphase ausgebaut und verfeinert. Im Idealfall kann aus ihr direkt der Code für das System generiert werden. Damit passt die Implementierung per Definition zur Spezifikation. Aus einer abstrakten High-level-Spezifikation ist Code-Generierung nur im Einzelfall möglich. Die formale Spezifikation wird in der Regel verfeinert und ausgebaut, alternativ wird das System mit Hilfe der abstrakten Spezifikation manuell implementiert. Die Verfeinerungsschritte werden dann einzeln verifiziert oder der entstandene Code wird durch (generierte) Testfälle überprüft. Die formalen Spezifikationssprachen bieten in der Regel keine eigenen Vorgehensmodelle an. In welcher Phase eines Entwicklungsprozesses welcher Teil der Spezifikation entsteht wird nicht detailliert. Die formalen Spezifikationssprachen sind daher in bestehende Prozesse der jeweiligen Firma zu integrieren. | |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
Eintrag kommentieren | ||||
| ||||
| ||||
| ||||
| Wie wird formal spezifiziert? | ||||
| ||||
| ||||
| ||||
| ||||
| Weitere Themen | | ||
| ||||
|
| | ||
|
| | ||
| ||||
| ||||
| | | ||
| ||||||||||||||
|
