 | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Wissensbrowser starten | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ||||||
|  | |  | |  | |
| ||||||
| ||||||
|  | | ||||
| ||||||
Verfahren |
|
Formale Spezifikationstechniken |
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| Beschreibung | |||||||||
| |||||||||
| Formale Spezifikationssprachen gibt es seit Anfang der 80er Jahre. Bei der Spezifikation von Softwaresystemen soll die ungenaue menschliche Sprache durch die präzisen Mittel der Mathematik mit klarer Syntax und Semantik ersetzt werden. Fehler in Spezifikation und Software werden damit so früh wie möglich vermieden. Qualität wird in formal spezifizierte Systeme hineinkonstruiert.
Motivation für formale Methoden Je später Fehler im Laufe eines Softwareprojektes gefunden werden, desto teurer oder risikoreicher sind sie. Fehler, die in der Anforderungsanalyse gefunden werden, sind um Größenordnungen preiswerter als die Fehlerbehebungen bei bereits ausgelieferten Produkten. Messungen von B.W. Boehm Anfang der 80er Jahre belegen das. Die Grundidee formaler Spezifikationsmethoden besteht darin, Qualität in ein System hinein zu spezifizieren bzw. zu konstruieren und diese nicht nur über Reviews, Inspektionen oder Tests zu messen. Im Idealfall wird ein formales Modell des Systems in der Analysephase erstellt und bis hin zum ausführbaren Code verfeinert. Durch die mathematische Präzision der formalen Methoden werden Mehrdeutigkeiten, Widersprüche oder Lücken früher entdeckt, als mit herkömmlichen informellen Methoden. Automatische Überprüfung der Modelle und des entstandenen Codes ist möglich (Verifikation, Validierung), Code und Testfälle sind generierbar. Systemeigenschaften können über die Spezifikation bewiesen werden. Wenn beispielsweise eine Fahrstuhlsteuerung spezifiziert wird, ist es wichtig, bestimmte Eigenschaften der Software sicherzustellen und diese im Zweifel zu beweisen. Die Fahrstuhltür darf beispielsweise niemals zwischen zwei Stockwerken aufgehen. In einem Stockwerk muss die Fahrstuhltür immer aufgehen. Für diese überschaubaren Probleme lohnt sich der Einsatz formaler Methoden, mit ihnen können die geforderten Eigenschaften sichergestellt werden. Ein Test der Software kann lediglich Fehler aufzeigen, aber nicht ihre Abwesenheit beweisen. "Formale-Methoden-Zoo" Eine ganze Reihe von formalen Methoden sind in Industrie und Forschung definiert worden. Man kann durchaus von einem undurchschaubaren Formale-Methoden-Zoo sprechen. Eine Übersicht findet sich beispielsweise in der Formal Methods Virtual Library , dort werden 92 Methoden und Werkzeuge genannt. Grob kann zunächst zwischen formalen Spezifikationsmethoden und Analysetechniken unterschieden werden. FOCUS, B oder Z sind Beispiele für formale Spezifikationsmethoden. Die mit diesen Methoden erstellten Modelle von Systemen können mit Verfahren wie Model Checking oder Theorem Beweisen analysiert werden. Der entstandene Code kann über Statische Analyse untersucht werden. Formale Spezifikationsmethoden beschäftigen sich mit der formalen Erfassung und Strukturierung von Anforderungen und ihrer Verfeinerung bis hin zum Systemdesign bzw. zu generiertem Code. Die formalen Spezifikationsmethoden können grob in modellbasierte und algebraische Methoden aufgeteilt werden. Algebraische Methoden konzentrieren sich auf die Funktionen eines Systems, modellbasierte Verfahren fokussieren den Zustand. | |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
Eintrag kommentieren
| ||||||||||||||
|
