Model Checking Timed UML State Machines and Collaborations

Alexander Knapp, Stephan Merz, Christopher Rauh

Abstract

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

Reference

@InProceedings{knapp:hugo-rt,
  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}
}