Р е б р и к о в
ПРОВЕРКА ВЫПОЛНЕНИЯ
ФУНКЦИОНАЛЬНЫХ ТРЕБОВАНИЙ
К АЛГОРИТМУ НА ОСНОВЕ СТРУКТУРНОЙ
ГЕНЕРАЦИИ МОДУЛЬНЫХ ТЕСТОВ
Разработан метод верификации алгоритмов, на базе дедуктивного подхода к проверке выполнения заданных требований. <...> Основой
метода является математическая модель описания наблюдаемого поведения алгоритма — элемента рефлексивно-транзитивного
замыкания путей в графе выполнения алгоритма. <...> При создании
метода предусмотрена возможность управления устранением цикломатической сложности за счет снижения точности метода и
использования жадных алгоритмов поиска. <...> E-mail: irudakov@yandex.ru, rebrikov_a@mail.ru
Ключевые слова: автоматизированная верификация, дедуктивный метод, структурная генерация тестов, наблюдаемое поведение алгоритмов. <...> Применение дедуктивных методов [1] для верификации алгоритмов сопряжено с ограниченностью спектра разрешимых задач c помощью теории [2], заложенной в используемый SMT-решатель [2]. <...> В то же время, путем расширения теории при дедуктивном подходе
верифицируемый алгоритм можно задавать на языке его реализации,
благодаря чему не требуется создание специализированных моделей,
как в системах, основанных на верификации состояний системы [3]. <...> При анализе функционирования сложных алгоритмов для полной, или
формальной, верификации [3, 4] требуются большие временные затраты, поэтому с целью их сокращения необходимо иметь возможность
проведения неполной верификации [5], посредством которой также
можно проводить проверку систем с нецелочисленной логикой, что
невозможно сделать при полной верификации. <...> Управляющим графом алгоритма называется кортеж [6]:
G = (N, E, n0 ),
где N — множество вершин, каждая из которых соответствует оператору алгоритма; E — множество дуг, соотвествующих переходу управления; n0 — стартовая вершина. <...> У
стартовой вершины n0 нет предков, и любая вершина графа достижима из нее. <...> На определенном графе удобно ввести следующие функции разметки:
f unc : N ×V → {F ∪∅}: каждой <...>