<XML><RECORDS><RECORD><REFERENCE_TYPE>10</REFERENCE_TYPE><REFNUM>8203</REFNUM><AUTHORS><AUTHOR>Miller,A.</AUTHOR><AUTHOR>Calder,M.</AUTHOR></AUTHORS><YEAR>2006</YEAR><TITLE>Verifying parameterised networks by abstraction and induction: experience from the IEEE 1394 protocol</TITLE><PLACE_PUBLISHED>DCS Technical Report Series</PLACE_PUBLISHED><PUBLISHER>Dept of Computing Science, University of Glasgow</PUBLISHER><PAGES>39</PAGES><ISBN>TR-2006-220</ISBN><LABEL>Miller:2006:8203</LABEL><KEYWORDS><KEYWORD>firewire</KEYWORD></KEYWORDS<ABSTRACT>We present two techniques for reasoning about the behaviour of arbitrary-sized networks of concurrent, communicating processes, and apply them to the IEEE 1394 tree identity protocol. The first technique involves the construction of a network invariant and combines data and behavioural abstraction with model checking to generalise indexed safety properties and existential liveness properties for networks with a star topology of any size. We show how this approach can be extended to systems whose topology belongs to any of a set of families (of acyclic topologies). The second technique is a lightweight induction approach in which we exploit the degenerative nature of the protocol. This novel approach uses induction to generalise unindexed liveness properties for all acyclic networks of any size.</ABSTRACT></RECORD></RECORDS></XML>