Using a Bounded Model Checker for Test Generation: How to Kill Two Birds with One SMT-solver
https://doi.org/10.18255/1818-1015-2014-6-83-93
Abstract
The automated test generation has received a lot of attention in the last decades as it is one of possible solutions to software testing inherent problems: the need to write tests and providing test coverage in presence of human factor. The most promising technique of generating a test automatically is the dynamic symbolic execution assisted by an automated constraint solver, e. g., an SMT-solver. This process is very similar to the bounded model checking, which also has to deal with generating models from a source code, asserting logic properties in it and process the returned model. This paper describes a prototype unit test generator for C based on a working bounded model checker called Borealis and shows that these two techniques are very similar and can be easily implemented by using the same basic components. The prototype test generator was sampled on a number of examples and showed good results in terms of test coverage and test excessiveness.
About the Authors
Maxim Petrov
Saint-Petersburg State Polytechnic University
Russian Federation
аспирант, Polytechnicheskaya street, 29, Saint-Petersburg 195251 Russia
Russian Federation
аспирант, Polytechnicheskaya street, 29, Saint-Petersburg 195251 Russia
Kirill Gagarski
Saint-Petersburg State Polytechnic University
Russian Federation
исследователь, Polytechnicheskaya street, 29, Saint-Petersburg 195251 Russia
Russian Federation
исследователь, Polytechnicheskaya street, 29, Saint-Petersburg 195251 Russia
Mikhail Belyaev
Saint-Petersburg State Polytechnic University
Russian Federation
аспирант, Polytechnicheskaya street, 29, Saint-Petersburg 195251 Russia
Russian Federation
аспирант, Polytechnicheskaya street, 29, Saint-Petersburg 195251 Russia
Vladimir Itsykson
Saint-Petersburg State Polytechnic University
Russian Federation
доцент, Polytechnicheskaya street, 29, Saint-Petersburg 195251 Russia
Russian Federation
доцент, Polytechnicheskaya street, 29, Saint-Petersburg 195251 Russia
References
1. Marat Akhin, Mikhail Belyaev, and Vladimir Itsykson. Yet another defect detection: Combining bounded model checking and code contracts // PSSV’13. 2013. P. 1–11.
2. Alessandro Armando, Jacopo Mantovani, and Lorenzo Platania. Bounded model checking of software using SMT solvers instead of SAT solvers // Int. J. Softw. Tools Technol. Transf. 2009. 11(1). P. 69–83.
3. Patrick Baudin, Jean C. Filliˆatre, Thierry Hubert, Claude March´e, Benjamin Monate, Yannick Moy, and Virgile Prevosto // ACSL: ANSI/ISO C Specification Language. Preliminary Design, version 1.4, 2008., preliminary edition, may 2008.
4. Kent Beck. Test-driven development: by example. Addison-Wesley Professional, 2003.
5. Boris Beizer. Software testing techniques. Dreamtech Press, 2003.
6. Dirk Beyer. Competition on software verification // TACAS’12. Springer, 2012. P. 504–524.
7. Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. Symbolic model checking without BDDs // TACAS’9. 1999. P. 193–207.
8. Edmund Clarke, Daniel Kroening, and Flavio Lerda. A tool for checking ANSI-C programs // TACAS’04. 2004. P. 168–176.
9. David M Cohen, Siddhartha R Dalal, Jesse Parelius, and Gardner C Patton. The combinatorial design approach to automatic test generation // IEEE software. 1996. 13(5). P. 83–88.
10. Lucas Cordeiro, Bernd Fischer, and Joao Marques-Silva. SMT-based bounded model checking for embedded ANSI-C software // ASE’09. 2009. P. 137–148.
11. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. 2008. P. 337–340.
12. RA DeMilli and A. Jefferson Offutt. Constraint-based automatic test data generation // Software Engineering, IEEE Transactions on. 1991. 17(9). P. 900–910.
13. Patrice Godefroid, Nils Klarlund, and Koushik Sen. DART: directed automated random testing // ACM Sigplan Notices. ACM, 2005. Vol. 40. P. 213–223.
14. Richard Hamlet. Random testing // Encyclopedia of software Engineering, 1994.
15. Franjo Ivanˇci´c and Sriram Sankaranarayanan. NECLA static analysis benchmarks.
16. Anil Kumar and J St Clair. Cunit-a unit testing framework for c // Diposnıvel em: http://cunit. sourceforge. net/doc/index. html. Acesso em, 25, 2005.
17. Chris Lattner. LLVM and Clang: Next generation compiler technology // The BSD Conference, 2008.
18. Chris Lattner and Vikram Adve. LLVM: A compilation framework for lifelong program analysis & transformation // CGO’04. 2004. P. 75–86.
19. Florian Merz, Stephan Falke, and Carsten Sinz. LLBMC: Bounded model checking of C and C++ programs using a compiler IR // VSTTE’12. 2012. P. 146–161.
20. Bertrand Meyer. Applying ‘design by contract’ // Computer. 1992. 25(10). P. 40–51.
21. Glenford J Myers, Corey Sandler, and Tom Badgett // The art of software testing. John Wiley & Sons, 2011.
22. Clementine Nebut, Franck Fleurey, Yves Le Traon, and J-M Jezequel. Automatic test generation: A use case driven approach // Software Engineering, IEEE Transactions on. 2006. 32(3). P. 140–155.
23. Carlos Pacheco, Shuvendu K Lahiri, Michael D Ernst, and Thomas Ball. Feedback-directed random test generation // Software Engineering, 2007. ICSE 2007. 29th International Conference on. IEEE, 2007. P. 75–84.
24. Koushik Sen, Darko Marinov, and Gul Agha. CUTE: a concolic unit testing engine for C // ACM, 2005. Vol. 30.
25. Nikolai Tillmann and Jonathan De Halleux. Pex—white box test generation for .Net // Tests and Proofs. Springer, 2008. P. 134–153.
26. Tao Xie, Nikolai Tillmann, Jonathan de Halleux, and Wolfram Schulte. Fitness-guided path exploration in dynamic symbolic execution // IEEE, 2009. P. 359–368.
Review
For citations:
Petrov M., Gagarski K., Belyaev M., Itsykson V. Using a Bounded Model Checker for Test Generation: How to Kill Two Birds with One SMT-solver. Modeling and Analysis of Information Systems. 2014;21(6):83-93. (In Russ.) https://doi.org/10.18255/1818-1015-2014-6-83-93
Views:
964
Email this article 