But what if I don't want to wait forever?

Citation

Fidge C & Shankland C (2003) But what if I don't want to wait forever?. Formal Aspects of Computing, 14 (3), pp. 281-294. https://doi.org/10.1007/s001650300006

Abstract
We present an abstract model of the leader election protocol used in the IEEE 1394 High Performance Serial Bus standard. The model is expressed in the probabilistic Guarded Command Language. By formal reasoning based on this description, we establish the probability of the root contention part of the protocol successfully terminating in terms of the number of attempts to do so. Some simple calculations then allow us to establish an upper bound on the time taken for those attempts.

Keywords
Formal specification; IEEE 1394; IEEE 1394a; Probabilistic reasoning; Verification

Journal
Formal Aspects of Computing: Volume 14, Issue 3