Abstract. The interplay of real-time and probability is crucial to the correctness of the IEEE 1394 FireWire root contention protocol. We present a formal verification of the protocol using probabilistic model checking. Rather than analyze the functional aspects of the protocol, by asking such questions as "will a leader be elected?", we focus on the protocol's performance, by asking the question "how certain are we that a leader will be elected sufficiently quickly?" Probabilistic timed automata are used to formally model and verify the protocol against properties which require that a leader is elected before a deadline with a certain probability. We use techniques such as abstraction, reachability analysis, and integer-time semantics to aid the model-checking process, and the efficacy of these techniques is compared.