AP 3: Modellbasierte Verifikation von Realzeiteigenschaften

Problembeschreibung

Ein bedeutender Vorteil der modellgetriebenen Anwendungsentwicklung ist die frühzeitige Überprüfung von Eigenschaften der zu entwickelnden Systeme, noch vor ihrem eigentlichen Zusammenbau. Allerdings gibt es noch keine CASE-Umgebungen, die die Analyse und Verifikation von realzeitbehafteten Modellen unterstützen.

Zielsetzung/Leistungsumfang

Ziel des AP ist die Untersuchung der Abbildung von Systemmodellen auf das Eingabeformat von Analysewerkzeugen, mit denen Realzeiteigenschaften überprüft werden können. Ausgangspunkt dafür wird die bereits in HIDOORS untersuchte Abbildung von Zustandsdiagrammen auf zeitabhängige Automaten sein, die auf eine Modellverifikation mit dem Model-Checker Uppaal abzielt. Hier sind folgende Innovationen geplant:

• Anschluss von Modellprüfern an das CASE-Werkzeug Ameos (z.B. Uppaal, SPIN, HyTech)
• Austauschbarkeit der Modellprüfer, um ihre unterschiedlichen Vorteile ausnutzen zu können
• Rückintegration von Fehlermeldungen der Model-Checker in die Modelle; dazu Erweiterung von Ameos

Weiterhin kann auf den Erfahrungen des DFKI und der TU Braunschweig aufgebaut werden.

Abhängigkeiten von anderen Arbeitspaketen

Import: AP 1, AP 2, Export: AP 4, AP 5, AP 6, AP 9.

Beteiligte Projektpartner

• TU Dresden (verantwortlich)
• ScopeSET
• DFKI