УДК 519.876.5
И. В. Р у д а к о в, А. В. Р е б р и к о в
ПРОВЕРКА ВЫПОЛНЕНИЯ
ФУНКЦИОНАЛЬНЫХ ТРЕБОВАНИЙ
К АЛГОРИТМУ НА ОСНОВЕ СТРУКТУРНОЙ
ГЕНЕРАЦИИ МОДУЛЬНЫХ ТЕСТОВ
Разработан метод верификации алгоритмов, на базе дедуктивно-
го подхода к проверке выполнения заданных требований. Основой
метода является математическая модель описания наблюдаемо-
го поведения алгоритма — элемента рефлексивно-транзитивного
замыкания путей в графе выполнения алгоритма. При создании
метода предусмотрена возможность управления устранением ци-
кломатической сложности за счет снижения точности метода и
использования жадных алгоритмов поиска.
E-mail:
,
Ключевые слова
:
автоматизированная верификация, дедуктивный ме-
тод, структурная генерация тестов, наблюдаемое поведение алгорит-
мов.
Применение дедуктивных методов [1] для верификации алгорит-
мов сопряжено с ограниченностью спектра разрешимых задач c по-
мощью теории [2], заложенной в используемый SMT-решатель [2].
В то же время, путем расширения теории при дедуктивном подходе
верифицируемый алгоритм можно задавать на языке его реализации,
благодаря чему не требуется создание специализированных моделей,
как в системах, основанных на верификации состояний системы [3].
При анализе функционирования сложных алгоритмов для полной, или
формальной, верификации [3, 4] требуются большие временные затра-
ты, поэтому с целью их сокращения необходимо иметь возможность
проведения неполной верификации [5], посредством которой также
можно проводить проверку систем с нецелочисленной логикой, что
невозможно сделать при полной верификации.
Управляющим графом алгоритма называется кортеж [6]:
G
= (
N, E, n
0
)
,
где
N
—
множество вершин, каждая из которых соответствует опера-
тору алгоритма;
E
—
множество дуг, соотвествующих переходу упра-
вления;
n
0
—
стартовая вершина.
Множество
N
состоит из двух непересекающихся множеств
N
s
,
N
p
,
где
N
s
—
операторы, и у каждого
n
s
2
N
s
имеется не более одной
вершины-потомка, т.е.
9
!
n
j
2
N
:(
n
s
,
n
j
)
2
E
;
N
p
—
условные опе-
раторы, и у каждого из них существует конечное число потомков. У
стартовой вершины
n
0
нет предков, и любая вершина графа достижи-
ма из нее.
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012
67
