Zeitschriftenartikel
Verifikation von UML-Statecharts unter besonderer Berücksichtigung von Speicherverbrauch und Laufzeit des Model Checkers
Lade...
Volltext URI
Dokumententyp
Text/Journal Article
Zusatzinformation
Datum
2011
Autor:innen
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.