Sciweavers

Share
FMSD
2006

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

10 years 1 months ago
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.
Muffy Calder, Alice Miller
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where FMSD
Authors Muffy Calder, Alice Miller
Comments (0)
books