Transition-based coverage estimation for symbolic model checking

Xingwen Xu, Shinji Kimura, Kazunari Horikawa, Takehiko Tsuchiya

Research output: Chapter in Book/Report/Conference proceedingConference contribution

10 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 languageEnglish
Title of host publicationProceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC
Pages1-6
Number of pages6
Volume2006
Publication statusPublished - 2006
EventASP-DAC 2006: Asia and South Pacific Design Automation Conference 2006 - Yokohama
Duration: 2006 Jan 242006 Jan 27

Other

OtherASP-DAC 2006: Asia and South Pacific Design Automation Conference 2006
CityYokohama
Period06/1/2406/1/27

Fingerprint

Model checking
Network protocols

ASJC Scopus subject areas

  • Engineering(all)

Cite this

Xu, X., Kimura, S., Horikawa, K., & Tsuchiya, T. (2006). Transition-based coverage estimation for symbolic model checking. In Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC (Vol. 2006, pp. 1-6). [1594636]

Transition-based coverage estimation for symbolic model checking. / Xu, Xingwen; Kimura, Shinji; Horikawa, Kazunari; Tsuchiya, Takehiko.

Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC. Vol. 2006 2006. p. 1-6 1594636.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Xu, X, Kimura, S, Horikawa, K & Tsuchiya, T 2006, Transition-based coverage estimation for symbolic model checking. in Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC. vol. 2006, 1594636, pp. 1-6, ASP-DAC 2006: Asia and South Pacific Design Automation Conference 2006, Yokohama, 06/1/24.
Xu X, Kimura S, Horikawa K, Tsuchiya T. Transition-based coverage estimation for symbolic model checking. In Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC. Vol. 2006. 2006. p. 1-6. 1594636
Xu, Xingwen ; Kimura, Shinji ; Horikawa, Kazunari ; Tsuchiya, Takehiko. / Transition-based coverage estimation for symbolic model checking. Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC. Vol. 2006 2006. pp. 1-6
@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",
language = "English",
isbn = "0780394518",
volume = "2006",
pages = "1--6",
booktitle = "Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC",

}

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

M3 - Conference contribution

SN - 0780394518

SN - 9780780394513

VL - 2006

SP - 1

EP - 6

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

ER -