Producing Short Counterexamples Using 'Crucial Events'

摘要

Ideally, a model checking tool should successfully tackle state space explosion for complete system validation, while providing short counterexamples when an error exists. Techniques such as partial order (p.o.) reduction [1,2] are very effective at tackling state space explosion, but do not produce short counterexamples. On the other hand, directed model checking [3,4] techniques find short counterexamples, but are prone to state space explosion in the absence of errors. To the best of our knowledge, there is currently no single technique that meets both requirements. We present such a technique in this paper. For a subset of CTL, which we call CETL (Crucial Event Temporal Logic), we show that there exists a unique minimum set of events in each program trace whose execution is both necessary and sufficient to lead to an error state. These events are called "crucial events". We show how crucial events can be used to produce short counterexamples, while also providing state space reduction. We have implemented the techniques presented here as an extension to the model checker SPIN, called SPICED (Simple PROMELA Interpreter with Crucial Event Detection). Experimental results are presented.