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. Keywords communicating processes, distributed systems, model checking, feature interaction, communications services.

• Type: Journal
• Year: 2006
• Where: FMSD
• Authors: Muffy Calder, Alice Miller
• Keywords: Analysis, FMSD 2006, Property Case Explosion, Temporal Properties