Accelerating Coverage Estimation Through Partial Model Checking
Accelerating Coverage Estimation Through Partial Model Checking
复制标题
DOI：
10.1109/tc.2013.63
复制
发表时间：
2014-07
影响因子：
3.7
通讯作者：
Yean-Ru Chen;Jia-Jen Yeh;Pao-Ann Hsiung;Sao-Jie Chen
中科院分区：
文献类型：
--
作者：
Yean-Ru Chen;Jia-Jen Yeh;Pao-Ann Hsiung;Sao-Jie Chen
在针对一组属性对系统设计进行模型检查时，覆盖估计经常用于测量属性检查的系统行为的数量。一种流行的覆盖率估计方法是对系统模型进行变异，并检查是否可以通过给定的属性检测到变异。对于每个突变和每个属性，一些最先进的覆盖估计方法需要进行完整的模型检查。通过这种重复的模型检查，基于突变的覆盖率估计变得非常耗时。为了缓解这个问题，部分模型检测（PMC）技术提出了重新检查那些系统状态的影响，突变，从而避免了不必要的重新检查的大部分系统状态，节省了时间。PMC方法已集成到状态图操纵器模型检查器中。应用该方法的几个例子表明，PMC有节省50%至70%的覆盖估计时间，并减少90%的模式访问。
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.