Transition-based coverage estimation for symbolic model checking

Xingwen Xu; Shinji Kimura; Kazunari Horikawa; Takehiko Tsuchiya

doi:10.1145/1118299.1118303

Transition-based coverage estimation for symbolic model checking

Xingwen Xu^*, Shinji Kimura, Kazunari Horikawa, Takehiko Tsuchiya

^*この研究の対応する著者

大学院情報生産システム研究科

研究成果: Conference contribution

12 被引用数 (Scopus)

抄録

Lack of complete formal specification is one of the major obstacles for the deployment of model checking. Coverage estimation addresses this issue by revealing the unverified part of the design according to the specified properties. In this paper we propose a new transition-based coverage metric to evaluate the completeness of properties for symbolic model checking. It is more comprehensive and accurate than the existing coverage metrics for model checking. An efficient symbolic algorithm is presented for computing the transition coverage for a subset of ACTL. Our coverage estimator has been applied to the model checking of a cache coherence protocol. We uncovered several coverage holes including one that eventually led to the discovery of a design bug.

本文言語	English
ホスト出版物のタイトル	Proceedings of the ASP-DAC 2006
ホスト出版物のサブタイトル	Asia and South Pacific Design Automation Conference 2006
出版社	Institute of Electrical and Electronics Engineers Inc.
ページ	1-6
ページ数	6
ISBN（印刷版）	0780394518, 9780780394513
DOI	https://doi.org/10.1145/1118299.1118303
出版ステータス	Published - 2006
イベント	ASP-DAC 2006: Asia and South Pacific Design Automation Conference 2006 - Yokohama, Japan 継続期間: 2006 1月 24 → 2006 1月 27

出版物シリーズ

名前	Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC
巻	2006

Conference

Conference	ASP-DAC 2006: Asia and South Pacific Design Automation Conference 2006
国/地域	Japan
City	Yokohama
Period	06/1/24 → 06/1/27

ASJC Scopus subject areas

コンピュータサイエンスの応用
コンピュータグラフィックスおよびコンピュータ支援設計
電子工学および電気工学

文献へのアクセス

10.1145/1118299.1118303

他のファイルとリンク

引用スタイル

Xu, X., Kimura, S., Horikawa, K., & Tsuchiya, T. (2006). Transition-based coverage estimation for symbolic model checking. In Proceedings of the ASP-DAC 2006: Asia and South Pacific Design Automation Conference 2006 (pp. 1-6). 記事 1594636 (Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC; Vol. 2006). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1145/1118299.1118303

Transition-based coverage estimation for symbolic model checking. / Xu, Xingwen; Kimura, Shinji; Horikawa, Kazunari その他.
Proceedings of the ASP-DAC 2006: Asia and South Pacific Design Automation Conference 2006. Institute of Electrical and Electronics Engineers Inc., 2006. p. 1-6 1594636 (Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC; Vol. 2006).

研究成果: Conference contribution

Xu, X, Kimura, S, Horikawa, K & Tsuchiya, T 2006, Transition-based coverage estimation for symbolic model checking. in Proceedings of the ASP-DAC 2006: Asia and South Pacific Design Automation Conference 2006., 1594636, Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC, vol. 2006, Institute of Electrical and Electronics Engineers Inc., pp. 1-6, ASP-DAC 2006: Asia and South Pacific Design Automation Conference 2006, Yokohama, Japan, 06/1/24. https://doi.org/10.1145/1118299.1118303

Xu X, Kimura S, Horikawa K, Tsuchiya T. Transition-based coverage estimation for symbolic model checking. In Proceedings of the ASP-DAC 2006: Asia and South Pacific Design Automation Conference 2006. Institute of Electrical and Electronics Engineers Inc. 2006. p. 1-6. 1594636. (Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC). doi: 10.1145/1118299.1118303

Xu, Xingwen ; Kimura, Shinji ; Horikawa, Kazunari その他. / Transition-based coverage estimation for symbolic model checking. Proceedings of the ASP-DAC 2006: Asia and South Pacific Design Automation Conference 2006. Institute of Electrical and Electronics Engineers Inc., 2006. pp. 1-6 (Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC).

@inproceedings{e4826b9780d24d718d665843ac699a14,

title = "Transition-based coverage estimation for symbolic model checking",

abstract = "Lack of complete formal specification is one of the major obstacles for the deployment of model checking. Coverage estimation addresses this issue by revealing the unverified part of the design according to the specified properties. In this paper we propose a new transition-based coverage metric to evaluate the completeness of properties for symbolic model checking. It is more comprehensive and accurate than the existing coverage metrics for model checking. An efficient symbolic algorithm is presented for computing the transition coverage for a subset of ACTL. Our coverage estimator has been applied to the model checking of a cache coherence protocol. We uncovered several coverage holes including one that eventually led to the discovery of a design bug.",

author = "Xingwen Xu and Shinji Kimura and Kazunari Horikawa and Takehiko Tsuchiya",

year = "2006",

doi = "10.1145/1118299.1118303",

language = "English",

isbn = "0780394518",

series = "Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "1--6",

booktitle = "Proceedings of the ASP-DAC 2006",

note = "ASP-DAC 2006: Asia and South Pacific Design Automation Conference 2006 ; Conference date: 24-01-2006 Through 27-01-2006",

}

TY - GEN

T1 - Transition-based coverage estimation for symbolic model checking

AU - Xu, Xingwen

AU - Kimura, Shinji

AU - Horikawa, Kazunari

AU - Tsuchiya, Takehiko

PY - 2006

Y1 - 2006

N2 - Lack of complete formal specification is one of the major obstacles for the deployment of model checking. Coverage estimation addresses this issue by revealing the unverified part of the design according to the specified properties. In this paper we propose a new transition-based coverage metric to evaluate the completeness of properties for symbolic model checking. It is more comprehensive and accurate than the existing coverage metrics for model checking. An efficient symbolic algorithm is presented for computing the transition coverage for a subset of ACTL. Our coverage estimator has been applied to the model checking of a cache coherence protocol. We uncovered several coverage holes including one that eventually led to the discovery of a design bug.

AB - Lack of complete formal specification is one of the major obstacles for the deployment of model checking. Coverage estimation addresses this issue by revealing the unverified part of the design according to the specified properties. In this paper we propose a new transition-based coverage metric to evaluate the completeness of properties for symbolic model checking. It is more comprehensive and accurate than the existing coverage metrics for model checking. An efficient symbolic algorithm is presented for computing the transition coverage for a subset of ACTL. Our coverage estimator has been applied to the model checking of a cache coherence protocol. We uncovered several coverage holes including one that eventually led to the discovery of a design bug.

UR - http://www.scopus.com/inward/record.url?scp=33748594435&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=33748594435&partnerID=8YFLogxK

U2 - 10.1145/1118299.1118303

DO - 10.1145/1118299.1118303

M3 - Conference contribution

AN - SCOPUS:33748594435

SN - 0780394518

SN - 9780780394513

T3 - Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC

SP - 1

EP - 6

BT - Proceedings of the ASP-DAC 2006

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - ASP-DAC 2006: Asia and South Pacific Design Automation Conference 2006

Y2 - 24 January 2006 through 27 January 2006

ER -

Transition-based coverage estimation for symbolic model checking

抄録

出版物シリーズ

Conference

ASJC Scopus subject areas

文献へのアクセス

他のファイルとリンク

フィンガープリント

引用スタイル