Model Checking Timed UML State Machines and Collaborations

Alexander Knapp, Stephan Merz, Christopher Rauh
We describe a prototype tool, Hugo/RT, that is designed to automatically verify whether the timed state machines in a UML model interact according to scenarios specified by time-annotated UML collaborations. Timed state machines are compiled into timed automata that exchange signals and operations via a network automaton. A collaboration with time constraints is translated into an observer timed automaton. The model checker Uppaal is called upon to verify the timed automata representing the model against the observer timed automaton.
© Springer-Verlag 2002
Available as: PDF
See also: Hugo project
  author =    {Alexander Knapp and Stephan Merz and Christopher Rauh},
  title =     {Model Checking Timed {UML} State Machines and Collaborations},
  booktitle = {7th Intl.\ Symp.\ Formal Techniques in Real-Time and Fault 
               Tolerant Systems (FTRTFT 2002)},
  pages =     {395--414},
  year =      2002,
  editor =    {W. Damm and E.-R. Olderog},
  volume =    2469,
  series =    {Lecture Notes in Computer Science},
  address =   {Oldenburg, Germany},
  month =     sep,
  publisher = {Springer-Verlag}

Stephan Merz