Formal Modelling and Analysis of Probabilistic Real-Time Systems