ПРОВЕРКА ВЫПОЛНЕНИЯ ФУНКЦИОНАЛЬНЫХ ТРЕБОВАНИЙ К АЛГОРИТМУ НА ОСНОВЕ СТРУКТУРНОЙ ГЕНЕРАЦИИ МОДУЛЬНЫХ ТЕСТОВ

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

АНАЛИЗ СТЕПЕНИ НЕОБНАРУЖИМОСТИ КОНФИДЕНЦИАЛЬНОЙ ИНФОРМАЦИИ, СКРЫВАЕМОЙ С ИСПОЛЬЗОВАНИЕМ СПЕЦИАЛЬНОЙ ФАЙЛОВОЙ СИСТЕМЫ, ЗАДАЧА ВЫБОРА СРЕДСТВ ЗАЩИТЫ В АВТОМАТИЗИРОВАННЫХ СИСТЕМАХ С УЧЕТОМ КЛАССОВ ЗАЩИЩЕННОСТИ ОТ НЕСАНКЦИОНИРОВАННОГО ДОСТУПА К ИНФОРМАЦИИ, ...

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

• Похожие документы из РУАЭСТ
• |
• Похожие документы из Руконт