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: Optimierungen und Erweiterungen

Inhalt

Das Werkzeug HUGO unterstützt die Verwendung von UML state machines bei der Software-Entwicklung. Es erlaubt einerseits die Erzeugung von Java-Klassen zur Implementierung der Zustandsmaschinen eines UML-Modells und andererseits die automatische Überprüfung von Eigenschaften durch Anbindung des Modelcheckers Spin. Dabei liegt der Schwerpunkt darauf, die Realisierbarkeit von Interaktionen zu überprüfen, die durch Kollaborationsdiagramme beschrieben werden.

Bei der Evaluierung von HUGO stellte sich heraus, dass die Anzahl der Zustände, die vom Modelchecker überprüft werden müssen, teilweise unnötig groß ist. In diesem Praktikum sollen Möglichkeiten zur Optimierung des erzeugten Promela-Codes untersucht werden. Ferner sollten einige Einschränkungen des aktuellen Prototyps beseitigt werden. Im einzelnen sind folgende Themen vorgesehen:

• Verkleinerung des erzeugten Promela-Codes durch generische Prozess-Deklarationen und Instanziierung.
• Möglichkeiten zur Verringerung der vom Modelchecker zu überprüfenden Zustände. Dies kann evtl. durch Verwendung von Funktionen statt Prozessen in der Spin-Erweiterung dSpin erreicht werden. Ist dies nicht möglich, wäre eine andere Struktur des erzeugten Codes zu erwägen, die eine effizientere Verifikation erlaubt.
• Erweiterungen des aktuellen Prototyps um mehrere Instanzen pro Klasse und um Event-Parameter.
• Auslesen von Kollaborationen aus dem UML-Modell anstatt der bisherigen ASCII-Eingabe.

Materialien

• HUGO Homepage
• Spin-Homepage
• dSpin-Homepage

Bearbeiter: Simon Bäumler
Aufgabensteller: Prof. Dr. Martin Wirsing
Betreuer: Dr. Stephan Merz, Dr. Alexander Knapp
Fertigstellung: Wintersemester 2001/02