Using symbolic model checking to detect service interactions in telecommunication services

Abstract

Feature interaction is a kind of inconsistent conflict between multiple communication services. In this paper we present an automatic method for detecting feature interactions in service specifications. This method is based on symbolic model checking which can perform verification bysy mbolicallyrepresen ting the search space with binarydecision diagrams. Experimental results show that the method outperforms a previous method based on explicit state traversal, in terms of time and memoryrequired for detection.