Where academic tradition
meets the exciting future

Formalising UML State Machines for Model Checking

Johan Lilius, Ivan Porres, Formalising UML State Machines for Model Checking. In: UML'99 The Unified Modeling Language, Lecture Notes in Computer Science, 430–445, Springer, 1999.


The paper discusses a complete formalisation of UML state machine semantics. This formalisation is given in terms of an operational semantics and it can be used as the basis for code generation, simulation and verification tools for UML Statecharts diagrams. The formalisation is done in two steps. First, the structure of a UML state machine is translated into a term rewriting system. In the second step, the operational semantics of state machines is defined. In addition, some problematic situations that may arise are discussed. Our formalisation is able to deal with all the features of UML state machines and it has been implemented in the vUML tool, a tool for model-checking UML models.

BibTeX entry:

  title = {Formalising UML State Machines for Model Checking},
  booktitle = {UML'99 The Unified Modeling Language},
  author = {Lilius, Johan and Porres, Ivan},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  pages = {430–445},
  year = {1999},
  keywords = {UML, Statecharts, modelchecking},

Belongs to TUCS Research Unit(s): Embedded Systems Laboratory (ESLAB), Software Construction Laboratorium

Publication Forum rating of this publication: level 1

Edit publication