<XML><RECORDS><RECORD><REFERENCE_TYPE>0</REFERENCE_TYPE><REFNUM>7173</REFNUM><AUTHORS><AUTHOR>Calder,M.</AUTHOR><AUTHOR>Miller,A.</AUTHOR></AUTHORS><YEAR>2004</YEAR><TITLE>Detecting feature interactions: how many components do we need?</TITLE><PLACE_PUBLISHED>Objects, Agents and Features. Lecture Notes in Computing Science. Volume 2975</PLACE_PUBLISHED><PUBLISHER>Springer Verlag</PUBLISHER><PAGES>45-66</PAGES><ISBN>0302-9743</ISBN><LABEL>Calder:2004:7173</LABEL><KEYWORDS><KEYWORD>feature interaction</KEYWORD></KEYWORDS<ABSTRACT>Features are a structuring mechanism for additional functionality, usually in response to changing requirements. When several features are invoked at the same time, by the same, or different components, the features may not interwork. This is known as feature interaction. We employ a property-based approach to feature interaction detection: this involves checking the validity (or not) of a temporal property against a given system model. We use the logic LTL for temporal properties and the model-checker Spin to prove properties. To gain any real insight into feature interactions, it is important to be able to infer properties for networks of any size, regardless of the underlying communication structure. We present an inference mechanism based on abstraction. The key idea is to model-check a system consisting of a constant number (m) of components together with an abstract component representing any number of other (possibly featured) components. The approach is applied to two systems with communication which is peer to peer and client server. We outline a proof of correctness in both cases. The techniques developed here are motivated by feature interaction analysis, but they are also applicable to reasoning about networks of other types of components with suitable notions of data abstraction.</ABSTRACT></RECORD></RECORDS></XML>