Compositional verification allows a system to be verified indirectly by verifying the individual components of the system. The keystep is to ensure that the decomposition of the system specification intocomponent specifications is correct. That is, it needs to be verified thatthe composition of the component specifications refines the system specification. In many cyber-physical systems, specifications are probabilisticin nature. For instance, a specification might state that the probabilityof reaching an unsafe state within 10.000 hours shall be less than 0.05.Verifying refinement under such assumptions requires techniques beyondtraditional theorem proving. This paper presents a solution where specifications are built up by probabilistic contracts based upon timed automata. In particular, the main contribution is an algorithm for verifyingrefinement between such specifications. The algorithm utilizes a reduction to the language emptiness problem, making the algorithm terminateafter a finite number of computations