maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2014-6-83-93mais-73Research ArticleОригинальные статьиArticlesИспользование метода ограниченной проверки моделей для генерации тестовUsing a Bounded Model Checker for Test Generation: How to Kill Two Birds with One SMT-solverПетровМаксим АлексеевичPetrovMaxim

аспирант, 195251, Россия, г. Санкт-Петербург, Политехническая ул., 29

аспирант, Polytechnicheskaya street, 29, Saint-Petersburg 195251 Russia

maxim.petrov@kspt.icc.spbstu.ruГагарскийКирилл АлексеевичGagarskiKirill

исследователь, 195251, Россия, г. Санкт-Петербург, Политехническая ул., 29

исследователь, Polytechnicheskaya street, 29, Saint-Petersburg 195251 Russia

gagarski@kspt.icc.spbstu.ruБеляевМихаил АнатольевичBelyaevMikhail

аспирант, 195251, Россия, г. Санкт-Петербург, Политехническая ул., 29

аспирант, Polytechnicheskaya street, 29, Saint-Petersburg 195251 Russia

belyaev@kspt.icc.spbstu.ruИцыксонВладимир МихайловичItsyksonVladimir

доцент, 195251, Россия, г. Санкт-Петербург, Политехническая ул., 29

доцент, Polytechnicheskaya street, 29, Saint-Petersburg 195251 Russia

vlad@icc.spbstu.ruСанкт-Петербургский государственный политехнический университетРоссияSaint-Petersburg State Polytechnic UniversityRussian Federation2014201220142168393Copyright © Петров М.А., Гагарский К.А., Беляев М.А., Ицыксон В.М., 20142014Петров М.А., Гагарский К.А., Беляев М.А., Ицыксон В.М.Petrov M., Gagarski K., Belyaev M., Itsykson V.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/73

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

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

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

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

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.

автоматическая генерация тестовдинамическое символьное выполнениеограниченная проверка моделейконтракты кодаSMTautomated test generationdynamic symbolic executionbounded model checkingsatisfiability modulo theoriesfunction contractsReferencesMarat Akhin, Mikhail Belyaev, and Vladimir Itsykson. Yet another defect detection: Combining bounded model checking and code contracts // PSSV’13. 2013. P. 1–11.Marat Akhin, Mikhail Belyaev, and Vladimir Itsykson. Yet another defect detection: Combining bounded model checking and code contracts // PSSV’13. 2013. P. 1–11.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.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.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.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.Kent Beck. Test-driven development: by example. Addison-Wesley Professional, 2003.Kent Beck. Test-driven development: by example. Addison-Wesley Professional, 2003.Boris Beizer. Software testing techniques. Dreamtech Press, 2003.Boris Beizer. Software testing techniques. Dreamtech Press, 2003.Dirk Beyer. Competition on software verification // TACAS’12. Springer, 2012. P. 504–524.Dirk Beyer. Competition on software verification // TACAS’12. Springer, 2012. P. 504–524.Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. Symbolic model checking without BDDs // TACAS’9. 1999. P. 193–207.Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. Symbolic model checking without BDDs // TACAS’9. 1999. P. 193–207.Edmund Clarke, Daniel Kroening, and Flavio Lerda. A tool for checking ANSI-C programs // TACAS’04. 2004. P. 168–176.Edmund Clarke, Daniel Kroening, and Flavio Lerda. A tool for checking ANSI-C programs // TACAS’04. 2004. P. 168–176.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.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.Lucas Cordeiro, Bernd Fischer, and Joao Marques-Silva. SMT-based bounded model checking for embedded ANSI-C software // ASE’09. 2009. P. 137–148.Lucas Cordeiro, Bernd Fischer, and Joao Marques-Silva. SMT-based bounded model checking for embedded ANSI-C software // ASE’09. 2009. P. 137–148.Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. 2008. P. 337–340.Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. 2008. P. 337–340.RA DeMilli and A. Jefferson Offutt. Constraint-based automatic test data generation // Software Engineering, IEEE Transactions on. 1991. 17(9). P. 900–910.RA DeMilli and A. Jefferson Offutt. Constraint-based automatic test data generation // Software Engineering, IEEE Transactions on. 1991. 17(9). P. 900–910.Patrice Godefroid, Nils Klarlund, and Koushik Sen. DART: directed automated random testing // ACM Sigplan Notices. ACM, 2005. Vol. 40. P. 213–223.Patrice Godefroid, Nils Klarlund, and Koushik Sen. DART: directed automated random testing // ACM Sigplan Notices. ACM, 2005. Vol. 40. P. 213–223.Richard Hamlet. Random testing // Encyclopedia of software Engineering, 1994.Richard Hamlet. Random testing // Encyclopedia of software Engineering, 1994.Franjo Ivanˇci´c and Sriram Sankaranarayanan. NECLA static analysis benchmarks.Franjo Ivanˇci´c and Sriram Sankaranarayanan. NECLA static analysis benchmarks.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.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.Chris Lattner. LLVM and Clang: Next generation compiler technology // The BSD Conference, 2008.Chris Lattner. LLVM and Clang: Next generation compiler technology // The BSD Conference, 2008.Chris Lattner and Vikram Adve. LLVM: A compilation framework for lifelong program analysis & transformation // CGO’04. 2004. P. 75–86.Chris Lattner and Vikram Adve. LLVM: A compilation framework for lifelong program analysis & transformation // CGO’04. 2004. P. 75–86.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.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.Bertrand Meyer. Applying ‘design by contract’ // Computer. 1992. 25(10). P. 40–51.Bertrand Meyer. Applying ‘design by contract’ // Computer. 1992. 25(10). P. 40–51.Glenford J Myers, Corey Sandler, and Tom Badgett // The art of software testing. John Wiley & Sons, 2011.Glenford J Myers, Corey Sandler, and Tom Badgett // The art of software testing. John Wiley & Sons, 2011.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.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.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.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.Koushik Sen, Darko Marinov, and Gul Agha. CUTE: a concolic unit testing engine for C // ACM, 2005. Vol. 30.Koushik Sen, Darko Marinov, and Gul Agha. CUTE: a concolic unit testing engine for C // ACM, 2005. Vol. 30.Nikolai Tillmann and Jonathan De Halleux. Pex—white box test generation for .Net // Tests and Proofs. Springer, 2008. P. 134–153.Nikolai Tillmann and Jonathan De Halleux. Pex—white box test generation for .Net // Tests and Proofs. Springer, 2008. P. 134–153.Tao Xie, Nikolai Tillmann, Jonathan de Halleux, and Wolfram Schulte. Fitness-guided path exploration in dynamic symbolic execution // IEEE, 2009. P. 359–368.Tao Xie, Nikolai Tillmann, Jonathan de Halleux, and Wolfram Schulte. Fitness-guided path exploration in dynamic symbolic execution // IEEE, 2009. P. 359–368.

The authors declare that there are no conflicts of interest present.