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

И.В. Рудаков, Р.Е. Гурин

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

Существующие методы верификации программ, использующие доказатель-

ство теорем (теоретико-доказательный подход), основаны на методах доказа-

тельства теорем, например, группа средств «theoremprover», где описание и спе-

цификация программы являются ее представлением в виде множества логиче-

ских утверждений. Несмотря на значительный прогресс в области верификации

ПО методами теоретико-доказательного подхода, верификация большинства

программ требует участия эксперта.

Методы проверки моделей (ModelChecking (MC)) позволяют осуществить

проверку свойств ПО с помощью построения и анализа формальной модели

программы. Как правило, в качестве модели используется модель Крипке [2],

которая формально задается следующим образом:

( , , , ),

M S S R L



где

—

множество состояний;

—

множество начальных состояний;

R S S

 

— отно-

шение переходов;

L D



— функция разметки. Модель программы пред-

ставляет собой систему переходов, включающую в себя множество состояний

модели, множество ее начальных состояний и отношения переходов на множе-

стве состояний. Каждое состояние модели определяется значениями булевых

переменных модели. Спецификация программы задается с помощью формул

темпоральной логики, которые в отличие от формул классической логики, где

истинность не зависит от времени, учитывают зависимость истинности форму-

лы от момента времени. Это позволяет описать свойства поведения программы,

реакции процессов на события, связь между процессами и событиями и т.

д.

Задача проверки выполнимости темпоральных формул является разрешимой,

так как состояние модели конечно.

Методы MC имеют ряд недостатков, что ограничивает их применение:



невозможно определить, охватывает ли заданная спецификация все

свойства, которым должна удовлетворять система;



сложность построения наиболее полной модели программы;



наличие эффекта комбинаторного взрыва;



требование конечного числа состояния модели.

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

ному набору спецификаций. Поэтому модель должна отражать все свойства

программы, которые необходимы для проверки спецификации. Модель должна

соответствовать поведению исходной программы. Адекватность модели прове-

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

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

лей [3] по заданной программе. Подход Counter Example Guided Abstraction

Refinement осуществляет построение модели за счет комбинирования методов

булевой абстракции с итеративной верификацией моделей [4–6] .

Эффект комбинаторного взрыва появляется в результате экспоненциально-

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

щих процессов. Алгоритмы MC не являются полиноминальными, время реше-

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

да. Задачи верификации МС имеют экспоненциальную сложность, что при