Efficient Counterexample Generation for Safety Violation in Model Checking


The KIPS Transactions:PartD, Vol. 12, No. 1, pp. 81-90, Feb. 2005
10.3745/KIPSTD.2005.12.1.81,   PDF Download:

Abstract

Given a model and a property, model checking determines whether the model satisfies the property. In case the model does not satisfy the property, model checking gives a counterexample which explains where the violation occurs. Since counterexamples are useful for model debugging as well as model understanding, counterexample generation is one of the indispensable components in the model checking tool. This paper presents efficient counterexample generation techniques when a safety property is falsified. These techniques are used to solve Push Push games which consist of 50 games. As a result, all the games are solved with the proposed techniques. However, with the original NuSMV, 42 games are solved but 8 failed. In addition, we obtain 86% time improvement and 62% space improvement compared to the original NuSMV in solving the game.


Statistics
Show / Hide Statistics

Statistics (Cumulative Counts from September 1st, 2017)
Multiple requests among the same browser session are counted as one view.
If you mouse over a chart, the values of data points will be shown.


Cite this article
[IEEE Style]
T. H. Lee and G. H. Kwon, "Efficient Counterexample Generation for Safety Violation in Model Checking," The KIPS Transactions:PartD, vol. 12, no. 1, pp. 81-90, 2005. DOI: 10.3745/KIPSTD.2005.12.1.81.

[ACM Style]
Tae Hoon Lee and Gi Hwon Kwon. 2005. Efficient Counterexample Generation for Safety Violation in Model Checking. The KIPS Transactions:PartD, 12, 1, (2005), 81-90. DOI: 10.3745/KIPSTD.2005.12.1.81.