logo

SCIENCE CHINA Information Sciences, Volume 60, Issue 1: 012105(2017) https://doi.org/10.1007/s11432-015-0450-5

An empirical study on constraint optimization techniques for test generation

More info
  • ReceivedNov 13, 2015
  • AcceptedFeb 3, 2016
  • PublishedOct 13, 2016

Abstract

Constraint solving is a frequent, but expensive operation with symbolic execution to generate tests for a program. To improve the efficiency of test generation using constraint solving, four optimization techniques are usually applied to existing constraint solvers, which are constraint independence, constraint set simplification, constraint caching, and expression rewriting. In this paper, we conducted an empirical study, using these four constraint optimization techniques in a well known test generation tool KLEE with 77 GNU Coreutils applications, to systematically investigate how these optimization techniques affect the efficiency of test generation. The experimental results show that these constraint optimization techniques as well as their combinations cannot improve the efficiency of test generation significantly for ALL-SIZED programs. Moreover, we studied the constraint optimization techniques with respect to two static metrics, lines of code (LOC) and cyclomatic complexity (CC), of programs. The experimental results show that the ``constraint set simplification'' technique can improve the efficiency of test generation significantly for the programs with high LOC and CC values. The ``constraint caching'' optimization technique can improve the efficiency of test generation significantly for the programs with low LOC and CC values. Finally, we propose four hybrid optimization strategies and practical guidelines based on different static metrics.


Acknowledgment

Acknowledgments

This work was supported in part by National Basic Research Program of China (973 Program) (Grant No. 2014CB340702) and National Natural Science Foundation of China (Grant Nos. 91418202, 61472178, 61373013).


References

[1] Beizer B. Software Testing Techniques. 2nd ed. New York: International Thomson Computer Press, 1990. Google Scholar

[2] Fang C R, Chen Z Y, Xu B W. Comparing logic coverage criteria on test case prioritization. Sci China Inf Sci, 2012, 55: 2826-2840 CrossRef Google Scholar

[3] Yang R, Chen Z Y, Zhang Z Y, et al. Efsm-based test case generation: sequence, data, and oracle. Int J Softw Eng Knowl Eng, 2015, 25: 633-667 CrossRef Google Scholar

[4] Orso A, Rothermel G. Software testing: a research travelogue (2000--2014). In: Proceedings of the IEEE International Conference on Future of Software Engineering (ICSE). New York: ACM, 2014. 117--132. Google Scholar

[5] King J C. Symbolic execution and program testing. Commun ACM, 1976, 19: 385-394 CrossRef Google Scholar

[6] Chen T, Zhang X-S, Guo S-Z, et al. State of the art: dynamic symbolic execution for automated test generation. Future Gener Comput Syst, 2013, 29: 1758-1773 CrossRef Google Scholar

[7] Anand S, Burke E K, Chen T Y, et al. An orchestrated survey of methodologies for automated software test case generation. J Syst Softw, 2013, 86: 1978-2001 CrossRef Google Scholar

[8] Cadar C, Dunbar D, Engler D R. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation. Berkeley: USENIX Association, 2008. 209--224. Google Scholar

[9] Cadar C, Ganesh V, Pawlowski P M, et al. Exe: automatically generating inputs of death. ACM Trans Inf Syst Secur, 2008, 12: 10-2001 Google Scholar

[10] Godefroid P, Klarlund N, Sen K. Dart: directed automated random testing. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. New York: ACM, 2005. 40: 213--223. Google Scholar

[11] Sen K, Marinov D, Agha G. CUTE: a concolic unit testing engine for C. In: Proceedings of the 10th European Software Engineering Conference Held Jointly With 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering. New York: ACM, 2005. 263--272. Google Scholar

[12] Barrett C, de Moura L, Stump A. Design and results of the first satisfiability modulo theories competition (smt-comp 2005). J Autom Reasoning, 2005, 35: 373-390 CrossRef Google Scholar

[13] Schittkowski K. NLPQL: a fortran subroutine solving constrained nonlinear programming problems. Ann Oper Res, 1986, 5: 485-500 CrossRef Google Scholar

[14] Cadar C, Engler D. Execution generated test cases: how to make systems code crash itself. In: Model Checking Software. Berlin: Springer, 2005. 2--23. Google Scholar

[15] Godefroid P, Levin M Y, Molnar D A, et al. Automated whitebox fuzz testing. In: Proceedings of the Network and Distributed System Security Symposium, San Diego, 2008. 8: 151--166. Google Scholar

[16] Brumley D, Newsome J, Song D, et al. Towards automatic generation of vulnerability-based signatures. In: Proceedings of IEEE Symposium on Security and Privacy, Berkeley/Oakland, 2006. 15--16. Google Scholar

[17] Brumley D, Newsome J, Song D, et al. Theory and techniques for automatic generation of vulnerability-based signatures. IEEE Trans Depend Secure Comput, 2008, 5: 224-241 CrossRef Google Scholar

[18] Brumley D, Wang H, Jha S, et al. Creating vulnerability signatures using weakest preconditions. In: Proceedings of the 20th IEEE Computer Security Foundations Symposium, Venice, 2007. 311--325. Google Scholar

[19] Liang Z K, Sekar R. Fast and automated generation of attack signatures: a basis for building self-protecting servers. In: Proceedings of the 12th ACM Conference on Computer and Communications Security. New York: ACM, 2005. 213--222. Google Scholar

[20] Newsome J, Brumley D, Song D. Vulnerability-specific execution filtering for exploit prevention on commodity software. In: Proceedings of the Network and Distributed System Security Symposium, San Diego, 2006. 58--71. Google Scholar

[21] Brumley D, Hartwig C, Kang M G, et al. Bitscope: Automatically Dissecting Malicious Binaries. School of Computer Science, Carnegie Mellon University, Technology Report CMU-CS-07-133. 2007. Google Scholar

[22] Brumley D, Hartwig C, Liang Z K, et al. Automatically identifying trigger-based behavior in malware. In: Botnet Detection. Berlin: Springer, 2008. 65--88. Google Scholar

[23] Moser A, Kruegel C, Kirda E. Exploring multiple execution paths for malware analysis. In: Proceedings of IEEE Symposium on Security and Privacy, Berkeley, 2007. 231--245. Google Scholar

[24] Song D, Brumley D, Yin H, et al. Bitblaze: a new approach to computer security via binary analysis. In: Information Systems Security. Berlin: Springer, 2008. 1--25. Google Scholar

[25] Chandra A K, Iyengar V S. Constraint solving for test case generation: a technique for high-level design verification. In: Proceedings of IEEE International Conference on Computer Design: VLSI in Computers and Processors, Cambridge, 1992. 245--248. Google Scholar

[26] DeMilli R A, Offutt A J. Constraint-based automatic test data generation. IEEE Trans Softw Eng, 1991, 17: 900-910 CrossRef Google Scholar

[27] Gotlieb A, Botella B, Rueher M. Automatic test data generation using constraint solving techniques. ACM SIGSOFT Softw Eng Notes, 1998, 23: 53-62 CrossRef Google Scholar

[28] Tovey C A. A simplified np-complete satisfiability problem. Discrete Appl Math, 1984, 8: 85-89 CrossRef Google Scholar

[29] Ganesh V, Dill D L. A decision procedure for bit-vectors and arrays. In: Computer Aided Verification. Berlin: Springer, 2007. 519--531. Google Scholar

[30] de Moura L, Bj{\o}rner N. Z3: an efficient smt solver. In: Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer, 2008. 337--340. Google Scholar

[31] Barrett C, Tinelli C. Cvc3. In: Computer Aided Verification. Berlin: Springer, 2007. 298--302. Google Scholar

[32] Palikareva H, Cadar C. Multi-solver support in symbolic execution. In: Computer Aided Verification. Berlin: Springer, 2013. 53--68. Google Scholar

[33] Jones C. Software metrics: good, bad and missing. Computer, 1994, 27: 98-100 CrossRef Google Scholar

[34] Shepperd M. A critique of cyclomatic complexity as a software metric. Softw Eng J, 1988, 3: 30-36 CrossRef Google Scholar

[35] Ferguson R, Korel B. The chaining approach for software test data generation. ACM Trans Softw Eng Meth, 1996, 5: 63-86 CrossRef Google Scholar

[36] Offutt A J, Hayes J H. A semantic model of program faults. ACM SIGSOFT Soft Eng Notes, 1996, 21: 195-200 CrossRef Google Scholar

[37] Brummayer R, Biere A. Boolector: an efficient smt solver for bit-vectors and arrays. In: Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer, 2009. 174--177. Google Scholar

[38] Erete I, Orso A. Optimizing constraint solving to better support symbolic execution. In: Proceedings of IEEE 4th International Conference on Software Testing, Verification and Validation Workshops (ICSTW), Berlin, 2011. 310--315. Google Scholar

Copyright 2019 Science China Press Co., Ltd. 《中国科学》杂志社有限责任公司 版权所有

京ICP备18024590号-1