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

^*Corresponding author for this work

Graduate School of Information, Production and Systems

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

12 Citations (Scopus)

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.

Original language	English
Title of host publication	Proceedings of the ASP-DAC 2006
Subtitle of host publication	Asia and South Pacific Design Automation Conference 2006
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	1-6
Number of pages	6
ISBN (Print)	0780394518, 9780780394513
DOIs	https://doi.org/10.1145/1118299.1118303
Publication status	Published - 2006
Event	ASP-DAC 2006: Asia and South Pacific Design Automation Conference 2006 - Yokohama, Japan Duration: 2006 Jan 24 → 2006 Jan 27

Publication series

Name	Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC
Volume	2006

Conference

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

ASJC Scopus subject areas

Computer Science Applications
Computer Graphics and Computer-Aided Design
Electrical and Electronic Engineering

Access to Document

10.1145/1118299.1118303

Cite this

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 et al.
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).

Research output: Chapter in Book/Report/Conference proceeding › 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

@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

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this