%0 Journal Article
%A Verdejo López, José Alberto
%A Pita Andreu, María Isabel
%A Martí Oliet, Narciso
%T The Leader Election Protocol of IEEE 1394 in Maude
%D 2001
%U https://hdl.handle.net/20.500.14352/60342
%X In this paper we consider three descriptions, at different abstract levels, of theleader election protocol from the IEEE 1394 serial multimedia bus. The descriptionsare given using the language Maude based on rewriting logic. Particularly, the timeaspects of the protocol are studied. The descriptions are first validated by an exhaustiveexploration of all the possible behaviors and states reachable from an initialconfiguration of a network, checking that always only one leader is chosen. The correctnessof the protocol is showed by a formal proof that the desirable properties ofthe protocol are always fulfilled.
%~