Ludwig-Maximilians-Universität München, Institut für InformatikUML State Machines können auf Time Events reagieren, die dadurch ausgelöst werden, daß sich die Zustandsmaschine seit einem definierten Zeitraum in einem gegebenen Zustand befindet. Dadurch ist es möglich, einfache Echtzeitsysteme mit der UML zu modellieren.
Diese Diplomarbeit befaßt sich mit der Verifikation von UML Zustandsmaschinen, die durch Time Events getriggert werden. Dazu wurde das Werkzeug Hugo/RT entwickelt, das Zustandsmaschinen in das Eingabeformat des Model Checkers Uppaal transformiert, der zur Modellierung Systeme von Zeitautomaten einsetzt. Ein Sequenzdiagramm, das einen gezeiteten Ablauf der Kommunikation der Objekte des Systems definiert, wird in einen beobachtenden Automaten übersetzt. Dieser wird durch den Austausch der Signale über einen Netzwerk-Automaten angeregt. Ist es dem Automaten möglich, den Zustand zu erreichen, der den Empfang der letzten Nachricht der Kollaboration symbolisiert, so ist auch dieser spezielle Nachrichtenaustausch möglich.
Schließlich wird Uppaal aufgerufen, um sowohl die gegebene Kollaboration, als auch andere Eigenschaften des Systems, wie beispielsweise Verklemmungsfreiheit, zu überprüfen.
Bei den verschiedenen Übersetzungsvorgängen ist von höchster Priorität, dass jeweils die Semantik der UML berücksichtigt wird.
Bearbeiter: Christopher Rauh
Aufgabensteller: Prof. Tobias Nipkow, PhD
Betreuer: Dr. Stephan Merz, Dr. Alexander Knapp
Fertigstellung: 15. April 2002