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 |