For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
Feature Interaction Detection by Bounded Model Checking
Tomoyuki YOKOGAWA Tatsuhiro TSUCHIYA Masahide NAKAMURA Tohru KIKUNO
IEICE TRANSACTIONS on Information and Systems
Publication Date: 2003/12/01
Print ISSN: 0916-8532
Type of Manuscript: Special Section PAPER (Special Issue on Dependable Computing)
Category: Dependable Communication
bounded model checking, SAT, feature interaction,
Full Text: PDF(590.3KB)>>
Feature interaction is the term used in telephony systems to refer to inconsistent conflict between multiple communication services. Feature interaction is considered a major obstacle to developing reliable telephony systems and many approaches have been explored to resolve it. In this paper we present an automatic method for detecting latent feature interaction in service specifications. This method uses bounded model checking as its basis. The basic idea behind bounded model checking is to reduce the detection problem to the propositional satisfiability (SAT) decision problem. For asynchronous systems like telecommunication systems, however, traditional bounded model checking does not work well because resulting propositional formulas tend to become very large. We propose a new encoding scheme to overcome this problem and show the effectiveness through comparative experiments with traditional bounded model checking and other model checking methods.