The Leader Election Protocol of IEEE 1394 in Maude

In this paper 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.

• Type: Journal
• Year: 2000
• Where: ENTCS
• Authors: Alberto Verdejo, Isabel Pita, Narciso Martí-Oliet
• Keywords: ENTCS 2000, IEEE 1394, Leader Election Protocol, Serial Multimedia Bus