Использование метода ограниченной проверки моделей для генерации тестов

В настоящее время автоматическая генерация тестов исследуется все более и более активно, поскольку является решением многих проблем, связанных с тестированием программного обеспечния (ПО), таких как необходимость написания тестов и обеспечения тестового покрытия с учетом человеческого фактора.

Наиболее перспективным методом автоматической генерации тестов является динамическое символьное исполнение (dynamic symbolic execution, DSE), выполняемое с помощью автоматического решателя ограничений, например SMT-решателя. Данный метод во многом похож на метод ограниченной проверки моделей, который также предполагает построение моделей из исходного кода, проверку логических свойств на них и обработку полученной модели.

В данной работе рассматривается метод генерации модульных тестов для языка C, основанный на методе ограниченной проверки моделей. Показано, что эти методы имеют много общего и могут быть реализованы с использованием общих базовых компонентов. Реализован прототип средства генерации тестов, основанный на работающем средстве ограниченной проверки моделей Borealis.

Прототип средства был опробован на множестве примеров и показал хорошие результаты с точки зрения полноты тестового покрытия и избыточности тестового набора.

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.