×

zbMATH — the first resource for mathematics

But what if I don’t want to wait forever? (English) Zbl 1029.68015
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
Software:
Uppaal2k
PDF BibTeX XML Cite
Full Text: DOI