Feature Interaction Verification Using Unbounded Model Checking with Interpolation
-
- MATSUO Takafumi
- Graduate School of Information Science and Technology, Osaka University
-
- TSUCHIYA Tatsuhiro
- Graduate School of Information Science and Technology, Osaka University
-
- KIKUNO Tohru
- Graduate School of Information Science and Technology, Osaka University
この論文をさがす
抄録
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.
収録刊行物
-
- IEICE Transactions on Information and Systems
-
IEICE Transactions on Information and Systems E92-D (6), 1250-1259, 2009
一般社団法人 電子情報通信学会
- Tweet
詳細情報 詳細情報について
-
- CRID
- 1390282679355630080
-
- NII論文ID
- 10026809795
-
- NII書誌ID
- AA10826272
-
- ISSN
- 17451361
- 09168532
-
- HANDLE
- 11094/27255
-
- 本文言語コード
- en
-
- データソース種別
-
- JaLC
- IRDB
- Crossref
- CiNii Articles
-
- 抄録ライセンスフラグ
- 使用不可