<XML><RECORDS><RECORD><REFERENCE_TYPE>3</REFERENCE_TYPE><REFNUM>7768</REFNUM><AUTHORS><AUTHOR>Calder,M.</AUTHOR><AUTHOR>Miller,A.</AUTHOR></AUTHORS><YEAR>2004</YEAR><TITLE>Verifying parameterised, featured networks by abstraction</TITLE><PLACE_PUBLISHED>Proceedings of the first International Symposium on Leveraging Applications of Formal Methods (ISOLA'04)</PLACE_PUBLISHED><PUBLISHER>N/A</PUBLISHER><PAGES>227--234</PAGES><LABEL>Calder:2004:7768</LABEL><KEYWORDS><KEYWORD>model checking</KEYWORD></KEYWORDS<ABSTRACT>Model-checking is a very effective, formal technique for reasoning about systems. A common limitation with model-checking is how to relate an individual results to the general case, i.e. does a result for a system of a given size scale to a system of any size? This question cannot be answered by model-checking alone, because in general, it is undecidable. However, we have developed techniques to solve the problem for some cases. In this paper we consider the application domain of reasoning about peer to peer, featured networks by model-checking. We have already shown that under certain circumstances, we can reason about the general case using a combination of abstraction and model-checking. The method relies on dividing the set of components into two distinct subsets: observable concrete components, which may have features, and abstract components, which have no features. In this paper we extend the method to allow featured abstract components. This means that the abstract components are no longer isomorphic and so the new technique is considerably more expressive than the original. We specify criteria which the features must fulfill and show that our new approach is sound.</ABSTRACT></RECORD></RECORDS></XML>