<XML><RECORDS><RECORD><REFERENCE_TYPE>0</REFERENCE_TYPE><REFNUM>6616</REFNUM><AUTHORS><AUTHOR>Calder,M.</AUTHOR><AUTHOR>Miller,A.</AUTHOR></AUTHORS><YEAR>2003</YEAR><TITLE>Using SPIN to Analyse the Tree Identification phase of the IEEE 1394 High Performance Serial Bus (FireWire) Protocol</TITLE><PLACE_PUBLISHED> Formal Aspects of Computing 14 (2003) 3 </PLACE_PUBLISHED><PUBLISHER>Springer Verlag</PUBLISHER><PAGES>247--266</PAGES><ISBN>0934-5043</ISBN><LABEL>Calder:2003:6616</LABEL><KEYWORDS><KEYWORD>model-checking</KEYWORD></KEYWORDS<ABSTRACT>We describe in detail how the Tree Identification phase of the IEEE 1394 High Performance Serial Bus (FireWire) protocol is modelled in Promela and verified using SPIN. Initial ideas concerning the inductive verification of arbitrary system configurations are discussed. </ABSTRACT></RECORD></RECORDS></XML>