Feature Interaction Detection by Bounded Model Checking

Tomoyuki YOKOGAWA; Tatsuhiro TSUCHIYA; Masahide NAKAMURA; Tohru KIKUNO

Feature Interaction Detection by Bounded Model Checking

Tomoyuki YOKOGAWA, Tatsuhiro TSUCHIYA, Masahide NAKAMURA, Tohru KIKUNO

Full Text Views

0

Share
Cite this

Summary :

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.

Publication: IEICE TRANSACTIONS on Information Vol.E86-D No.12 pp.2579-2587

Publication Date: 2003/12/01

Publicized

Online ISSN

DOI

Type of Manuscript: Special Section PAPER (Special Issue on Dependable Computing)

Category: Dependable Communication

Cite this

Copy

Tomoyuki YOKOGAWA, Tatsuhiro TSUCHIYA, Masahide NAKAMURA, Tohru KIKUNO, "Feature Interaction Detection by Bounded Model Checking" in IEICE TRANSACTIONS on Information, vol. E86-D, no. 12, pp. 2579-2587, December 2003, doi: .
Abstract: 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.
URL: https://globals.ieice.org/en_transactions/information/10.1587/e86-d_12_2579/_p

Copy

@ARTICLE{e86-d_12_2579,
author={Tomoyuki YOKOGAWA, Tatsuhiro TSUCHIYA, Masahide NAKAMURA, Tohru KIKUNO, },
journal={IEICE TRANSACTIONS on Information},
title={Feature Interaction Detection by Bounded Model Checking},
year={2003},
volume={E86-D},
number={12},
pages={2579-2587},
abstract={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.},
keywords={},
doi={},
ISSN={},
month={December},}

Copy

TY - JOUR
TI - Feature Interaction Detection by Bounded Model Checking
T2 - IEICE TRANSACTIONS on Information
SP - 2579
EP - 2587
AU - Tomoyuki YOKOGAWA
AU - Tatsuhiro TSUCHIYA
AU - Masahide NAKAMURA
AU - Tohru KIKUNO
PY - 2003
DO -
JO - IEICE TRANSACTIONS on Information
SN -
VL - E86-D
IS - 12
JA - IEICE TRANSACTIONS on Information
Y1 - December 2003
AB - 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.
ER -