<XML><RECORDS><RECORD><REFERENCE_TYPE>0</REFERENCE_TYPE><REFNUM>8117</REFNUM><AUTHORS><AUTHOR>Calder,M.</AUTHOR><AUTHOR>Miller,A.</AUTHOR></AUTHORS><YEAR>2006</YEAR><TITLE>Feature Interaction Detection by Pairwise Analysis of LTL Properties--a case study</TITLE><PLACE_PUBLISHED>Formal Methods in System Design, Volume 28(3), May 2006</PLACE_PUBLISHED><PUBLISHER>Springer</PUBLISHER><PAGES>213--261</PAGES><ISBN>0925-9856 (Paper) 1572-8102 (Onl</ISBN><LABEL>Calder:2006:8117</LABEL><KEYWORDS><KEYWORD>communicating processes</KEYWORD></KEYWORDS<ABSTRACT>A Promela specification and a set of temporal properties are developed for a basic call service with a number of features. The properties are expressed in the logic LTL. Interactions between features are detected by pairwise analysis of features and properties. The analysis quickly results inboth state-space and property case explosion. To overcome this state-spaces are minimised, model checking results generalised through symmetry and bisimulation, and analysis performed automatically using scripts. The result is a more extensive feature interaction analysis than others in the field.</ABSTRACT></RECORD></RECORDS></XML>