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

摘要: Ein Model Checker verifiziert, ob ein Modell bestimmte Anforderungen erfullt. Eine Moglichkeit, das Verhalten von Softwaresystemen zu modellieren, sind endliche Automaten. Diese finden Einzug in die Unified Modelling Language Form Statecharts. UML-Statecharts konnen hohes Mas an Komplexitat erreichen, so dass sich ihr Zustandsraum nicht mehr komplett den Hauptspeicher abbilden lasst. Dies fuhrt dazu, eine vollstandige Verifikation mit einem moglich ist, da der gesamte untersucht werden kann. Um diesem Problem begegnen, stellt diese Arbeit domanenspezifische Sprache UDL (UML-Statechart Description Language), sowie Transformation Eingabesprache Promela vor. Der Schwerpunkt und des Ubersetzungsprozesses liegt dabei auf Generierung effizientem Promelacode, beim Verifizieren einen moglichst kleinen belegt. Vorteil durch diesen Ansatz auch grosere Modelle wieder verifizierbar werden. Die Machbarkeit Ansatzes daraus entstehenden Vorteile anhand einer Fallstudie dem 3DBewegungstrackingsystem AssyControl demonstriert.