6 / 16
И.В. Рудаков, Р.Е. Гурин
54
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2016. № 4
нения операторов, которые эквиваленты с точки зрения результата, анализиро-
вать только один. Варианты выполнения статически выбираются до начала ис-
полнения программы.
Техника редукции частичных порядков позволяет сократить на 10…90
% объ-
ем используемой памяти и время выполнения программы верификации [11].
Метод collapse.
Глобальное состояние модели задается определенной ком-
бинацией состояний отдельных ее процессов и содержимого ее каналов. Каждое
глобальное состояние повторяет полное описание комбинации состояний про-
цессов. Данный вид представления является неэффективным с точки зрения
траты машинных ресурсов.
Метод collapse [12] позволяет разделить информацию о состояниях на две
составляющие:
глобальные данные модели, включая содержимое всех каналов;
управляющую информацию и состояние локальных переменных, исклю-
чая содержимое каналов, задаваемых для каждого процесса.
Cоставляющие хранятся отдельно, а в вектор состояния включаются индек-
сы, один из которых назначен для хранения глобальных данных и содержимого
каналов, а остальные — для процессов.
Метод collapse позволяет достичь уменьшения на 60…80 % объема исполь-
зуемой памяти при небольшом увеличении времени выполнения программы
верификации (10…20 %) [12].
Разработка синтетического метода верификации ПО.
В научной литера-
туре встречается множество описаний различных методов верификации ПО,
отметим, что характерной проблемой методов верификации является проблема
комбинаторного взрыва. Главная идея разрабатываемого метода — отход от
привычного бинарного представления пространства состояний к логическому.
Инструменты на основе Satisfiability Modulo Theories (SMT) решателей позво-
ляют сделать это (рис. 3), поскольку в основе SMT-решателя лежат формальные
методы такие, как доказательство теорем и дедуктивный анализ.
Рис. 3.
Упрощенное представление алгоритма верификации
Разрабатываемый метод верификации ПО обладает следующими характе-
ристиками:
осуществляет верификацию программ, написанных на языке Си;
использует синтетический метод верификации — осуществляет верифи-
кацию кода программы с помощью методов статического анализа и методов
формальной верификации;
допускает автоматическое и ручное создание тестовых случаев;