Transition traversal coverage estimation for symbolic model checking

Xingwen Xu, Shinji Kimura, Kazunari Horikawa, Takehiko Tsuchiya

研究成果: Conference contribution

抄録

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.

本文言語English
ホスト出版物のタイトルASICON 2005
ホスト出版物のサブタイトル2005 6th International Conference on ASIC, Proceedings
ページ850-853
ページ数4
出版ステータスPublished - 2005 12 1
イベントASICON 2005: 2005 6th International Conference on ASIC - Shanghai, China
継続期間: 2005 10 242005 10 27

出版物シリーズ

名前ASICON 2005: 2005 6th International Conference on ASIC, Proceedings
2

Conference

ConferenceASICON 2005: 2005 6th International Conference on ASIC
国/地域China
CityShanghai
Period05/10/2405/10/27

ASJC Scopus subject areas

  • 工学(全般)

フィンガープリント

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

引用スタイル