We use tuples of extended class, object and statechart UML diagrams as UML specifications of real-time systems. The semantics
of the UML specification is defined by transformation to the eXtended Timed Graphs (XTG). The correctness of our transformation
is demonstrated by showing that the XTG computation tree can be projected into the computation tree of the corresponding UML
specification. The transformation opens the possibility to specify temporal-logic properties at the UML level and to verify
them at the XTG level using the PMC model checker.