Presentation 2005-12-02
Structural Coverage of Traversed Transitions for Symbolic Model Checking
Xingwen Xu, Shinji Kimura, Kazunari Horikawa, Takehiko Tsuchiya,
PDF Download Page PDF download Page Link
Abstract(in Japanese) (See Japanese page)
Abstract(in English) Coverage estimation for model checking has become an important issue in practical formal verification. Transition traversal coverage focuses on the transition characteristics of CTL operators and calculates which transitions are traversed during the model checking process of properties. One limitation of the method is the lack of the correspondence between the circuit structure and transitions. One transition might be covered no matter which part of the circuit is checked (or not) related to the transition. This leads to the overestimation of the coverability of properties. In this paper, we enhance the transition traversal coverage by analyzing the structural coverage of each traversed transition. We consider which variables are checked explicitly or implicitly on the traversed transitions. Thus, we deduce which part of the circuit is checked by properties for each traversed transition. The importance is that we can analyze which part of the circuit has not been verified. The accuracy of the transition traversal coverage is enhanced by our technique. We show the effectiveness of the proposed method by experiments.
Keyword(in Japanese) (See Japanese page)
Keyword(in English) structural coverage / transition traversal / symbolic model checking
Paper # VLD2005-87,ICD2005-182,DC2005-64
Date of Issue

Conference Information
Committee DC
Conference Date 2005/11/25(1days)
Place (in Japanese) (See Japanese page)
Place (in English)
Topics (in Japanese) (See Japanese page)
Topics (in English)
Chair
Vice Chair
Secretary
Assistant

Paper Information
Registration To Dependable Computing (DC)
Language ENG
Title (in Japanese) (See Japanese page)
Sub Title (in Japanese) (See Japanese page)
Title (in English) Structural Coverage of Traversed Transitions for Symbolic Model Checking
Sub Title (in English)
Keyword(1) structural coverage
Keyword(2) transition traversal
Keyword(3) symbolic model checking
1st Author's Name Xingwen Xu
1st Author's Affiliation Graduate School of IPS, Waseda University()
2nd Author's Name Shinji Kimura
2nd Author's Affiliation Graduate School of IPS, Waseda University
3rd Author's Name Kazunari Horikawa
3rd Author's Affiliation System LSI Design Division, Toshiba Corporation
4th Author's Name Takehiko Tsuchiya
4th Author's Affiliation System LSI Design Division, Toshiba Corporation
Date 2005-12-02
Paper # VLD2005-87,ICD2005-182,DC2005-64
Volume (vol) vol.105
Number (no) 449
Page pp.pp.-
#Pages 6
Date of Issue