<XML><RECORDS><RECORD><REFERENCE_TYPE>3</REFERENCE_TYPE><REFNUM>6818</REFNUM><AUTHORS><AUTHOR>Calder,M.</AUTHOR><AUTHOR>Miller,A.</AUTHOR></AUTHORS><YEAR>2001</YEAR><TITLE>Using SPIN to Analyse the FireWire Protocol - a Case Study</TITLE><PLACE_PUBLISHED>Proceedings of the International Workshop on Application of Formal Methods to IEEE 1394 Standard </PLACE_PUBLISHED><PUBLISHER>University of Stirling</PUBLISHER><PAGES>9--13</PAGES><ISBN>1 85769 1539</ISBN><LABEL>Calder:2001:6818</LABEL><KEYWORDS><KEYWORD>verification</KEYWORD></KEYWORDS<ABSTRACT>We describe initial attempts to model the Tree Identification phase of the IEEE 1394 High Performance Serial Bus (aka ``FireWire'') protocol in Promela and to verify properties of the proptocol using SPIN. We demonstrate the analysis techniques that are available with SPIN and the optimisation techniques that we employ to maintain the tractability of the state-space. We also discuss how analysis can be performed automatically using scripts. </ABSTRACT></RECORD></RECORDS></XML>