Model Checking UML State Machines and Collaborations

Timm Schäfer, Alexander Knapp, Stephan Merz

Abstract

The Unified Modeling Language provides two complementary notations, state machines and collaborations, for the specification of dynamic system behavior. We describe a prototype tool, Hugo, that is designed to automatically verify whether the interactions expressed by a collaboration can indeed be realized by a set of state machines. We compile state machines into a Promela model and collaborations into sets of Büchi automata (``never claims''). The model checker Spin is called upon to verify the model against the automata.

Note

This paper describes the original version of Hugo, based on an interpretater for the UML meta model. The implementation has since changed completely, and is much more efficient.

© Elsevier 2001

Available as: PDF

See also: Hugo project

Reference

@Article{schaefer:model-checking-uml,
  author =  {Timm Sch{\"a}fer and Alexander Knapp and Stephan Merz},
  title =   {Model checking {UML} state machines and collaborations},
  journal = {Electronic Notes in Theoretical Computer Science},
  year =    2001,
  volume =  55,
  number =  3,
  pages =   {13 pages}
}