Transition traversal coverage estimation for symbolic model checking

Xingwen Xu, Shinji Kimura, Kazunari Horikawa, Takehiko Tsuchiya

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

Abstract

Model checking can exhaustively verify a set of spec! ed properties on a given implementation. However, it is very hard to determine whether suf dent properties have been speci ed or not. In this paper, we propose a transition traversal coverage method for a subset of CTL to evaluate the completeness of properties. With this method, we can detect the transitions which are not veri ed by any property. It is more comprehensive and accurate than state-based coverage metric. We avoid generating the perturbed implementation by directly traversing transitions based on the semantics of CTL formulas. Experimental results show that the proposed method can discover subtle coverage holes with low computation cost.

Original languageEnglish
Title of host publicationASICON 2005
Subtitle of host publication2005 6th International Conference on ASIC, Proceedings
Pages850-853
Number of pages4
Publication statusPublished - 2005 Dec 1
EventASICON 2005: 2005 6th International Conference on ASIC - Shanghai, China
Duration: 2005 Oct 242005 Oct 27

Publication series

NameASICON 2005: 2005 6th International Conference on ASIC, Proceedings
Volume2

Conference

ConferenceASICON 2005: 2005 6th International Conference on ASIC
CountryChina
CityShanghai
Period05/10/2405/10/27

ASJC Scopus subject areas

  • Engineering(all)

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

Cite this