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

1 Citation (Scopus)

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: 2005 6th International Conference on ASIC, Proceedings
Pages850-853
Number of pages4
Volume2
Publication statusPublished - 2005
EventASICON 2005: 2005 6th International Conference on ASIC - Shanghai
Duration: 2005 Oct 242005 Oct 27

Other

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

Fingerprint

Model checking
Semantics
Costs

ASJC Scopus subject areas

  • Engineering(all)

Cite this

Xu, X., Kimura, S., Horikawa, K., & Tsuchiya, T. (2005). Transition traversal coverage estimation for symbolic model checking. In ASICON 2005: 2005 6th International Conference on ASIC, Proceedings (Vol. 2, pp. 850-853). [1611460]

Transition traversal coverage estimation for symbolic model checking. / Xu, Xingwen; Kimura, Shinji; Horikawa, Kazunari; Tsuchiya, Takehiko.

ASICON 2005: 2005 6th International Conference on ASIC, Proceedings. Vol. 2 2005. p. 850-853 1611460.

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

Xu, X, Kimura, S, Horikawa, K & Tsuchiya, T 2005, Transition traversal coverage estimation for symbolic model checking. in ASICON 2005: 2005 6th International Conference on ASIC, Proceedings. vol. 2, 1611460, pp. 850-853, ASICON 2005: 2005 6th International Conference on ASIC, Shanghai, 05/10/24.
Xu X, Kimura S, Horikawa K, Tsuchiya T. Transition traversal coverage estimation for symbolic model checking. In ASICON 2005: 2005 6th International Conference on ASIC, Proceedings. Vol. 2. 2005. p. 850-853. 1611460
Xu, Xingwen ; Kimura, Shinji ; Horikawa, Kazunari ; Tsuchiya, Takehiko. / Transition traversal coverage estimation for symbolic model checking. ASICON 2005: 2005 6th International Conference on ASIC, Proceedings. Vol. 2 2005. pp. 850-853
@inproceedings{87e7e91520224467be104c74a00bfe2b,
title = "Transition traversal coverage estimation for symbolic model checking",
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.",
author = "Xingwen Xu and Shinji Kimura and Kazunari Horikawa and Takehiko Tsuchiya",
year = "2005",
language = "English",
isbn = "0780392108",
volume = "2",
pages = "850--853",
booktitle = "ASICON 2005: 2005 6th International Conference on ASIC, Proceedings",

}

TY - GEN

T1 - Transition traversal coverage estimation for symbolic model checking

AU - Xu, Xingwen

AU - Kimura, Shinji

AU - Horikawa, Kazunari

AU - Tsuchiya, Takehiko

PY - 2005

Y1 - 2005

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=33847296271&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=33847296271&partnerID=8YFLogxK

M3 - Conference contribution

SN - 0780392108

SN - 9780780392106

VL - 2

SP - 850

EP - 853

BT - ASICON 2005: 2005 6th International Conference on ASIC, Proceedings

ER -