Обнаружение дефектов в программном обеспечении путем объединения ограниченной проверки моделей и аппроксимации функций
https://doi.org/10.18255/1818-1015-2013-6-22-35
Аннотация
В последние годы такой метод обеспечения качества программного обеспечения (ПО), как ограниченная проверка моделей (Bounded Model Checking, BMC), исследуется все более и более активно, поскольку он позволяет успешно обнаруживать как функциональные, так и нефункциональные дефекты в реальном ПО. В данной статье предлагается оригинальный подход к реализации BMC, основанный на объединении результатов нескольких последних исследований в этой области: использовании системы компиляции LLVM для разбора и трансформации исходного кода, применении SMT-решателя Z3 для проверки свойств корректности и повышения эффективности анализа за счет аппроксимаций функций. Проведенные экспериментальные исследования показывают применимость подхода к реальным проектам.
Ключевые слова
При поддержке: Министерство образования и науки Российской Федерации
Об авторах
Марат Халимович Ахин
Санкт-Петербургский государственный политехнический университет
Россия
Россия
аспирант,
194021, Россия, г. Санкт-Петербург, Политехническая ул., 21
Михаил Анатольевич Беляев
Санкт-Петербургский государственный политехнический университет
Россия
Россия
аспирант,
194021, Россия, г. Санкт-Петербург, Политехническая ул., 21
Владимир Михайлович Ицыксон
Санкт-Петербургский государственный политехнический университет
Россия
Россия
доцент,
194021, Россия, г. Санкт-Петербург, Политехническая ул., 21
Список литературы
1. Clarke E., Kroening D., Lerda F. A Tool for Checking ANSI-C Programs // TACAS ’04. Springer-Verlag, 2004. P. 168–176.
2. 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.
3. Cordeiro L., Fischer B., Marques-Silva J. SMT-Based Bounded Model Checking for Embedded ANSI-C Software // ASE ’09. IEEE. 2009. P. 137–148.
4. 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.
5. Ицыксон В.М., Глухих М.И. Язык спецификаций поведения программных компонентов // Научно-технические ведомости СПбГПУ. Информатика. Телекоммуникации. Управление. 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. Ицыксон В. М., Зозуля А. В. Автоматизированная трансформация программ при миграции на новые библиотеки // Программная инженерия. 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).
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.pdf
8. Sery O., Fedyukovich G., Sharygina N. Interpolation-Based Function Summaries in Bounded Model Checking // HVC ’11. Springer-Verlag, 2011. P. 160–175.
9. Biere A., Cimatti A., Clarke E. M., Zhu Y. Symbolic Model Checking without BDDs // TACAS ’99. Springer-Verlag, 1999. P. 193–207.
10. 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.
11. Lattner C., Adve V. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation // CGO ’04. IEEE, 2004. P. 75–86.
12. 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.
13. McMillan K.L. Applications of Craig Interpolants in Model Checking // TACAS ’05. Springer-Verlag, 2005. P. 1–12.
14. 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.
15. De Moura L., Bjørner N. Z3: An Efficient SMT Solver // TACAS ’08. Springer-Verlag, 2008. P. 337–340.
16. Barrett C., De Moura L., Stump A. SMT-COMP: Satisfiability Modulo Theories Competition // CAV ’05. Springer-Verlag, 2005. P. 503–516.
17. Cok D.R., Griggio A., Bruttomesso R. The 2012 SMT Competition. 2012. http://smtcomp.sourceforge.net/2012/
18. Coverity. Open Source Report 2011. http://www.coverity.com/library/pdf/coverity-scan-2011-open-source-integrity-report.pdf
19. NEC Laboratories. NECLA Static Analysis Benchmarks. 2013. http://www.nec-labs.com/research/system/systems_SAV-website/benchmarks.php
Рецензия
Для цитирования:
Ахин М.Х., Беляев М.А., Ицыксон В.М. Обнаружение дефектов в программном обеспечении путем объединения ограниченной проверки моделей и аппроксимации функций. Моделирование и анализ информационных систем. 2013;20(6):22-35. https://doi.org/10.18255/1818-1015-2013-6-22-35
For citation:
Akhin M., Belyaev M., Itsykson V. Defect Detection: Combining Bounded Model Checking and Code Contracts. Modeling and Analysis of Information Systems. 2013;20(6):22-35. (In Russ.) https://doi.org/10.18255/1818-1015-2013-6-22-35
Просмотров:
1087
Послать статью по эл. почте 