Abstract. This paper describes work in progess performed as part of an ongoing project aimed at the development of theoretical foundations and model checking algorithms for the verification of soft deadlines in timed systems, that is, properties such as "there is a 90% chance that the message will be delivered within 5 time units". The research is focussed on the probabilistic timed automata model, an extension of timed automata , and includes: model checking of discrete-probabilistic automata based on the region graph construction}; symbolic methods based on forwards and backwards reachability; and the continuous probabilistic timed automata.