But what if I don’t want to wait forever? (English) Zbl 1029.68015

Fidge, Colin; Shankland, Carron

Formal Asp. Comput. 14, No. 3, 281-294 (2002).

Summary: 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.

MSC:

68M12	Network protocols
68Q65	Abstract data types; algebraic specification

Keywords:

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

Software:

Uppaal2k