Using SPIN for feature interaction analysis—a case study
Muffy Calder, Alice Ann Miller · 2001
Abstract. We show how SPIN is applied to analyse the behaviour of a real software artifact { feature interaction in telecommunications ser-vices. We demonstrate how minimal abstraction and optimisation tech-niques can greatly reduce the cost of model-checking, and how analysis can be performed automatically using scripts. Keywords telecommunications services; Promela/SPIN; communicating processes; distributed systems; formal modelling; analysis and reasoning techniques; feature interaction 1