Combining UML and formal notations for modelling real-time systems