Transition-based coverage estimation for symbolic model checking

Xingwen Xu, Shinji Kimura, Kazunari Horikawa, Takehiko Tsuchiya

研究成果: Conference contribution

10 被引用数 (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
出版ステータスPublished - 2006
イベントASP-DAC 2006: Asia and South Pacific Design Automation Conference 2006 - Yokohama, Japan
継続期間: 2006 1 242006 1 27

出版物シリーズ

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

Conference

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

ASJC Scopus subject areas

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

フィンガープリント 「Transition-based coverage estimation for symbolic model checking」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル