 | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights 
| ||||||
|  | |  | |  | |
| ||||||
| ||||||
|  | | ||||
| ||||||
Verfahren |
|
Statemate Verifikation (Details) |
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| Beschreibung | |||||||||
| |||||||||
| Als eine Vorstufe zur eigentlichen Verifikation bietet die Statemate-Verifikationsumgebung eine Reihe von Analysen und Debughilfen an. Dazu gehören beispielsweise Tests, ob Nichtdeterminismen im Modell vorhanden sind, ob mehrere Komponenten in einem Schritt auf dieselbe Variable schreiben (multiple writer conflict) und ob Lese-/Schreibkonflikte auf einer Variablen möglich sind. Die Ergebnisse dieser Analysen können wiederum sowohl als symbolisches Zeitdiagramm als auch als Statemate-Simulationsdatei festgehalten werden.
Darüber hinaus ist es möglich zu überprüfen, ob und wie Basic-Zustände und Zustandskonfigurationen des Modells erreichbar sind (drive-to-state, drive-to-configuration). Ebenso können einfache Anfragen an das Modell gestellt werden (drive-to-property) wie zum Beispiel die Frage, ob ein Ausgang (Ausgangsvariable) einen bestimmten Wert annehmen kann. Falls die Zustände erreichbar sind bzw. die untersuchten Ausgänge den gewünschten Wert annehmen können, wird eine Statemate-Simulationsdatei generiert, die eine Simulation bis zu dem relevanten Zustand zeigt... Die einzelnen Werkzeuge der Verifikationsumgebung sind in einer grafischen Oberfläche integriert, die es erlaubt, durch die verschiedenen Hierarchiestufen des Modells zu navigieren, Teilkomponenten auszuwählen, für die Beweise konstruiert werden sollen, und diese Beweise auch auszuführen. Die Ergebnisse der Beweisläufe werden in einer Datenbank verwaltet und automatisch als ungültig gekennzeichnet, wenn sich die entsprechende Komponente oder eine Anforderung geändert haben. Die eigentliche Verifikation erfolgt in der Statemate-Verifikationsumgebung im sogennanten Assumption/Commitment-Stil. Die überwiegende Mehrheit der Softwaresysteme, für deren Verifikation die Verifikationsumgebung entwickelt wurde, sind nicht in sich geschlossene Systeme, sondern sie interagieren mit ihrer Umgebung (Eingebettete Systeme Rückkehr zu Statemate Verifikation | |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
Eintrag kommentieren | ||||
| ||||
| ||||
| ||||
| Statemate Verifikation... | ||||
| ||||
| ||||
| ||||
| ||||
| Weitere Themen | | ||
| ||||
|
| | ||
|
| | ||
| ||||
| ||||
| | | ||
| ||||||||||||||
|
