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.