The Leader Election Protocol of IEEE 1394 in Maude

Alberto Verdejo, Isabel Pita, and Narciso Martí-Oliet

In K. Futatsugi, editor, Proceedings Third International Workshop on Rewriting Logic and its Applications, WRLA 2000, Kanazawa, Japan, September 18-20, 2000, volume 36 of Electronic Notes in Theoretical Computer Science, pages 385-406. Elsevier, 2000.

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

  [pdf]

@InProceedings{VerdejoPitaMarti-Oliet00,
  author =       {A. Verdejo and I. Pita and N. Mart{\'\i}-Oliet},
  title =        {The Leader Election Protocol of {IEEE} 1394 in {Maude}},
  booktitle =    {Proceedings Third International Workshop on Rewriting
                  Logic and its Applications, WRLA 2000, Kanazawa, Japan,
                  September 18--20, 2000},
  year =         2000,
  editor =       {Kokichi Futatsugi},
  volume =       36,
  publisher =    {Elsevier},
  series =       {Electronic Notes in Theoretical Computer Science},
  pages =        {385-406}
}