2026-06-27T10:10:53Zhttps://docta.ucm.es/rest/oai/requestoai:docta.ucm.es:20.500.14352/603422023-08-27T19:53:18Zcom_20.500.14352_14col_20.500.14352_15
Docta Complutense
author
Verdejo López, José Alberto
author
Pita Andreu, María Isabel
author
Martí Oliet, Narciso
2023-06-20T20:29:02Z
2023-06-20T20:29:02Z
2001-07
https://hdl.handle.net/20.500.14352/60342
In this paper we consider three descriptions, at different abstract levels, of the
leader election protocol from the IEEE 1394 serial multimedia bus. The descriptions
are given using the language Maude based on rewriting logic. 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. The correctness
of the protocol is showed by a formal proof that the desirable properties of
the protocol are always fulfilled.
eng
The Leader Election Protocol of IEEE 1394 in Maude
journal article
URL
https://docta.ucm.es/bitstreams/cde36cab-5f9e-4f98-b725-d3aa2a7e2148/download
File
MD5
6fa423f5ee7ef28f464edbb322a106e4
311649
application/pdf
04-TR-118-01-fw.pdf
URL
https://docta.ucm.es/bitstreams/a0c5076e-c214-4c55-a738-633a601d19f0/download
File
MD5
12875cd4c3c3d606dbd7ff1019239b18
87007
text/plain
04-TR-118-01-fw.pdf.txt