Ludwig-Maximilians-Universität München, Institut für Informatik
Lehr- und Forschungseinheit für Programmierung und Softwaretechnik

Fortgeschrittenenpraktikum

Model Checking von UML State Machines: Visualisierung von Gegenbeispielen als UML-Sequenzdiagramme im CASE-Tool ArgoUML

Inhalt

Die UML ermöglicht die Beschreibung des Verhaltens eines dynamischen Systems mit Hilfe von Zustandsautomaten und Kollaborationsdiagrammen. Zustandsautomaten werden mit UML-Klassen assoziiert und beschreiben die Zustände von Objekten und ihre Reaktionen auf eingehende Ereignisse. Als eine besondere Form von Interaktionddiagrammen beschreiben die Sequenzdiagramme, wie sich die Objekte eines Systems durch die ausgetauschten Nachrichten gegenseitig beinflussen. Das Werkzeug HUGO ist in der Lage zu prüfen, ob die Beziehungen, die in einem Kollaborationsdiagramm beschrieben sind, mit den angegebenen Zustandsautomaten realisiert werden können. HUGO übersetzt die Zustandsautomaten in die SPIN-Eingabesprache Promela und die Kollaboratinen in sog. Büchi-Automaten ("never claims"). Danach wird der Modelchecker SPIN aufgerufen und das Modell und die Automaten werden auf die Möglichkeit der Kollaborationen hin überprüft. Falls eine Kollaboration m&oum;lich ist, erzeugt SPIN ein "Gegenbeispiel", das die erfolgreiche Ausführung zeigt. Es kann auch üperf&uum;ft werden, ob das angegebene Modell eine Verklemmung verursacht. In dieser Projektarbeit wurde ein Prozeß erstellt, der das "Gegenbeispiel" als ein Sequenzdiagramm mit Hilfe des CASE-Tools ArgoUML darstellt.

Materialien

Bearbeiter: Sergiy Safonov
Aufgabensteller: Prof. Dr. Martin Wirsing
Betreuer: Dr. Alexander Knapp
Fertigstellung: März 2003