Helsinki University of Technology,
     Laboratory for Theoretical Computer Science

Symbolic Methods for UML Behavioural Diagrams (SMUML)

A research project funded by TEKES, Nokia, Conformiq, and Mipro
Jan 1, 2005 - Dec 31, 2007

Project leader: Prof. Ilkka Niemelš

Research Personnel: Tommi Junttila, Heikki Tauriainen, Jori Dubrovin, Vesa Ojala, Toni Jussila, Timo Latvala, Sami Liedes, Juhani Peltonen

Summary: The increasing size and level of concurrency of software systems poses new challenges for obtaining reliable software and cost effectiveness in the software process. Especially the analysis of the dynamic (behavioral) aspects of a software system in its various development phases is gaining more importance. The sooner the incorrect behaviours of a software system can be detected, the cheaper it is to correct them.

This project studies the analysis of dynamic aspects of software system models described in the Unified Modelling Language (UML). In UML such aspects are described with so-called behavioural diagrams, e.g. state machine and message sequence diagrams. This project focuses on UML models composed of concurrently running objects communication with each other via asynchronous message passing and attribute access; the behavior of each object is described with a state machine. The goal is to develop new techniques for model checking such systems in order to to find bugs such as deadlocks, assertion violations, and implicit consumption of messages.

Publications of the project

The SMUML Software Distribution

The software developed in the project is released under the GNU General Public License. The current release version 1.0.1 can be downloaded here.