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

Abstract

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.