[KNS03b] M. Kwiatkowska, G. Norman and J. Sproston. Probabilistic Model Checking of Deadline Properties in the IEEE1394 FireWire Root Contention Protocol. Formal Aspects of Computing, 14(3), pages 295-318. April 2003. [ps.gz] [pdf] [bib]
Downloads:  ps.gz ps.gz (173 KB)  pdf pdf (400 KB)  bib bib
Notes: Further information and verification results are available from the PRISM web page.
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.