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 verification of the protocol using probabilistic model checking. Rather than analyse 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.

Authors and Affiliations

1. School of Computer Science, University of Birmingham, Birmingham, UK, , , , , , GB

   Marta Kwiatkowska & Gethin Norman

2. Dipartimento di Informatica, Università di Torino, Torino, Italy, , , , , , IT

   Jeremy Sproston

Received July 2001/Accepted in revised form November 2002

Correspondence and offprint requests to: Marta Kwiatkowska, School of Computer Science, University of Birmingham, Birmingham B15 2TT, UK. Email: M.Z.Kwiatkowska@cs.bham.ac.uk

Reprints and permissions