<?xml version="1.0" encoding="UTF-8"?><?xml-stylesheet type="text/xsl" href="static/style.xsl"?><OAI-PMH xmlns="http://www.openarchives.org/OAI/2.0/" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://www.openarchives.org/OAI/2.0/ http://www.openarchives.org/OAI/2.0/OAI-PMH.xsd"><responseDate>2026-06-27T22:27:49Z</responseDate><request verb="GetRecord" identifier="oai:docta.ucm.es:20.500.14352/60342" metadataPrefix="qdc">https://docta.ucm.es/rest/oai/request</request><GetRecord><record><header><identifier>oai:docta.ucm.es:20.500.14352/60342</identifier><datestamp>2023-08-27T19:53:18Z</datestamp><setSpec>com_20.500.14352_14</setSpec><setSpec>col_20.500.14352_15</setSpec></header><metadata><qdc:qualifieddc xmlns:qdc="http://dspace.org/qualifieddc/" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:dcterms="http://purl.org/dc/terms/" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:doc="http://www.lyncode.com/xoai" xsi:schemaLocation="http://purl.org/dc/elements/1.1/ http://dublincore.org/schemas/xmls/qdc/2006/01/06/dc.xsd http://purl.org/dc/terms/ http://dublincore.org/schemas/xmls/qdc/2006/01/06/dcterms.xsd http://dspace.org/qualifieddc/ http://www.ukoln.ac.uk/metadata/dcmi/xmlschema/qualifieddc.xsd">
   <dc:title>The Leader Election Protocol of IEEE 1394 in Maude</dc:title>
   <dc:creator>Verdejo López, José Alberto</dc:creator>
   <dc:creator>Pita Andreu, María Isabel</dc:creator>
   <dc:creator>Martí Oliet, Narciso</dc:creator>
   <dcterms:abstract>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.</dcterms:abstract>
   <dcterms:dateAccepted>2023-06-20T20:29:02Z</dcterms:dateAccepted>
   <dcterms:available>2023-06-20T20:29:02Z</dcterms:available>
   <dcterms:created>2023-06-20T20:29:02Z</dcterms:created>
   <dcterms:issued>2001-07</dcterms:issued>
   <dc:type>journal article</dc:type>
   <dc:identifier>https://hdl.handle.net/20.500.14352/60342</dc:identifier>
   <dc:identifier>XXXX-XXXX</dc:identifier>
   <dc:language>eng</dc:language>
   <dc:rights>open access</dc:rights>
</qdc:qualifieddc></metadata></record></GetRecord></OAI-PMH>