 |
| | | | | Beschreibung | | Mit Hilfe der vom OFFIS und der Universität Oldenburg entwickelten Verifikationsumgebung für Statemate kann die Erfüllung der Anforderungen einer in Symbolic Timing Diagrams vorliegenden Spezifikation durch ein als State-Chart vorliegendes Modellbildung nachgewiesen werden. Der Unterschied zu einer „einfachen“ Simulation innerhalb von Statemate liegt in der Vollständigkeit dieses Nachweises und der automatischen Durchführung.
Mit der Statemate-Verifikationsumgebung wird das Werkzeug Statemate um die Möglichkeit der formalen Verifikation (siehe Verifikation (formal)) unter Verwendung eines Model Checkers (siehe Model Checking) erweitert. Damit der Model Checker das zu überprüfende Modell verarbeiten kann, muss dieses zunächst aus der Statemate-eigenen Repräsentation in das Eingabeformat des Model Checkers überführt werden, was innerhalb der Statemate-Verifikationsumgebung automatisch geschieht.
Die direkte Eingabesprache für die nachzuweisenden Anforderungen (Eigenschaften) ist mathematisch und für die meisten Benutzer schwer zu verstehen. Daher bietet die Statemate-Verifikationsumgebung eine einfach verständliche graphische Eingabemöglichkeit für die zu verifizierenden Eigenschaften des Systems: Symbolische Zeitdiagramme (siehe Symbolic Timing Diagrams). Sie sind eine Erweiterung der klassischen Zeitdiagramme, die im Hardwarebereich verbreitet sind. Analog zu der Behandlung der Modelle werden die als symbolische Zeitdiagramme vorliegenden Spezifikationen von der Statemate-Verifikationsumgebung in die Eingabesprache des Model Checkers übersetzt.
Gilt eine Anforderung für ein Modell nicht, so generiert der Model Checker einen sogenannten Fehlerpfad, der anzeigt, wie die spezifizierte Eigenschaft verletzt wurde. Der Fehlerpfad kann wiederum als symbolisches Zeitdiagramm oder als Statemate-Simulationsdatei festgehalten werden. Die Statemate-Simulationsdateien können dann im Statemate-Simulator nachvollzogen werden.
Die folgende Abbildung gibt einen groben Überblick über die Komponenten der am OFFIS entwickelten Statemate Verifikationsumgebung.
Abbildung 1: Überblick über die Komponenten der Statemate Verifikationsumgebung
Weitere Details über die Funktionsweise der Statemate Verifikationsumgebung sind unter Statemate Verifikation (Details) nachzulesen.
| |
| | | | | | | | | | | | | Zu dieser Seite wurden noch keine Kommentare oder Bewertungen abgegeben. |
|
| | | | |  | Übergeordnet | | | | | | | | | | | | | | Statemate Verifikation | | | | |  | Untergeordnet | | | | | | | | | | | | | | | | | | | | | | | | Ansprechpartner | | | | | | | | Literaturhinweise | | | | | | | | | | | | | | | | | | | Löst die Probleme | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Weitere Themen | | | | | | | | | | | Glossar | | | | | | | | | | | | | | | | | | | |
|
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights 
Eintrag kommentieren
