Разработка и исследование синтетического метода верификации программы с помощью SMT-решателей

Рассмотрена проблема разработки и исследования методов поиска недетерминированного поведения программного обеспечения. Методы верификации программного обеспечения предназначены для подтверждения фактов соответствия конечного программного продукта заявленным требованиям, целью верификации программного обеспечения является обнаружение ошибок, уязвимостей, некорректно реализованных свойств и требований. Существующие методы верификации имеют ряд проблем и недостатков. Предложен синтетический метод верификации программного обеспечения на основе SMT-решателя, позволяющий решить проблему комбинаторного взрыва, охватывающий все заданные свойства проверяемой программы, не требующий построения сложной модели программы. Получен алгоритм работы метода верификации и его реализации на языке SMT-LIB.

Литература

[1] Бурякова Н.А., Чернов А.В. Классификация частично формализованных и формальных моделей и методов верификации программного обеспечения // Электрон. науч. жур. "Инженерный вестник Дона". 2010. Т. 14. № 4. URL: http://www.ivdon.ru/ru/magazine/archive/n4y2010/259

[2] Вельдер С.Э., Шалыто А.А. Верификация простых автоматных программ на основе метода ModelChecking // Материалы XV Междунар. науч.-методич. конф. "Высокие интеллектуальные технологии и инновации в образовании и науке". 2008. C. 286.

[3] Holzmann G., Smith M. Software model checking: Extracting verification models from source code // Formal methods for protocol engineering and distributed systems. Kluwer Academic Publ., 1999. P. 481-497.

[4] Clarke E., Kroening D., Lerda F. A tool for checking ANSI-C programs // Tools and algorithms for the construction and analysis of systems (TACAS 2004) / Ed. by K. Jensen, A. Podelski. Vol. 2988 of Lecture Notes in Computer Science. Springer, 2004. P. 168-176.

[5] Counterexample-guided abstraction refinement / E. Clarke, O. Grumberg, S. Jha et al. // Computer Aided Verification. 2000. P. 154-169.

[6] Software verification with blast / T.A. Henzinger, R. Jhala, R. Majumdar, G. Sutre // 10th SPIN Workshop on Model Checking Software (SPIN). LNCS 2648. Springer-Verlag, 2003. P. 235-239.

[7] Cousot P. Abstract interpretation. ACM Computing Surveys (CSUR) // ACM. New York. 1996. Vol. 28. Iss. 2. P. 324-328.

[8] Глухих М.И., Ицыксон В.М., Цесько В.А. Использование зависимостей для повышения точности статического анализа программ // Модел. и анализ информ. систем. 2011. № 4. C. 72-73.

[9] Holzmann G., Peled D. An improvement in formal verification // FORTE 1994 Conference. 1994. P. 197-211.

[10] A partial order approach to branching time logic model checking / R. Gerth, R. Kuiper, D. Peled, W. Penczek // Inf. Comput. 1999. Vol. 150. No. 2. P. 132-152.

[11] Partial order reductions preserving simulations / W. Penczek, M. Szreter, R. Gerth, R. Kuiper // Proc. of Concurrency, Specification and Programming (CSP’99). Warsaw, 1999. P. 153-172.

[12] Holzmann G.J. An analysis of bitstate hashing // Formal methods in system design, 1998. Vol. 13. No. 3. Р. 287-307.

[13] Holzmann G.J. The spin model checker: Primer and Reference Manual. Addison-Wesley, 2003. 608 p.

[14] Вартанов С.П., Герасимов А.Ю. Динамический анализ программ с целью поиска ошибок и уязвимостей при помощи целенаправленной генерации входных данных // Сб. трудов ИСП РАН. 2014. Т. 26. Вып. 1. C. 375-394. DOI: 10.15514/ISPRAS-2014-26(1)-15 URL: http://www.ispras.ru/proceedings/isp_26_2014_1/isp_26_2014_1_375/

[15] Julien H., Monniaux D., Moy М. PAGAI: a path sensitive static analyzer. Grenoble-INP, VERIMAG Grenoble France, 2012. 14 p.

[16] Merz F., Falke S., Sinz С. LLBMC: Bounded model checking of C and C++ programs using a compiler IR. Institute for Theoretical Computer Science Karlsruhe Institute of Technology (KIT). Germany, 2012. 16 p.