Feature interaction detection by pairwise analysis of LTL properties - A case study

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 in both 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.