Abstract
When a model does not satisfy a given specification, a counterexample is produced by the model checker to demonstrate the failure. A user must then examine the counterexample trace, in order to visually identify the failure that it demonstrates. If the trace is long, or the specification is complex, finding the failure in the trace becomes a non-trivial task. In this paper, we address the problem of analyzing a counterexample trace and highlighting the failure that it demonstrates. Using the notion of causality, introduced by Halpern and Pearl, we formally define a set of causes for the failure of the specification on the given counterexample trace. These causes are marked as red dots and presented to the user as a visual explanation of the failure. We study the complexity of computing the exact set of causes, and provide a polynomial-time algorithm that approximates it. This algorithm is implemented as a feature in the IBM formal verification platform RuleBase PE, where these visual explanations are an integral part of every counterexample trace. Our approach is independent of the tool that produced the counterexample, and can be applied as a light-weight external layer to any model checking tool, or used to explain simulation traces.
This work was supported in part by the Natural Sciences and Engineering Research Council of Canada.
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
Prosyd: Property-Based System Design (2005), http://www.prosyd.org/
Armoni, R., Bustan, D., Kupferman, O., Vardi, M.Y.: Resets vs. aborts in linear temporal logic. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 65–80. Springer, Heidelberg (2003)
Ball, T., Naik, M., Rajamani, S.: From symptom to cause: Localizing errors in counterexample traces. In: Proc. of POPL, pp. 97–105 (2003)
Beer, I., Ben-David, S., Chockler, H., Orni, A., Trefler, R.: Explaining Counterexamples Using Causality. IBM technical report number H-0266, http://domino.watson.ibm.com/library/cyberdig.nsf/Home
Ben-David, S., Eisner, C., Geist, D., Wolfsthal, Y.: Model checking at IBM. FMSD 22(2), 101–108 (2003)
Chechik, M., Gurfinkel, A.: A framework for counterexample generation and exploration. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol. 3442, pp. 217–233. Springer, Heidelberg (2005)
Chockler, H., Grumberg, O., Yadgar, A.: Efficient automatic STE refinement using responsibility. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 233–248. Springer, Heidelberg (2008)
Chockler, H., Halpern, J.Y., Kupferman, O.: What causes a system to satisfy a specification? ACM TOCL 9(3) (2008)
Clarke, E., Emerson, E.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1981)
Clarke, E., Grumberg, O., McMillan, K., Zhao, X.: Efficient generation of counterexamples and witnesses in symbolic model checking. In: Proc. 32nd DAC, pp. 427–432 (1995)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Copty, F., Irron, A., Weissberg, O., Kropp, N., Kamhi, G.: Efficient debugging in a formal verification environment. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 275–292. Springer, Heidelberg (2001)
Dershowitz, N., Hanna, Z., Nadel, A.: A scalable algorithm for minimal unsatisfiable core extraction. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 36–41. Springer, Heidelberg (2006)
Dong, Y., Ramakrishnan, C.R., Smolka, S.A.: Model checking and evidence exploration. In: Proc. of ECBS, pp. 214–223 (2003)
Eisner, C., Fisman, D.: A Practical Introduction to PSL. Series on Integrated Circuits and Systems (2006)
Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Campenhout, D.V.: Reasoning with temporal logic on truncated paths. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 27–39. Springer, Heidelberg (2003)
Eiter, T., Lukasiewicz, T.: Complexity results for structure-based causality. In: Proc. 7th IJCAI, pp. 35–40 (2001)
Griesmayer, A., Staber, S., Bloem, R.: Automated fault localization for c programs. ENTCS 174(4), 95–111 (2007)
Groce, A.: Error explanation with distance metrics. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 108–122. Springer, Heidelberg (2004)
Groce, A., Kroening, D.: Making the most of BMC counterexamples. In: SGSH (July 2004)
Hall, N.: Two concepts of causation. Causation and Counterfactuals. MIT Press, Cambridge (2002)
Halpern, J., Pearl, J.: Causes and explanations: A structural-model approach — part I: Causes. In: Proc. of 17th UAI, pp. 194–202. Morgan Kaufmann Publishers, San Francisco (2001)
Hume, D.: A treatise of human nature. John Noon, London (1939)
Jin, H., Ravi, K., Somenzi, F.: Fate and free will in error traces. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 445–458. Springer, Heidelberg (2002)
Kupferman, O., Vardi, M., Wolper, P.: An automata-theoretic approach to branching-time model checking. JACM 47(2), 312–360 (2000)
Maidl, M.: The common fragment of CTL and LTL. In: Proc. of FOCS, pp. 643–652 (2000)
Queille, J., Sifakis, J.: Specification and verification of concurrent systems in Cesar. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1981)
RuleBase PE homepage, http://www.haifa.il.ibm.com/projects/verification/RB_Homepage
Shen, S., Qin, Y., Li, S.: A faster counterexample minization algorithm based on refutation analysis. In: Proc. of DATE, pp. 672–677 (2005)
Staber, S., Bloem, R.: Fault localization and correction with QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 355–368. Springer, Heidelberg (2007)
Sülflow, A., Fey, G., Bloem, R., Drechsler, R.: Using unsatisfiable cores to debug multiple design errors. In: Proc. of Symp. on VLSI, pp. 77–82 (2008)
Wang, C., Yang, Z., Ivancic, F., Gupta, A.: Whodunit? causal analysis for counterexamples. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 82–95. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Beer, I., Ben-David, S., Chockler, H., Orni, A., Trefler, R. (2009). Explaining Counterexamples Using Causality. In: Bouajjani, A., Maler, O. (eds) Computer Aided Verification. CAV 2009. Lecture Notes in Computer Science, vol 5643. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02658-4_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-02658-4_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02657-7
Online ISBN: 978-3-642-02658-4
eBook Packages: Computer ScienceComputer Science (R0)