Advertisement

Explaining Counterexamples Using Causality

  • Ilan Beer
  • Shoham Ben-David
  • Hana Chockler
  • Avigail Orni
  • Richard Trefler
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)

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.

Keywords

Execution Time Model Check Temporal Logic Linear Temporal Logic Kripke Structure 
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

  1. 1.
    Prosyd: Property-Based System Design (2005), http://www.prosyd.org/
  2. 2.
    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)CrossRefGoogle Scholar
  3. 3.
    Ball, T., Naik, M., Rajamani, S.: From symptom to cause: Localizing errors in counterexample traces. In: Proc. of POPL, pp. 97–105 (2003)Google Scholar
  4. 4.
    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
  5. 5.
    Ben-David, S., Eisner, C., Geist, D., Wolfsthal, Y.: Model checking at IBM. FMSD 22(2), 101–108 (2003)zbMATHGoogle Scholar
  6. 6.
    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)CrossRefGoogle Scholar
  7. 7.
    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)CrossRefGoogle Scholar
  8. 8.
    Chockler, H., Halpern, J.Y., Kupferman, O.: What causes a system to satisfy a specification? ACM TOCL 9(3) (2008)Google Scholar
  9. 9.
    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)CrossRefGoogle Scholar
  10. 10.
    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)Google Scholar
  11. 11.
    Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  12. 12.
    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)CrossRefGoogle Scholar
  13. 13.
    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)CrossRefGoogle Scholar
  14. 14.
    Dong, Y., Ramakrishnan, C.R., Smolka, S.A.: Model checking and evidence exploration. In: Proc. of ECBS, pp. 214–223 (2003)Google Scholar
  15. 15.
    Eisner, C., Fisman, D.: A Practical Introduction to PSL. Series on Integrated Circuits and Systems (2006)Google Scholar
  16. 16.
    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)CrossRefGoogle Scholar
  17. 17.
    Eiter, T., Lukasiewicz, T.: Complexity results for structure-based causality. In: Proc. 7th IJCAI, pp. 35–40 (2001)Google Scholar
  18. 18.
    Griesmayer, A., Staber, S., Bloem, R.: Automated fault localization for c programs. ENTCS 174(4), 95–111 (2007)Google Scholar
  19. 19.
    Groce, A.: Error explanation with distance metrics. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 108–122. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  20. 20.
    Groce, A., Kroening, D.: Making the most of BMC counterexamples. In: SGSH (July 2004)Google Scholar
  21. 21.
    Hall, N.: Two concepts of causation. Causation and Counterfactuals. MIT Press, Cambridge (2002)Google Scholar
  22. 22.
    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)Google Scholar
  23. 23.
    Hume, D.: A treatise of human nature. John Noon, London (1939)Google Scholar
  24. 24.
    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)CrossRefGoogle Scholar
  25. 25.
    Kupferman, O., Vardi, M., Wolper, P.: An automata-theoretic approach to branching-time model checking. JACM 47(2), 312–360 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Maidl, M.: The common fragment of CTL and LTL. In: Proc. of FOCS, pp. 643–652 (2000)Google Scholar
  27. 27.
    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)CrossRefGoogle Scholar
  28. 28.
  29. 29.
    Shen, S., Qin, Y., Li, S.: A faster counterexample minization algorithm based on refutation analysis. In: Proc. of DATE, pp. 672–677 (2005)Google Scholar
  30. 30.
    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)CrossRefGoogle Scholar
  31. 31.
    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)Google Scholar
  32. 32.
    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)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Ilan Beer
    • 1
  • Shoham Ben-David
    • 2
  • Hana Chockler
    • 1
  • Avigail Orni
    • 1
  • Richard Trefler
    • 2
  1. 1.IBM Research Mount CarmelHaifaIsrael
  2. 2.David R. Cheriton School of Computer ScienceUniversity of WaterlooWaterlooCanada

Personalised recommendations