Formal Verification of Timed Properties for Randomized Distributed Algorithms