Transition-based coverage estimation for symbolic model checking

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

*Corresponding author for this work

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

12 Citations (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.

Original languageEnglish
Title of host publicationProceedings of the ASP-DAC 2006
Subtitle of host publicationAsia and South Pacific Design Automation Conference 2006
PublisherInstitute of Electrical and Electronics Engineers Inc.
Number of pages6
ISBN (Print)0780394518, 9780780394513
Publication statusPublished - 2006
EventASP-DAC 2006: Asia and South Pacific Design Automation Conference 2006 - Yokohama, Japan
Duration: 2006 Jan 242006 Jan 27

Publication series

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


ConferenceASP-DAC 2006: Asia and South Pacific Design Automation Conference 2006

ASJC Scopus subject areas

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


Dive into the research topics of 'Transition-based coverage estimation for symbolic model checking'. Together they form a unique fingerprint.

Cite this