Probabilistic Model Checking of Deadline Properties in the IEEE 1394 FireWire Root Contention Protocol

The interplay of real-time and probability is crucial to the correctness of the IEEE 1394 FireWire root contention protocol. We present a formal veri cation 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 suciently 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 modelchecking process, and the ecacy of these techniques is compared