Die Erstellung einer Spezifikation geht notwendigerweise der Durchführung einer Verifikation voraus. In einer Spezifikation werden die Eigenschaften festgelegt, die ein Modell erfüllen muss. Üblicherweise geschieht dies in einem mathematisch-logischen Formalismus. Für Hardware- und Software-Systeme wird in der Regel eine temporale Logik verwendet, mit der Zusicherungen darüber ausgedrückt werden können, wie sich das Verhalten des betrachteten Systems in Abhängigkeit von der Zeit entwickelt.
Eigenschaften einer Spezifikation
Spezifikationen müssen vor allem präzise und nachvollziehbar sein. Einerseits müssen die festgelegten Eigenschaften widerspruchsfrei sein und es muss klar sein, dass Ersteller und Benutzer einer Spezifikation aus ihr jeweils die gleichen Eigenschaften des Modells ablesen.
Entscheidend ist bei der Erstellung der Spezifikation unter anderem ihre Vollständigkeit im Hinblick darauf, dass alle relevanten Eigenschaften des Systems abgedeckt sind. Denn mit Model Checkern und Theorem Provern gibt es zwar automatisierte Verfahren zur Überprüfung der Korrektheit einer Modellierung in Bezug auf die Spezifikation; aber die Ergebnisse einer solchen Verifikation machen keinerlei Aussage über Eigenschaften des Systems, die in der Spezifikation nicht festgelegt sind. Ist die Spezifikation also unvollständig, so kann die Verifikation leicht das trügerische Ergebnis eines korrekten Systems liefern, obwohl wesentliche Eigenschaften gar nicht berücksichtigt wurden.
Ein weiteres Qualitätskriterium für Spezifikationen ist ihre Wiederverwendbarkeit, die insbesondere für Softwarekomponenten relevant ist, die Bestandteil von Bibliotheken sein können und als solche immer wieder in unterschiedlichem Kontext verwendet werden können, so dass sich hier der Aufwand einer (auf der Spezifikation aufbauenden) Verifikation besonders auszahlt.
Ein wichtiger Nebeneffekt einer Spezifikation ist ihre Funktion bei der Erstellung einer Dokumentation zu dem in Entwicklung befindlichen Produkt. Die Spezifikation kann hierbei als Referenz-Dokumentation des Systems angesehen werden und als Basis für eine informellere Form der Dokumentation wie zum Beispiel Benutzer- und Systemhandbücher dienen.
|
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights 
Eintrag kommentieren
