Where academic tradition
meets the exciting future

Model Checking Dynamic and Hierarchical UML State Machines

Toni Jussila, Jori Dubrovin, Tommi Junttila, Timo Latvala Latvala, Ivan Porres, Model Checking Dynamic and Hierarchical UML State Machines. In: Proceedings of the 3rd Workshop on Model Design and Validation (MoDeVa 2006), 2006.

Abstract:

This paper presents a technique to model check UML specifications
by translating UML models to the model checker SPIN. Our models consist of active UML classes,
whose behavior is defined by hierarchical state machines. The
intended application is to find errors in protocols communicating using asynchronous message
passing. Compared to previous efforts using a similar approach, our novel points are the
following. First, we consider a subset of UML
that in our opinion is expressive enough for protocol models but allows a simpler
translation to SPIN than existing work. Preliminary analysis of simple industrial
models support our conclusions on the expressivity of our UML subset. Second,
we present a powerful action language that is still amenable to automatic analysis.
The action language is used to specify the effects of transitions, which may include dynamic
creation of new objects. Finally, we discuss an even simpler SPIN
translation for flattened UML state machines and compare it to the translation
that supports hierarchy.

BibTeX entry:

@INPROCEEDINGS{inpJuDuJuLaPo06a,
  title = {Model Checking Dynamic and Hierarchical UML State Machines},
  booktitle = {Proceedings of the 3rd Workshop on Model Design and Validation (MoDeVa 2006)},
  author = {Jussila, Toni and Dubrovin, Jori and Junttila, Tommi and Latvala, Timo Latvala and Porres, Ivan},
  year = {2006},
}

Belongs to TUCS Research Unit(s): Software Construction Laboratorium

Edit publication