Abstract
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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Peled, D.: Combining partial order reductions with on-the-fly model-checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 377–390. Springer, Heidelberg (1994)
Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032, p. 142. Springer, New York (1996)
Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. International Journal on Software Tools for Technology Transfer 6(4) (2004)
Tan, J., Avrunin, G.S., Clarke, L.A., Zilberstein, S., Leue, S.: Heuristic-guided counterexample search in FLAVERS. SIGSOFT Softw. Eng. Notes 29(6), 201–210 (2004)
Lluch-Lafuente, A., Edelkamp, S., Leue, S.: Partial order reduction in directed model checking. In: Proceedings of the 9th International SPIN Workshop on Model Checking of Software, London, UK, pp. 112–127. Springer, Heidelberg (2002)
Mazurkiewicz, A.W.: Basic notions of trace theory. In: Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, School/Workshop, London, UK, pp. 285–363. Springer, Heidelberg (1989)
Winskel, G.: Event structures. In: Advances in Petri nets 1986, part II on Petri nets: applications and relationships to other models of concurrency, New York, NY, USA, pp. 325–392. Springer-Verlag New York, Inc, Heidelberg (1987)
Chase, C.M., Garg, V.K.: Efficient detection of restricted classes of global predicates. In: Helary, J.-M., Raynal, M. (eds.) WDAG 1995. LNCS, vol. 972, pp. 303–317. Springer, Heidelberg (1995)
Pelanek, R.: BEEM: BEnchmarks for Explicit Model checkers (2007), http://anna.fi.muni.cz/models/index.html
Holzmann, G.: On-the-fly LTL model checking with SPIN (2007), http://spinroot.com/spin/
Garg, V.K., Mittal, N., Sen, A.: Applications of lattice theory to distributed computing. ACM SIGACT Notes 34(3), 40–61 (2003)
Sen, A., Garg, V.K.: Detecting temporal logic predicates in distributed programs using computation slicing. In: Papatriantafilou, M., Hunel, P. (eds.) OPODIS 2003. LNCS, vol. 3144, pp. 171–183. Springer, Heidelberg (2004)
Davey, B., Priestley, H.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1990)
Garg, V.K., Mittal, N.: On slicing a distributed computation. In: ICDCS 2001: Proceedings of the The 21st International Conference on Distributed Computing Systems, p. 322. IEEE Computer Society, Washington (2001)
Kashyap, S., Garg, V.K.: Producing short counterexamples using “crucial events”. Technical Report TR-PDS-2008-002, ECE Dept, University of Texas at Austin (2008), http://maple.ece.utexas.edu/TechReports/2008/TR-PDS-2008-002.pdf
Vergauwen, B., Lewi, J.: A linear local model checking algorithm for CTL. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 447–461. Springer, Heidelberg (1993)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Clarke, E.M., Grumberg, O., Minea, M., Peled, D.: State space reduction using partial order techniques. International Journal on Software Tools for Technology Transfer (STTT) 2(3), 279–287 (1999)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kashyap, S., Garg, V.K. (2008). Producing Short Counterexamples Using “Crucial Events”. In: Gupta, A., Malik, S. (eds) Computer Aided Verification. CAV 2008. Lecture Notes in Computer Science, vol 5123. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70545-1_47
Download citation
DOI: https://doi.org/10.1007/978-3-540-70545-1_47
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70543-7
Online ISBN: 978-3-540-70545-1
eBook Packages: Computer ScienceComputer Science (R0)