Based on the Duration Calculus, this report introduces a notion of
  timed transition diagrams for modelling real-time systems. The
  semantics M(D) of a timed transition diagram D is defined to be a DC
  formula. High level requirement properties of a real-time system is
  specified as DC formulas and the verification of the satisfaction of
  a property $\varphi$ by a TTD $D$ is done by property in DC the
  implication from M(D) to $\varphi$. The main contribution of the
  paper is to propose a method for verification properties of a timed
  systems, and for proving the refinement of two TTDs by simply
  checking the simulation of single step-transitions together with the
  calculation of the time bounds of paths of transitions.

  Key Words: Real-Time Systems, Duration Calculus, Timed Transition
  Diagrams, Specification, Refinement.