<XML><RECORDS><RECORD><REFERENCE_TYPE>3</REFERENCE_TYPE><REFNUM>6950</REFNUM><AUTHORS><AUTHOR>Miller,A.</AUTHOR><AUTHOR>Calder,M.</AUTHOR></AUTHORS><YEAR>2003</YEAR><TITLE>An application of abstraction and induction techniques to degenerating systems of processes</TITLE><PLACE_PUBLISHED> Proceedings of the International Workshop on Model-Checking for Dependable Software-Intensive Systems (MCDSIS`03), supplement to the Proceedings of DSN-2003 </PLACE_PUBLISHED><PUBLISHER>IEEE Computer Society Press</PUBLISHER><PAGES>W75 - W79</PAGES><LABEL>Miller:2003:6950</LABEL><KEYWORDS><KEYWORD>verification</KEYWORD></KEYWORDS<ABSTRACT>The tree identify phase (TIP) of the IEEE FireWire protocol is an example of a degenerating system of processes. Once a process has sent an acknowledgement to its neighbour it no longer plays any part in the protocol. In this paper we show how this degenerative nature of the protocol can be exploited to prove that certain properties that hold for a model of a small, fixed number of processes following the TIP, hold for the corresponding model of size N, for any N greater than 2. We also prove a similar result, for a different set of properties, via abstraction combined with the construction of an `abstract' model. </ABSTRACT></RECORD></RECORDS></XML>