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

Разработка и исследование синтетического метода верификации программы…

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

возрастающей сложности алгоритма и экспоненциальный рост пространства

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

тельно увеличивают время проверки программы.

Алгоритмы MC эффективно работают и гарантированно завершаются только

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

ным числом состояний используют два направления: верификация моделей с бес-

конечным числом состояний и верификация параметризированных моделей.

Поскольку большинство используемых методов и программных средств для

верификаций ПО требуют участия экспертов, которые сталкиваются с пробле-

мой комбинаторного взрыва, задача реализации метода верификации, миними-

зирующего эффект комбинаторного взрыва, а также оценка его параметров и

генерация соответствующих тестовых случаев являются актуальными.

Цель настоящей работы — разработка и исследование алгоритма верифи-

кации ПО, решающего проблему комбинаторного взрыва.

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

вать последствия комбинаторного взрыва при верификации ПО.

Эффект

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

стояний при линейном росте числа взаимодействующих процессов. Послед-

ствиями экспоненциального роста состояний являются значительно возросшие

требования к объему памяти, используемой верификатором, а также возрастает

время проверки модели. Для сжатия верифицируемого множества состояний

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

двоичные решающие диаграммы BDD (Binary Decision Diagrams) [7]. В этом

случае описываемые объекты (множества, функции, матрицы) кодируются гра-

фовой структурой в соответствии с определенными правилами. Часто такое

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

леннее, чем размер соответствующего описания. Кроме того, операции над

представленными объектами, выполняются за полиномиальное время от раз-

мера соответствующих графов. Алгоритмы BDD могут быть значительно эф-

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

бинарное решающее дерево остается компактным.

Для борьбы с комбинаторным взрывом при верификации моделей программ

используются методы редукции частичных порядков [8



10]. В этих методах про-

веряется достаточное подмножество множества всех трасс. Такое подмножество

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

Типы проверяемых зависимостей выявляются эмпирически. Верный выбор правил

редукции может существенно ускорить алгоритм верификации моделей.

Бинарные решающие диаграммы.

Диаграммы BDD являются экономной

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

ного графа.

Бинарная решающая диаграмма представляет собой функцию вида

: {0, 1}

n S



которая является ориентированным корневым ациклическим графом с

множеством вершин

V T N T N

    

Вершины множества

называются