This paper describes work in progress performed as part of an ongoing project

concerned with the verification of soft deadlines of timed systems. More precisely,

our aim is to provide theoretical foundations and model checking algorithms for

the formal verification of 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 of Kwiatkowska et. al. 1999, an extension of timed automata

of Alur and Dill 94, and includes: model checking of discrete-probabilistic automata

based on the region graph construction; symbolic methods based on forwards and

backwards reachability; and continuous probabilistic timed automata.