maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2013-6-22-35mais-155Research ArticleОригинальные статьиArticlesОбнаружение дефектов в программном обеспечении путем объединения ограниченной проверки моделей и аппроксимации функцийDefect Detection: Combining Bounded Model Checking and Code ContractsАхинМарат ХалимовичAkhinMarat

аспирант,

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

аспирант,

Polytechnicheskaya street, 21, Saint-Petersburg 194021 Russia

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

аспирант,

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

аспирант,

Polytechnicheskaya street, 21, Saint-Petersburg 194021 Russia

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

доцент,

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

доцент,

Polytechnicheskaya street, 21, Saint-Petersburg 194021 Russia

vlad@icc.spbstu.ruСанкт-Петербургский государственный политехнический университетРоссияSaint-Petersburg State Polytechnical UniversityRussian Federation2013201220132062235Copyright © Ахин М.Х., Беляев М.А., Ицыксон В.М., 20132013Ахин М.Х., Беляев М.А., Ицыксон В.М.Akhin M., 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/155

В последние годы такой метод обеспечения качества программного обеспечения (ПО), как ограниченная проверка моделей (Bounded Model Checking, BMC), исследуется все более и более активно, поскольку он позволяет успешно обнаруживать как функциональные, так и нефункциональные дефекты в реальном ПО. В данной статье предлагается оригинальный подход к реализации BMC, основанный на объединении результатов нескольких последних исследований в этой области: использовании системы компиляции LLVM для разбора и трансформации исходного кода, применении SMT-решателя Z3 для проверки свойств корректности и повышения эффективности анализа за счет аппроксимаций функций. Проведенные экспериментальные исследования показывают применимость подхода к реальным проектам.

Bounded model checking (BMC) of C/C++ programs is a matter of scientific enquiry that attracts great attention in the last few years. In this paper, we present our approach to this problem. It is based on combining several recent results in BMC, namely, the use of LLVM as a baseline for model generation, employment of high-performance Z3 SMT solver to do the formula heavy-lifting, and the use of various function summaries to improve analysis efficiency and expressive power. We have implemented a basic prototype; experiment results on a set of simple test BMC problems are satisfactory.  

ограниченная проверка моделейконтракт кодаинтерполяция КрейгаSMTобнаружение ошибокbounded model checkingsatisfiability modulo theoriesLLVMfunction contractsfunction summariesМинистерство образования и науки Российской ФедерацииReferencesClarke E., Kroening D., Lerda F. A Tool for Checking ANSI-C Programs // TACAS ’04. Springer-Verlag, 2004. P. 168–176.Clarke E., Kroening D., Lerda F. A Tool for Checking ANSI-C Programs // TACAS ’04. Springer-Verlag, 2004. P. 168–176.Armando A., Mantovani J., Platania L. Bounded Model Checking of Software using SMT Solvers instead of SAT Solvers // Int. J. Softw. Tools Technol. Transf. Springer-Verlag, 2009. 11, 1. P. 69–83.Armando A., Mantovani J., Platania L. Bounded Model Checking of Software using SMT Solvers instead of SAT Solvers // Int. J. Softw. Tools Technol. Transf. Springer-Verlag, 2009. 11, 1. P. 69–83.Cordeiro L., Fischer B., Marques-Silva J. SMT-Based Bounded Model Checking for Embedded ANSI-C Software // ASE ’09. IEEE. 2009. P. 137–148.Cordeiro L., Fischer B., Marques-Silva J. SMT-Based Bounded Model Checking for Embedded ANSI-C Software // ASE ’09. IEEE. 2009. P. 137–148.Merz F., Falke S., Sinz C. LLBMC: Bounded Model Checking of C and C++ Programs using a Compiler IR // VSTTE ’12. Springer-Verlag, 2012. P. 146–161.Merz F., Falke S., Sinz C. LLBMC: Bounded Model Checking of C and C++ Programs using a Compiler IR // VSTTE ’12. Springer-Verlag, 2012. P. 146–161.Ицыксон В.М., Глухих М.И. Язык спецификаций поведения программных компонентов // Научно-технические ведомости СПбГПУ. Информатика. Телекоммуникации. Управление. 3. СПб: СПбГПУ, 2010. С. 63–71. (Itsykson V., Glukhikh M. Yazyk specifikaciy povedeniya programmnyh komponentov // Nauchno-tehnicheskie vedomosti SPbGPU. Informatika. Telekommunikacii. Upravlenie. 3. SPb: SPbGPU, 2010. P. 63–71 [in Russian]).Ицыксон В.М., Глухих М.И. Язык спецификаций поведения программных компонентов // Научно-технические ведомости СПбГПУ. Информатика. Телекоммуникации. Управление. 3. СПб: СПбГПУ, 2010. С. 63–71. (Itsykson V., Glukhikh M. Yazyk specifikaciy povedeniya programmnyh komponentov // Nauchno-tehnicheskie vedomosti SPbGPU. Informatika. Telekommunikacii. Upravlenie. 3. SPb: SPbGPU, 2010. P. 63–71 [in Russian]).Ицыксон В. М., Зозуля А. В. Автоматизированная трансформация программ при миграции на новые библиотеки // Программная инженерия. 6. М: Новые Технологии, 2012 С. 8–14. (English transl.: Itsykson V., Zozulya A. Automated Program Transformation for Migration to New Libraries // SECR ’11. IEEE, 2011. P. 1–7).Ицыксон В. М., Зозуля А. В. Автоматизированная трансформация программ при миграции на новые библиотеки // Программная инженерия. 6. М: Новые Технологии, 2012 С. 8–14. (English transl.: Itsykson V., Zozulya A. Automated Program Transformation for Migration to New Libraries // SECR ’11. IEEE, 2011. P. 1–7).Baudin P., Filliˆatre J.C., Hubert T., March´e C., Monate B., Moy Y., Prevosto V. ACSL: ANSI/ISO C Specification Language. Preliminary Design, Version 1.4, 2008. http://www.frama-c.cea.fr/download/acsl_1.4.pdfBaudin P., Filliˆatre J.C., Hubert T., March´e C., Monate B., Moy Y., Prevosto V. ACSL: ANSI/ISO C Specification Language. Preliminary Design, Version 1.4, 2008. http://www.frama-c.cea.fr/download/acsl_1.4.pdfSery O., Fedyukovich G., Sharygina N. Interpolation-Based Function Summaries in Bounded Model Checking // HVC ’11. Springer-Verlag, 2011. P. 160–175.Sery O., Fedyukovich G., Sharygina N. Interpolation-Based Function Summaries in Bounded Model Checking // HVC ’11. Springer-Verlag, 2011. P. 160–175.Biere A., Cimatti A., Clarke E. M., Zhu Y. Symbolic Model Checking without BDDs // TACAS ’99. Springer-Verlag, 1999. P. 193–207.Biere A., Cimatti A., Clarke E. M., Zhu Y. Symbolic Model Checking without BDDs // TACAS ’99. Springer-Verlag, 1999. P. 193–207.Barrett C., Sebastiani R., Seshia S.A., Tinelli C. Satisfiability Modulo Theories // Handbook of Satisfiability. 185. Frontiers in Artificial Intelligence and Applications, 2009. P. 825–885.Barrett C., Sebastiani R., Seshia S.A., Tinelli C. Satisfiability Modulo Theories // Handbook of Satisfiability. 185. Frontiers in Artificial Intelligence and Applications, 2009. P. 825–885.Lattner C., Adve V. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation // CGO ’04. IEEE, 2004. P. 75–86.Lattner C., Adve V. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation // CGO ’04. IEEE, 2004. P. 75–86.Cytron R., Ferrante J., Rosen B.K., Wegman M.N., Zadeck F.K. Efficiently Computing Static Single Assignment Form and the Control Dependence Graph // ACM TOPLAS. 1991. 13, 4. P. 451–490.Cytron R., Ferrante J., Rosen B.K., Wegman M.N., Zadeck F.K. Efficiently Computing Static Single Assignment Form and the Control Dependence Graph // ACM TOPLAS. 1991. 13, 4. P. 451–490.McMillan K.L. Applications of Craig Interpolants in Model Checking // TACAS ’05. Springer-Verlag, 2005. P. 1–12.McMillan K.L. Applications of Craig Interpolants in Model Checking // TACAS ’05. Springer-Verlag, 2005. P. 1–12.Craig W. Three Uses of the Herbrand-Gentzen Theorem in Relating Model Theory and Proof Theory // The Journal of Symbolic Logic. 22, 3. Association for Symbolic Logic, 1957. P. 269–285.Craig W. Three Uses of the Herbrand-Gentzen Theorem in Relating Model Theory and Proof Theory // The Journal of Symbolic Logic. 22, 3. Association for Symbolic Logic, 1957. P. 269–285.De Moura L., Bjørner N. Z3: An Efficient SMT Solver // TACAS ’08. Springer-Verlag, 2008. P. 337–340.De Moura L., Bjørner N. Z3: An Efficient SMT Solver // TACAS ’08. Springer-Verlag, 2008. P. 337–340.Barrett C., De Moura L., Stump A. SMT-COMP: Satisfiability Modulo Theories Competition // CAV ’05. Springer-Verlag, 2005. P. 503–516.Barrett C., De Moura L., Stump A. SMT-COMP: Satisfiability Modulo Theories Competition // CAV ’05. Springer-Verlag, 2005. P. 503–516.Cok D.R., Griggio A., Bruttomesso R. The 2012 SMT Competition. 2012. http://smtcomp.sourceforge.net/2012/Cok D.R., Griggio A., Bruttomesso R. The 2012 SMT Competition. 2012. http://smtcomp.sourceforge.net/2012/Coverity. Open Source Report 2011. http://www.coverity.com/library/pdf/coverity-scan-2011-open-source-integrity-report.pdfCoverity. Open Source Report 2011. http://www.coverity.com/library/pdf/coverity-scan-2011-open-source-integrity-report.pdfNEC Laboratories. NECLA Static Analysis Benchmarks. 2013. http://www.nec-labs.com/research/system/systems_SAV-website/benchmarks.phpNEC Laboratories. NECLA Static Analysis Benchmarks. 2013. http://www.nec-labs.com/research/system/systems_SAV-website/benchmarks.php

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