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

Diplomarbeit

Constructing Automata for UML 2.0 Interactions

Inhalt

Model checking as a method for verifying system models has become widely used in software engineering recently. One important aspect of distributed systems that needs to be verified is the communication between different entities in the system. Several graphical languages have been proposed to model those aspects of computer systems. The Unified Modeling Language is one well known and widely used standard describing software models in general, and communication behaviour in particular. The extended version UML 2.0 introduces significant changes to interactions, UML s formalism to specify the communication behaviour in distributed systems. The informal specification describes an interaction language with substantial expressive power provided by the newly introduced interaction operators. However, a formal semantics is lacking. Since model checkers usually work on finite state systems, most often in the form of finite state automata like Büchi automata, constructing automata for interactions is a fundamental intermediate step between the specification and the verification of a system. Consequently, defining a formal semantics for interactions in the form of automata helps to alleviate the deficiency of UML 2.0 and also bridges the gap between modelling and verification.

This diploma thesis presents an approach to define semantics for UML 2.0 interactions. Furthermore, a simple text-based language to describe interactions is introduced. Interaction specifications in that language are used as input for the interaction processor, prototypically implementing the algorithms used to define the formal semantics for interactions. Output of the transformation can be generated in different formats and is strongly oriented towards the requirements of Hugo/RT. Hugo/RT is an ongoing project with the goal to develop a set of tools to apply model checking techniques to UML state machines and interactions. A short case study shows the use of Hugo/RT and highlights the extended expressive power of UML 2.0 interactions.

Materialien

• HUGO/RT Homepage

Bearbeiter: Jochen Wuttke
Aufgabensteller: Prof. Dr. Martin Wirsing
Betreuer: Dr. Alexander Knapp
Fertigstellung: 10. Mai 2005