Обнаружение дефектов в программном обеспечении путем объединения ограниченной проверки моделей и аппроксимации функций


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

Просмотров: 285

Обратные ссылки

  • Обратные ссылки не определены.


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)