Abstract
When a system fails to satisfy its specification, the model checker produces an error trace (or counter-example) that demonstrates an undesirable behavior, which is then used in debugging the system. Error explanation is the task of discovering errors in the system or the reasons why the system exhibits the error trace. While there has been considerable recent interest in automating this task and developing tools based on different heuristics, there has been very little effort in characterizing the computational complexity of the problem of error explanation.
In this paper, we study the complexity of two popular heuristics used in error explanation. The first approach tries to compute the smallest number of system changes that need to be made in order to ensure that the given counter-example is no longer exhibited, with the intuition being that these changes are the errors that need fixing. The second approach relies on the observation that differences between correct and faulty runs of a system shed considerable light on the sources of errors. In this approach, one tries to compute the correct trace of the system that is closest to the counter-example. We consider three commonly used abstractions to model programs and systems, namely, finite state Mealy machines, extended finite state machines and pushdown automata. We show that the first approach of trying to find the fewest program changes is NP-complete no matter which of the three formal models is used to represent the system. Moreover we show that no polynomial factor approximation algorithm for computing the smallest set of changes is possible, unless P = NP. For the second approach, we present a polynomial time algorithm that finds the closest correct trace, when the program is represented by a Mealy machine or a pushdown automata. When the program is represented by an extended finite state machine, the problem is once again NP-complete, and no polynomial factor approximation algorithm is likely.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)
Zeller, A.: Isolating cause-effect chains for computer programs. In: Proceedings of the ACM Symposium on the Foundations of Software Engineering, pp. 1–10 (2002)
Zeller, A., Hildebrandt, R.: Simplifying and isolating failure-inducing input. IEEE Transactions on Software Engineering 28, 183–200 (2002)
Jin, H., Ravi, K., Somenzi, F.: Fate and free will in error traces. In: TACAS 2001. LNCS, vol. 2031, pp. 445–459. Springer, Heidelberg (2001)
Renieris, M., Reiss, S.: Fault localization with nearest neighbor queries. In: Proceedings of the Conference on Automated Software Engineering (2003)
Ball, T., Naik, M., Rajamani, S.: From symptom to cause: Localizing errors in counterexample traces. In: Proceedings of the ACM Symposium on the Principles of Programming Languages, pp. 97–105 (2003)
Groce, A., Visser, W.: What went wrong: Explaining counterexamples. In: Proceedings of the SPIN Workshop on Model Checking of Software, pp. 121–135 (2003)
Groce, A.: Error explanation with distance metrics. In: Proceedings of Conference on Tools and Algorithms for Construction and Analysis of Systems, pp. 108–122 (2004)
Ball, T., Rajamani, S.K.: The SLAM project: Debugging system software via static analysis. In: Proceedings of the ACM Symposium on the Principles of Programming Languages, pp. 1–3 (2002)
Brat, G., Havelund, K., Park, S., Visser, W.: Java PathFinder – A second generation of a Java model checker. In: Proceedings of the Workshop on Advances in Verification (2000)
Lewis, D.: Causation. Journal of Philosophy 70, 556–567 (1973)
Zeller, A.: Yesterday, my program worked. Today, is does not. Why? In: Proceedings of the ACM Symposium on the Foundations of Software Engineering, pp. 253–267 (1999)
Tip, F., Dinesh, T.B.: A slicing-based approach for locating type errors. ACM Transactions on Software Engineering and Methodology 10, 5–55 (2001)
Bhargavan, K., Gunter, C.A., Kim, M., Lee, I., Obradovic, D., Sokolsky, O., Viswanathan, M.: Verisim: Formal analysis of network simulations. IEEE: Transactions on Software Engineering 28, 129–145 (2002)
Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Reading (1979)
Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Proceedings of the ACM Symposium on the Theory of Computation (2004)
Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: Proceedings of the ACM Symposium on the Principles of Programming Languages, pp. 49–61 (1995)
Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms. McGraw-Hill Higher Education, New York (2001)
Pitt, L., Warmuth, M.K.: The minimum consistent DFA problem cannot be approximated within any polynomial. Journal of the ACM 40, 95–142 (1993)
Lawler, E.L.: A procedure for computing the K best solutions to discrete optimization problems and its application to the shortest path problem. Management Science 18, 401–405 (1972)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kumar, N., Kumar, V., Viswanathan, M. (2005). On the Complexity of Error Explanation. In: Cousot, R. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2005. Lecture Notes in Computer Science, vol 3385. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30579-8_29
Download citation
DOI: https://doi.org/10.1007/978-3-540-30579-8_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-24297-0
Online ISBN: 978-3-540-30579-8
eBook Packages: Computer ScienceComputer Science (R0)