<XML><RECORDS><RECORD><REFERENCE_TYPE>10</REFERENCE_TYPE><REFNUM>7126</REFNUM><AUTHORS><AUTHOR>Miller,A.</AUTHOR><AUTHOR>Calder,M.</AUTHOR></AUTHORS><YEAR>2003</YEAR><TITLE>Two approaches to verifying the Tree identify phase of the IEEE 1394 (FireWire) protocol for any size of network</TITLE><PLACE_PUBLISHED>DCS Tech Report</PLACE_PUBLISHED><PUBLISHER>Dept of Computing Science, University of Glasgow</PUBLISHER><ISBN>TR-2003-155</ISBN><LABEL>Miller:2003:7126</LABEL><KEYWORDS><KEYWORD>IEEE 1394</KEYWORD></KEYWORDS<ABSTRACT>We describe two techniques for proving properties of the tree identify phase of the IEEE 1394 Tree identify protocol for any size of network. The first approach involves the construction of a network invariant together with data abstraction to prove safety properties for systems with a star configuration and an extension to systems with a configuration belonging to one of a given set of families. The second approach applies to all acyclic configurations and exploits the degenerative nature of the protocol. </ABSTRACT></RECORD></RECORDS></XML>