Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

A bounded constraint-based approach to aid in fault localization from a counterexample

  • Original Article
  • Published:
Innovations in Systems and Software Engineering Aims and scope Submit manuscript

Abstract

A model checker can produce a trace of counter-example for an erroneous program, which is often difficult to exploit for locating faults. In this paper, we propose a fault localization algorithm from counter-examples, named LocFaults, combining the approaches of Bounded Model-Checking (BMC) with a constraint satisfaction problem (CSP). The input is a faulty program for which a counter-example and a postcondition are provided. To identify helpful information for fault location, LocFaults analyzes the paths of the CFG (Control Flow Graph) of the erroneous program to calculate the subsets of suspicious instructions to correct the program. Indeed, we generate a system of constraints for paths of the control flow graph for which at most k conditional statements can be wrong. Then we calculate the MCSs (Minimal Correction Sets) of limited size on each of these paths. The removal of one of these sets of constraints yields a maximal satisfiable subset, in other words, a maximal subset of constraints satisfying the postcondition. LocFaults has been experimentally evaluated on a set of academic and realistic programs. The main advantage of this flow-driven approach is that the computed sets of suspicious instructions are small, each of them being associated with an identified path. Moreover, the constraint programming-based framework of LocFaults allows mixing Boolean and numerical constraints in an efficient and straightforward way.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Algorithm 1
Algorithm 2
Algorithm 3
Algorithm 4

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

Data availability

The datasets generated and/or analyzed during the current study are available at http://www.capv.toile-libre.org/Benchs_Mohammed.html.

Code availability

The code for the implementation of LocFaults can be found at https://github.com/mdbekkouche/LocFaultsTool.

Notes

  1. Refer to https://www.ibm.com/docs/en/icos/12.10.0?topic=constraints-logical-cplex

References

  1. Avizienis A, Laprie J-C, Randell B (2001) Fundamental concepts of dependability. Department of Computing Science Technical Report Series

  2. Avižienis A, Laprie J-C, Randell B (2004) Dependability and its threats: a taxonomy. In: Building the information society: IFIP 18th world computer congress topical sessions 22–27 August 2004 Toulouse, France, Springer, pp 91–120

  3. Wong WE, Debroy V (2010) Software fault localization. In: Encyclopedia of software engineering

  4. Testing and Debugging. http://www.jodypaul.com/SWE/TD/TestDebug.html. Accessed 13 Oct (2022)

  5. Bekkouche M, Collavizza H, Rueher M (2015) Locfaults: a new flow-driven and constraint-based error localization approach. In: Proceedings of the 30th annual ACM symposium on applied computing, pp 1773–1780

  6. Liffiton MH, Sakallah KA (2008) Algorithms for computing minimal unsatisfiable subsets of constraints. J Autom Reason 40(1):1–33

    Article  MathSciNet  Google Scholar 

  7. Jose M, Majumdar R (2011) Cause clue clauses: error localization using maximum satisfiability. ACM SIGPLAN Notices 46(6):437–446

    Article  Google Scholar 

  8. Gotlieb A, Botella B, Rueher M (1998) Automatic test data generation using constraint solving techniques. ACM SIGSOFT Softw Eng Notes 23(2):53–62

    Article  Google Scholar 

  9. Xuan J, Monperrus M (2014) Test case purification for improving fault localization. In: Proceedings of the 22nd ACM SIGSOFT international symposium on foundations of software engineering, pp 52–63

  10. Jones JA, Harrold MJ, Stasko J (2002) Visualization of test information to assist fault localization. In: Proceedings of the 24th international conference on software engineering. ICSE 2002, IEEE, pp 467–477

  11. Zeller A, Hildebrandt R (2002) Simplifying and isolating failure-inducing input. IEEE Trans Softw Eng 28(2):183–200

    Article  Google Scholar 

  12. Renieres M, Reiss SP (2003) Fault localization with nearest neighbor queries. In: 18th IEEE international conference on automated software engineering. Proceedings., IEEE, pp 30–39 (2003)

  13. Liblit B, Naik M, Zheng AX, Aiken A, Jordan MI (2005) Scalable statistical bug isolation. Acm Sigplan Notices 40(6):15–26

    Article  Google Scholar 

  14. Guo L, Roychoudhury A, Wang T (2006) Accurately choosing execution runs for software fault localization. In: International conference on compiler construction, Springer, pp 80–95

  15. Dallmeier V, Lindig C, Zeller A (2005) Lightweight defect localization for java. In: European conference on object-oriented programming, Springer, pp 528–550

  16. Zakari A, Lee SP, Hashem IAT (2019) A single fault localization technique based on failed test input. Array 3:100008

    Article  Google Scholar 

  17. Zakari A, Lee SP, Chong CY (2018) Simultaneous localization of software faults based on complex network theory. IEEE Access 6:23990–24002

    Article  Google Scholar 

  18. Dutta A, Kunal K, Srivastava SS, Shankar S, Mall R (2021) Ftfl: a fisher’s test-based approach for fault localization. Innovat Syst Softw Eng 17(4):381–405

    Article  Google Scholar 

  19. Clarke EM, Emerson EA (1981) Design and synthesis of synchronization skeletons using branching time temporal logic. In: Workshop on logic of programs, Springer, pp 52–71

  20. D’silva V, Kroening D, Weissenbacher G (2008) A survey of automated techniques for formal software verification. IEEE Trans Comput-Aid Des Integr Circuits Syst 27(7):1165–1178

    Article  Google Scholar 

  21. Ball T, Naik M, Rajamani SK (2003) From symptom to cause: localizing errors in counterexample traces. In: Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on principles of programming languages, pp 97–105

  22. Groce A, Kroening D, Lerda F (2004) Understanding counterexamples with explain. In: International conference on computer aided verification, Springer, pp 453–456

  23. Groce A, Chaki S, Kroening D, Strichman O (2006) Error explanation with distance metrics. Int J Softw Tools Technol Transf 8(3):229–247

    Article  Google Scholar 

  24. Lewis D (1974) Causation. J Philos 70(17):556–567

    Article  Google Scholar 

  25. Jose M, Majumdar R (2011) Bug-assist: assisting fault localization in ansi-c programs. In: International conference on computer aided verification, Springer, pp 504–509

  26. Marques-Silva J, Planes J (2008) Algorithms for maximum satisfiability using unsatisfiable cores. In: Proceedings of the conference on design, automation and test in Europe, pp 408–413

  27. Marques-Silva J (2009) The msuncore maxsat solver

  28. Lamraoui S-M, Nakajima S (2014) A formula-based approach for automatic fault localization of imperative programs. In: International conference on formal engineering methods, Springer, pp 251–266

  29. Lamraoui S-M, Nakajima S (2016) A formula-based approach for automatic fault localization of multi-fault programs. J Inf Process 24(1):88–98

    Google Scholar 

  30. Dutertre B, De Moura L (2006) The yices smt solver at Tool paper 2(2):1–2 http://yices.csl.sri.com/tool-paper.pdf

  31. Chinneck JW (2007) Feasibility and infeasibility in optimization:: algorithms and computational methods vol. 118. Springer

  32. Chinneck JW (1996) Localizing and diagnosing infeasibilities in networks. INFORMS J Comput 8(1):55–62

    Article  MathSciNet  Google Scholar 

  33. Chinneck JW (2001) Fast heuristics for the maximum feasible subsystem problem. INFORMS J Comput 13(3):210–223

    Article  MathSciNet  Google Scholar 

  34. Birnbaum E, Lozinskii EL (2003) Consistent subsets of inconsistent systems: structure and behaviour. J Exp Theoret Artif Intell 15(1):25–46

    Article  Google Scholar 

  35. Tamiz M, Mardle SJ, Jones DF (1996) Detecting iis in infeasible linear programmes using techniques from goal programming. Comput Oper Res 23(2):113–119

    Article  Google Scholar 

  36. Junker U (2004) Preferred explanations and relaxations for over-constrained problems. In: AAAI-2004

  37. Barnett M, Leino KRM (2005) Weakest-precondition of unstructured programs. In: Proceedings of the 6th ACM SIGPLAN-SIGSOFT workshop on program analysis for software tools and engineering, pp 82–87

  38. Collavizza H, Rueher M, Van Hentenryck P (2010) Cpbpv: a constraint-programming framework for bounded program verification. Constraints 15(2):238–264

    Article  MathSciNet  Google Scholar 

  39. Collavizza H, Le Vinh N, Ponsini O, Rueher M, Rollet A (2014) Constraint-based bmc: a backjumping strategy. Int J Softw Tools Technol Transf 16(1):103–121

    Article  Google Scholar 

  40. Rosenblum DS, Weyuker EJ (1997) Lessons learned from a regression testing case study. Empir Softw Eng 2(2):188–191

    Article  Google Scholar 

  41. Clarke E, Kroening D, Lerda F (2004) A tool for checking ansi-c programs. In: International conference on tools and algorithms for the construction and analysis of systems, Springer, pp 168–176

  42. Bekkouche M (2023) Correcting instruction expression logic errors with genexp: a genetic programming solution. Comput Sci 31(2):92

    MathSciNet  Google Scholar 

Download references

Funding

No funding was received to assist with the preparation of this manuscript.

Author information

Authors and Affiliations

  1. LabRI-SBA Laboratory, École Supérieure en Informatique, Sidi Bel Abbès, Algeria

    Mohammed Bekkouche

Authors
  1. Mohammed Bekkouche
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Mohammed Bekkouche.

Ethics declarations

Conflict of interest

The author has no relevant financial or non-financial interests to disclose.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Bekkouche, M. A bounded constraint-based approach to aid in fault localization from a counterexample. Innovations Syst Softw Eng (2024). https://doi.org/10.1007/s11334-024-00558-1

Download citation

  • Received:

  • Accepted:

  • Published:

  • DOI: https://doi.org/10.1007/s11334-024-00558-1

Keywords

Search

Navigation