The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. ex. Some numerals are expressed as "XNUMX".
Copyrights notice
The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. Copyrights notice
Dans cet article, nous proposons une méthode de vérification de modèle illimitée pour la vérification des interactions de fonctionnalités pour les systèmes de télécommunication. La vérification de modèle illimitée est une méthode de vérification basée sur SAT et a récemment attiré l'attention en tant qu'approche puissante. L'approche basée sur l'interpolation est l'une des méthodes de vérification de modèle illimitée les plus prometteuses et s'est avérée efficace pour la vérification du matériel. Cependant, l’application de la vérification illimitée des modèles aux systèmes asynchrones, tels que les systèmes de télécommunications, a rarement été pratiquée. En effet, avec le codage conventionnel, le comportement d'un système asynchrone ne peut être représenté que sous la forme d'une grande formule propositionnelle, ce qui entraîne un coût de calcul important. Pour surmonter ce problème, nous proposons d'utiliser un nouveau schéma de codage du comportement du système et d'adapter l'algorithme de modélisation illimitée à cet encodage. En exploitant la concurrence d'un système asynchrone, ce schéma de codage permet d'utiliser une formule très concise pour représenter le comportement du système. Pour démontrer l'efficacité de notre approche, nous menons des expériences où 21 paires de services de télécommunication sont vérifiées à l'aide de plusieurs méthodes dont la nôtre. Les résultats montrent que notre approche présente une accélération significative par rapport à la vérification de modèle illimitée utilisant l'encodage traditionnel.
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Copier
Takafumi MATSUO, Tatsuhiro TSUCHIYA, Tohru KIKUNO, "Feature Interaction Verification Using Unbounded Model Checking with Interpolation" in IEICE TRANSACTIONS on Information,
vol. E92-D, no. 6, pp. 1250-1259, June 2009, doi: 10.1587/transinf.E92.D.1250.
Abstract: In this paper, we propose an unbounded model checking method for feature interaction verification for telecommunication systems. Unbounded model checking is a SAT-based verification method and has attracted recent attention as a powerful approach. The interpolation-based approach is one of the most promising unbounded model checking methods and has been proven to be effective for hardware verification. However, the application of unbounded model checking to asynchronous systems, such as telecommunication systems, has rarely been practiced. This is because, with the conventional encoding, the behavior of an asynchronous system can only be represented as a large propositional formula, thus resulting in large computational cost. To overcome this problem we propose to use a new scheme for encoding the behavior of the system and adapt the unbounded model checking algorithm to this encoding. By exploiting the concurrency of an asynchronous system, this encoding scheme allows a very concise formula to represent system's behavior. To demonstrate the effectiveness of our approach, we conduct experiments where 21 pairs of telecommunication services are verified using several methods including ours. The results show that our approach exhibits significant speed-up over unbounded model checking using the traditional encoding.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.E92.D.1250/_p
Copier
@ARTICLE{e92-d_6_1250,
author={Takafumi MATSUO, Tatsuhiro TSUCHIYA, Tohru KIKUNO, },
journal={IEICE TRANSACTIONS on Information},
title={Feature Interaction Verification Using Unbounded Model Checking with Interpolation},
year={2009},
volume={E92-D},
number={6},
pages={1250-1259},
abstract={In this paper, we propose an unbounded model checking method for feature interaction verification for telecommunication systems. Unbounded model checking is a SAT-based verification method and has attracted recent attention as a powerful approach. The interpolation-based approach is one of the most promising unbounded model checking methods and has been proven to be effective for hardware verification. However, the application of unbounded model checking to asynchronous systems, such as telecommunication systems, has rarely been practiced. This is because, with the conventional encoding, the behavior of an asynchronous system can only be represented as a large propositional formula, thus resulting in large computational cost. To overcome this problem we propose to use a new scheme for encoding the behavior of the system and adapt the unbounded model checking algorithm to this encoding. By exploiting the concurrency of an asynchronous system, this encoding scheme allows a very concise formula to represent system's behavior. To demonstrate the effectiveness of our approach, we conduct experiments where 21 pairs of telecommunication services are verified using several methods including ours. The results show that our approach exhibits significant speed-up over unbounded model checking using the traditional encoding.},
keywords={},
doi={10.1587/transinf.E92.D.1250},
ISSN={1745-1361},
month={June},}
Copier
TY - JOUR
TI - Feature Interaction Verification Using Unbounded Model Checking with Interpolation
T2 - IEICE TRANSACTIONS on Information
SP - 1250
EP - 1259
AU - Takafumi MATSUO
AU - Tatsuhiro TSUCHIYA
AU - Tohru KIKUNO
PY - 2009
DO - 10.1587/transinf.E92.D.1250
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E92-D
IS - 6
JA - IEICE TRANSACTIONS on Information
Y1 - June 2009
AB - In this paper, we propose an unbounded model checking method for feature interaction verification for telecommunication systems. Unbounded model checking is a SAT-based verification method and has attracted recent attention as a powerful approach. The interpolation-based approach is one of the most promising unbounded model checking methods and has been proven to be effective for hardware verification. However, the application of unbounded model checking to asynchronous systems, such as telecommunication systems, has rarely been practiced. This is because, with the conventional encoding, the behavior of an asynchronous system can only be represented as a large propositional formula, thus resulting in large computational cost. To overcome this problem we propose to use a new scheme for encoding the behavior of the system and adapt the unbounded model checking algorithm to this encoding. By exploiting the concurrency of an asynchronous system, this encoding scheme allows a very concise formula to represent system's behavior. To demonstrate the effectiveness of our approach, we conduct experiments where 21 pairs of telecommunication services are verified using several methods including ours. The results show that our approach exhibits significant speed-up over unbounded model checking using the traditional encoding.
ER -