Accelerating coverage estimation through partial model checking

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

研究成果: Article同行評審

3 引文 斯高帕斯(Scopus)

摘要

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.

原文English
文章編號6484055
頁(從 - 到)1613-1625
頁數13
期刊IEEE Transactions on Computers
63
發行號7
DOIs
出版狀態Published - 2014 一月 1

All Science Journal Classification (ASJC) codes

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

指紋 深入研究「Accelerating coverage estimation through partial model checking」主題。共同形成了獨特的指紋。

引用此