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

Diplomarbeit

Model Checking and Compiling UML State Machines

Inhalt

We describe HUGO, a prototype tool designed to facilitate the use of UML state machines in software projects. On the one hand it automatically verifies state machines using the model checker SPIN, on the other hand it compiles state machines into Java code that can be integrated into any Java application. The model checking feature is primarily designed to verify whether interactions expressed by certain collaborations can indeed be realized by a set of state machines; additionally a check for possible deadlocks can be performed. The compilation into Java code bridges a gap between the behavioral specification of Java classes, using state machines, and their implementation.

Materialien

• HUGO Homepage mit Download und Anleitung
• Einführung (PDF, ca. 106kB)

Bearbeiter: Timm Schäfer
Aufgabensteller: Prof. Dr. Martin Wirsing
Betreuer: Dr. Stephan Merz, Dr. Alexander Knapp
Fertigstellung: 27. Juni 2001