zbMATH — the first resource for mathematics

The leader election protocol of IEEE 1394 in Maude. (English) Zbl 0962.68107
Futatsugi, Kokichi, The 3rd international workshop on rewriting logic and its applications, RWLW. Kanazawa City Cultural Hall, Kanzawa, Japan, September 18-20, 2000. Amsterdam: Elsevier, Electronic Notes in Theoretical Computer Science. 36, 22 p., electronic only (2000).
Summary: We consider two descriptions in Maude of the leader election protocol from the IEEE 1394 serial multimedia bus. Particularly, the time aspects of the protocol are studied. The descriptions are first validated by an exhaustive exploration of all the possible behaviors and states reachable from an initial configuration of a network, checking that always only one leader is chosen. As a final step for proving the correctness of the protocol we give a formal proof showing that the desirable properties of the protocol are always fulfilled.
For the entire collection see [Zbl 0957.00046].

68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: Link