Logo des Repositoriums
 
Zeitschriftenartikel

Verifikation von UML-Statecharts unter besonderer Berücksichtigung von Speicherverbrauch und Laufzeit des Model Checkers

Vorschaubild nicht verfügbar

Volltext URI

Dokumententyp

Text/Journal Article

Zusatzinformation

Datum

2011

Zeitschriftentitel

ISSN der Zeitschrift

Bandtitel

Verlag

Geselllschaft für Informatik e.V.

Zusammenfassung

Ein Model Checker verifiziert, ob ein Modell bestimmte Anforderungen erfüllt. Eine Möglichkeit, das Verhalten von Softwaresystemen zu modellieren, sind endliche Automaten. Diese finden Einzug in die Unified Modelling Language in Form von Statecharts. UML-Statecharts können ein hohes Maß an Komplexitt erreichen, so dass sich ihr Zustandsraum nicht mehr komplett in den Hauptspeicher abbilden lsst. Dies führt dazu, dass eine vollstndige Verifikation mit einem Model Checker nicht mehr möglich ist, da der gesamte Zustandsraum nicht mehr untersucht werden kann. Um diesem Problem zu begegnen, stellt diese Arbeit die domnenspezifische Sprache UDL (UML-Statechart Description Language), sowie eine Transformation von UDL in die Model Checker Eingabesprache Promela vor. Der Schwerpunkt der Sprache UDL und des Übersetzungsprozesses liegt dabei auf der Generierung von effizientem Promelacode, der beim Verifizieren einen möglichst kleinen Zustandsraum belegt. Der Vorteil ist, dass durch diesen Ansatz auch größere Modelle wieder verifizierbar werden. Die Machbarkeit des Ansatzes und die daraus entstehenden Vorteile werden anhand einer Fallstudie mit dem 3D-Bewegungstrackingsystem AssyControl demonstriert.

Beschreibung

Ammann, Christian (2011): Verifikation von UML-Statecharts unter besonderer Berücksichtigung von Speicherverbrauch und Laufzeit des Model Checkers. Softwaretechnik-Trends Band 31, Heft 3. Bonn: Geselllschaft für Informatik e.V.. PISSN: 0720-8928. Berichte aus den Fachgruppen und Arbeitskreisen

Schlagwörter

Zitierform

DOI

Tags