Accelerating coverage estimation through partial model checking

Yean-Ru Chen, Jia Jen Yeh, Pao Ann Hsiung, Sao Jie Chen

Research output: Contribution to journalArticle

2 Citations (Scopus)

Abstract

In model checking a system design against a set of properties, coverage estimation is frequently used to measure the amount of system behavior being checked by the properties. A popular coverage estimation method is to mutate the system model and check if the mutation can be detected by the given properties. For each mutation and each property, a full model check is required by some state-of-the-art coverage estimation methods. With such repeated model checking, mutation-based coverage estimation becomes significantly time-consuming. To alleviate this problem, a partial model checking (PMC) technique is proposed to recheck only those system states that were affected by a mutation, thus unnecessary rechecking of a large portion of the system states is avoided and time is saved. The PMC method has been integrated into the State Graph Manipulators model checker. Applying the proposed method to several examples showed that PMC has a saving of 50% to 70% in the coverage estimation time, and a reduction of 90% in mode visits.

Original languageEnglish
Article number6484055
Pages (from-to)1613-1625
Number of pages13
JournalIEEE Transactions on Computers
Volume63
Issue number7
DOIs
Publication statusPublished - 2014 Jan 1

Fingerprint

Model checking
Model Checking
Coverage
Partial
Mutation
Property of set
Manipulator
Manipulators
System Design
Systems analysis
Model
Graph in graph theory

All Science Journal Classification (ASJC) codes

  • Software
  • Theoretical Computer Science
  • Hardware and Architecture
  • Computational Theory and Mathematics

Cite this

Chen, Yean-Ru ; Yeh, Jia Jen ; Hsiung, Pao Ann ; Chen, Sao Jie. / Accelerating coverage estimation through partial model checking. In: IEEE Transactions on Computers. 2014 ; Vol. 63, No. 7. pp. 1613-1625.
@article{c6da7d59c746414e8774b505c0f044df,
title = "Accelerating coverage estimation through partial model checking",
abstract = "In model checking a system design against a set of properties, coverage estimation is frequently used to measure the amount of system behavior being checked by the properties. A popular coverage estimation method is to mutate the system model and check if the mutation can be detected by the given properties. For each mutation and each property, a full model check is required by some state-of-the-art coverage estimation methods. With such repeated model checking, mutation-based coverage estimation becomes significantly time-consuming. To alleviate this problem, a partial model checking (PMC) technique is proposed to recheck only those system states that were affected by a mutation, thus unnecessary rechecking of a large portion of the system states is avoided and time is saved. The PMC method has been integrated into the State Graph Manipulators model checker. Applying the proposed method to several examples showed that PMC has a saving of 50{\%} to 70{\%} in the coverage estimation time, and a reduction of 90{\%} in mode visits.",
author = "Yean-Ru Chen and Yeh, {Jia Jen} and Hsiung, {Pao Ann} and Chen, {Sao Jie}",
year = "2014",
month = "1",
day = "1",
doi = "10.1109/TC.2013.63",
language = "English",
volume = "63",
pages = "1613--1625",
journal = "IEEE Transactions on Computers",
issn = "0018-9340",
publisher = "IEEE Computer Society",
number = "7",

}

Accelerating coverage estimation through partial model checking. / Chen, Yean-Ru; Yeh, Jia Jen; Hsiung, Pao Ann; Chen, Sao Jie.

In: IEEE Transactions on Computers, Vol. 63, No. 7, 6484055, 01.01.2014, p. 1613-1625.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Accelerating coverage estimation through partial model checking

AU - Chen, Yean-Ru

AU - Yeh, Jia Jen

AU - Hsiung, Pao Ann

AU - Chen, Sao Jie

PY - 2014/1/1

Y1 - 2014/1/1

N2 - In model checking a system design against a set of properties, coverage estimation is frequently used to measure the amount of system behavior being checked by the properties. A popular coverage estimation method is to mutate the system model and check if the mutation can be detected by the given properties. For each mutation and each property, a full model check is required by some state-of-the-art coverage estimation methods. With such repeated model checking, mutation-based coverage estimation becomes significantly time-consuming. To alleviate this problem, a partial model checking (PMC) technique is proposed to recheck only those system states that were affected by a mutation, thus unnecessary rechecking of a large portion of the system states is avoided and time is saved. The PMC method has been integrated into the State Graph Manipulators model checker. Applying the proposed method to several examples showed that PMC has a saving of 50% to 70% in the coverage estimation time, and a reduction of 90% in mode visits.

AB - In model checking a system design against a set of properties, coverage estimation is frequently used to measure the amount of system behavior being checked by the properties. A popular coverage estimation method is to mutate the system model and check if the mutation can be detected by the given properties. For each mutation and each property, a full model check is required by some state-of-the-art coverage estimation methods. With such repeated model checking, mutation-based coverage estimation becomes significantly time-consuming. To alleviate this problem, a partial model checking (PMC) technique is proposed to recheck only those system states that were affected by a mutation, thus unnecessary rechecking of a large portion of the system states is avoided and time is saved. The PMC method has been integrated into the State Graph Manipulators model checker. Applying the proposed method to several examples showed that PMC has a saving of 50% to 70% in the coverage estimation time, and a reduction of 90% in mode visits.

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

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

U2 - 10.1109/TC.2013.63

DO - 10.1109/TC.2013.63

M3 - Article

VL - 63

SP - 1613

EP - 1625

JO - IEEE Transactions on Computers

JF - IEEE Transactions on Computers

SN - 0018-9340

IS - 7

M1 - 6484055

ER -