Abstract
Behavior models are often used to describe behaviors of the system-to-be during requirements analysis or design phases. The correctness of the specified model can be formally verified by model checking techniques. Model checkers provide counterexamples if the model does not satisfy the given property. However, the tasks to analyze counterexamples and identify the model errors require manual labor because counterexamples do not directly indicate where and why the errors exist, and when liveness properties are checked, counterexamples have infinite trace length, which makes it harder to automate the analysis. In this paper, we propose a novel automated approach to find errors in a behavior model using an infinite counterexample. We find similar witnesses to the counterexample then compare them to elicit errors. Our approach reduces the problem to a single-source shortest path search problem on directed graphs and is applicable to liveness properties.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Ball, T., Naik, M., Rajamani, S.K.: From symptom to cause: localizing errors in counterexample traces. In: POPL 2003, pp. 97–105 (2003)
Beer, I., Ben-David, S., Chockler, H., Orni, A., Trefler, R.: Explaining counterexamples using causality. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 94–108. Springer, Heidelberg (2009)
Chaki, S., Groce, A., Strichman, O.: Explaining abstract counterexamples. In: SIGSOFT 2004/FSE 12, pp. 73–82 (2004)
Clarke, E.M.: The birth of model checking. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 1–26. Springer, Heidelberg (2008)
Clarke, E.M.J., Grumberg, O., Peled, D.A.: Model checking. MIT Press, Cambridge (1999)
Cleve, H., Zeller, A.: Locating causes of program failures. In: ICSE 2005, pp. 342–351 (2005)
Dijkstra, E.W.: A note on two problems in connection with graphs. Numerische Mathematik, 269–271 (1959)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: ICSE 1999, pp. 411–420 (1999)
Giannakopoulou, D., Magee, J.: Fluent model checking for event-based systems. In: ESEC/FSE 2003, pp. 257–266 (2003)
Giannakopoulou, D., Magee, J., Kramer, J.: Checking progress with action priority: Is it fair? In: ESEC/FSE 1999, pp. 511–527 (1999)
Griesmayer, A., Staber, S., Bloem, R.: Automated fault localization for C programs. Elec. Notes in Theor. Comp. Sci. 174, 95–111 (2007)
Groce, A., Chaki, S., Kroening, D., Strichman, O.: Error explanation with distance metrics. STTT 8(3), 229–247 (2006)
Groce, A., Visser, W.: What went wrong: explaining counterexamples. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 121–135. Springer, Heidelberg (2003)
Holzmann, G.J.: The SPIN model checker: primer and reference manual. Addison-Wesley, Reading (2004)
Jones, J.A., Harrold, M.J., Stasko, J.: Visualization of test information to assist fault localization. In: ICSE 2002, pp. 467–477 (2002)
Killian, C., Anderson, J.W., Jhala, R., Vahdat, A.: Life, death, and the critical transition: finding liveness bugs in systems code. In: NSDI 2007, pp. 243–256 (2007)
Konstantinidis, S., Silva, P.V.: Computing maximal error-detecting capabilities and distances of regular languages. Technical report, CMUP 2008-28 (2008)
Kumazawa, T., Tamai, T.: Iterative model fixing with counterexamples. In: APSEC 2008, pp. 369–376 (2008)
Kumazawa, T., Tamai, T.: Localizing errors and presenting alternatives: a model-based approach. In: SES 2009, pp. 55–62 (2009) (in Japanese)
Levenshtein, V.I.: Binary codes capable of correcting deletions, insertions and reversals. Soviet Physics Doklady 10(8), 707–710 (1966)
Magee, J., Kramer, J.: Concurrency: state models & Java programming, 2nd edn. John Wiley & Sons, Chichester (2006)
Mohri, M.: Edit-distance of weighted automata: general definitions and algorithms. Int. J. of Found. of Comp. Sci. 14(6), 957–982 (2003)
Renieris, M., Reiss, S.P.: Fault localization with nearest neighbor queries. In: ASE 2003, pp. 30–39 (2003)
Schmidt, D.C.: Model-driven engineering. IEEE Computer 39(2), 25–31 (2006)
Uchitel, S., Brunet, G., Chechik, M.: Synthesis of partial behaviour models from properties and scenarios. IEEE TSE 35(3), 384–406 (2009)
Wing, J.M., Vaziri-Farahani, M.: A case study in model checking software systems. Sci. of Comp. Prog. 28, 273–299 (1997)
Zeller, A.: Isolating cause-effect chains from computer programs. In: SIGSOFT 2002/FSE 10, pp. 1–10 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kumazawa, T., Tamai, T. (2011). Counterexample-Based Error Localization of Behavior Models. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds) NASA Formal Methods. NFM 2011. Lecture Notes in Computer Science, vol 6617. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20398-5_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-20398-5_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-20397-8
Online ISBN: 978-3-642-20398-5
eBook Packages: Computer ScienceComputer Science (R0)