Model Checking UML State Machines and Collaborations

Timm Schäfer, Alexander Knapp, Stephan Merz
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.
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
  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}

Stephan Merz
Last modified: Sun Feb 16 10:39:42 MET 2003