Model checking timed UML state machines and collaborations

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.