An Efficient Algorithm to Understand Long Counterexample

Abstract:

For given system to proceed model checking, if system model is discontent with the quality which to be detected, model detector will give counterexample, it will cause the generated counterexample too long when system state-space is very large, it is a very important problem, how to find the reason of model failure from long counterexample quickly, the article uses extractive technique of minimal unsatisfiable subformula to put forward a kind of understanding counterexample way which is extracted minimal unsatisfiable subformula quickly from Boolean formula. The algorithm can pinpoint error and find the reason of model failure. Experimental result indicated that understanding counterexample is based on minimal unsatisfiable subformula can accelerate understanding counterexample speed, improve the efficient of debugging, guide system abstract model improvement effectively.

• Periodical: Applied Mechanics and Materials (Volume 328)
• Pages: 254-260
• DOI: https://doi.org/10.4028/www.scientific.net/AMM.328.254
• Online since: June 2013
• Authors: Zhi Yuan Chen, Shao Bin Huang, Ming Yu Ji, Lin Shan Shen
• Keywords: Boolean Formula, Long Counterexample, Minimal Unsatisfiable Subformula, Model Checking, Understanding Counterexample

References

[1] E Clarke, E Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. Logics of Programs, (1982), pp.52-71.

DOI: 10.1007/bfb0025774

[2] J Queille, J Sifakis. Specification and verification of concurrent systems in CESAR //International Symposium on Programming. (1982), pp.337-351.

DOI: 10.1007/3-540-11494-7_22

[3] I Beer, S Ben-David, H Chockler, et al. Explaining counterexamples using causality //Computer Aided Verification. (2009), pp.94-108.

DOI: 10.1007/978-3-642-02658-4_11

[4] N Jalbert, K Sen. A trace simplification technique for effective debugging of concurrent programs //Proceedings of the eighteenth ACM SIGSOFT international symposium on Foundations of software engineering. (2010), pp.57-66.

DOI: 10.1145/1882291.1882302

[5] J Y Halpern, J Pearl. Causes and explanations: A structural-model approach. Part I: Causes. The British journal for the philosophy of science, (2005), 56(4), pp.843-887.

DOI: 10.1093/bjps/axi147

[6] M Jose, R Majumdar. Cause Clue Clauses: Error Localization using Maximum Satisfiability. Arxiv preprint arXiv: 1011.1589, (2010).

DOI: 10.1145/2345156.1993550

[7] C Wang, Z Yang, F Ivančić, et al. Whodunit? Causal analysis for counterexamples. Automated Technology for Verification and Analysis, (2006), 4218, pp.82-95.

DOI: 10.1007/11901914_9

[8] A Suelflow, G Fey, R Bloem, et al. Using unsatisfiable cores to debug multiple design errors//Proceedings of the 18th ACM Great Lakes symposium on VLSI. (2008), pp.77-82.

DOI: 10.1145/1366110.1366131