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
Neste artigo, propomos um método de verificação de modelo ilimitado para verificação de interação de recursos para sistemas de telecomunicações. A verificação ilimitada de modelos é um método de verificação baseado em SAT e tem atraído atenção recente como uma abordagem poderosa. A abordagem baseada em interpolação é um dos métodos de verificação de modelo ilimitado mais promissores e provou ser eficaz para verificação de hardware. No entanto, a aplicação de verificação ilimitada de modelos a sistemas assíncronos, como sistemas de telecomunicações, raramente tem sido praticada. Isto porque, com a codificação convencional, o comportamento de um sistema assíncrono só pode ser representado como uma grande fórmula proposicional, resultando assim em grande custo computacional. Para superar este problema propomos utilizar um novo esquema para codificar o comportamento do sistema e adaptar o algoritmo de verificação de modelo ilimitado a esta codificação. Ao explorar a simultaneidade de um sistema assíncrono, este esquema de codificação permite uma fórmula muito concisa para representar o comportamento do sistema. Para demonstrar a eficácia da nossa abordagem, conduzimos experimentos onde 21 pares de serviços de telecomunicações são verificados usando vários métodos, incluindo o nosso. Os resultados mostram que nossa abordagem apresenta uma aceleração significativa em relação à verificação ilimitada de modelos usando a codificação tradicional.
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.
Copiar
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
Copiar
@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},}
Copiar
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 -