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

ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2016. № 4

УДК 004.3+519.6

DOI: 10.18698/0236-3933-2016-4-49-64

РАЗРАБОТКА И ИССЛЕДОВАНИЕ СИНТЕТИЧЕСКОГО МЕТОДА

ВЕРИФИКАЦИИ ПРОГРАММЫ С ПОМОЩЬЮ SMT-РЕШАТЕЛЕЙ

И.В. Рудаков

irudakov@yandex.ru

Р.Е. Гурин

rg.bmstu@gmail.com

МГТУ им. Н.Э. Баумана, Москва, Российская Федерация

Аннотация

Ключевые слова

Рассмотрена проблема разработки и исследования методов

поиска недетерминированного поведения программного

обеспечения. Методы верификации программного обеспе-

чения предназначены для подтверждения фактов соответ-

ствия конечного программного продукта заявленным тре-

бованиям, целью верификации программного обеспечения

является обнаружение ошибок, уязвимостей, некорректно

реализованных свойств и требований. Существующие мето-

ды верификации имеют ряд проблем и недостатков. Пред-

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

обеспечения на основе SMT-решателя, позволяющий ре-

шить проблему комбинаторного взрыва, охватывающий все

заданные свойства проверяемой программы, не требующий

построения сложной модели программы. Получен алгоритм

работы метода верификации и его реализации на языке

SMT–LIB

Верификация, анализ кода,

статический анализ, дина-

мический анализ, интерпре-

тация, символьное выполне-

ние, проверка модели

Поступила в редакцию 09.09.2015

Основным методом верификации программного обеспечения (ПО) в настоящее

время является тестирование. При тестировании ПО на вход тестовой про-

граммы подается подготовленный пользователем набор данных, далее проверя-

ется, соответствует ли выданный программой результат ожидаемому [1]. Одним

из важных свойств тестирования является возможность выполнять помимо

статической проверки кода еще и динамическую.

Исторически первым методом проверки ПО на наличие ошибок и уязви-

мостей стала экспертиза (review). Экспертиза может быть применима к любым

свойствам ПО на любом этапе проекта и позволяет выявить практически

любые виды ошибок и уязвимостей, это минимизирует число ошибок и их

последствия в конечном программном продукте. Одним из минусов этого мето-

да является невозможность его автоматизации и активное участие людей

при верификации ПО. В связи с этим наряду с существующими методами вери-

фикации, особое внимание уделяется автоматизированным методам верифи-

кации ПО.