Affordable Access

Model Checking Timed UML State Machines and Collaborations

IFIP Lecture Notes in Computer Science (LNCS)
Publication Date
  • Design


We describe a prototype tool, /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 is called upon to verify the timed automata representing the model against the observer timed automaton.Full Text at Springer, may require registration or fee

There are no comments yet on this publication. Be the first to share your thoughts.