Compositional verification allows a system to be verified indirectly by verifying the individual components of the system. The key step is to ensure that the decomposition of the system specification into component specifications is correct. That is, it needs to be verified that the composition of the component specifications refines the system specification. In many cyber-physical systems, specifications are probabilistic in nature. For instance, a specification might state that the probability of reaching an unsafe state within 10.000 h shall be less than 0.05. Verifying refinement under such assumptions requires techniques beyond traditional 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 verifying refinement between such specifications. The algorithm utilizes a reduction to the language emptiness problem, making the algorithm terminate after a finite number of computations.