Введение
1. Основные определения и обозначения 22
1.1 Конечные автоматы 22
1.2 Расширенные автоматы 28
1.3 Параллельная композиция автоматов 30
1.4 Модели неисправности и проверяющие тесты 32
1.5 Краткий обзор по тестированию программного обеспечения на основе формальных моделей 33
1.6 Методы синтеза тестов для расширенных автоматов 40
1.7 Статический и динамический анализ безопасности программного обеспечения 42
1.8 Выводы по главе 1 42
2. Синтез проверяющих тестов с гарантированной полнотой по модели расширенного автомата 44
2.1 Инструмент \\Java для мутационного тестирования программных реализаций 45
2.2 Расширенный автомат для протокола SCP (Simple Connection Protocol) 46
2.3 Метод построения проверяющего теста с использованием инструмента \Java 47
2.4 Построение различающих последовательностей для расширенных автоматов
2.4.1 Построение различающей последовательности на основе пересечения двух расширенных автоматов 51
2.4.2 Построение различающей последовательности на основе автоматных абстракций двух расширенных автоматов 52
2.4.3 Построение различающей последовательности на основе предикатных абстракций двух расширенных автоматов 53
2.4.4 Построение различающей последовательности на основе контекстно свободных срезов двух расширенных автоматов 55
2.4.5 Построение различающих последовательностей для специальных классов расширенных автоматов 57 2.5 Анализ качества построенных тестов на примере Audio-CD плеера и
протокола Simple Connection Protocol 58
2.5.1 Audio-CD плеер 58
2.5.2 Протокол Simple Connection Protocol
2.6 Локализация неисправностей в сети из конечных автоматов 64
2.7 Выводы по главе 2 69
3. Построение проверяющих последовательностей для недетерминированных автоматов 71
3.1 Модель неисправности и адаптивная проверяющая последовательность 73
3.2 Алгоритм построения адаптивной проверяющей последовательности при наличии разделяющей последовательности
3.2.1 Общие определения 75
3.2.2 Построение множества Separate 78
3.2.3 Построение множества Transition 79
3.2.4 Иллюстрация алгоритма на примере 82
3.3 Построение адаптивной проверяющей последовательности с использованием (адаптивного) различающего примера 84
3.3.1 Дополнительные определения 85
3.4 Использование уникально достижимых состояний 92
3.4.1 Уникально достижимые состояния 93
3.4.2 Построение адаптивной различающей последовательности с использованием различающего тестового примера и уникально достижимых состояний
3.5 О возможности построения адаптивной проверяющей последовательности для частичных наблюдаемых автоматов 103
3.6 Заключение и выводы по главе 3 104
4. Проверка безопасности по с использованием верификаторов 105
4.1 Программы-верификаторы 106
4.1.1 Анализатор Spin 106
4.1.2 Анализатор Java Path Finder 107
4.2 Результаты экспериментов по оценке эффективности обнаружения уязвимостей статическими методами 109
4.3 Алгоритм поиска уязвимостей, основанный на использовании верификаторов 110
4.3.1 Общий алгоритм поиска уязвимостей на основе верификаторов 110
4.3.2 Общее описание процесса обнаружения уязвимостей 112
4.3.3 Уязвимости «переполнения типа» 112
4.3.4 Уязвимости «переполнения приведения типа» и «переполнения массива» 113
4.3.5 Уязвимости повторного освобождения и повторного выделения памяти 114
4.4 Краткое описание разработанного КПП 115
4.4.1 Архитектура разработанного ПО 115
4.4.2 ППП по статическому анализу 117
4.4.3 ППП по трансляции 118
4.4.4 ППП по внедрению служебных инструкций 120
4.5 Компьютерные эксперименты с разработанным КПП для обнаружения уязвимостей в C программах 120
4.5.1 Описание тестовых программ 121
4.5.2 Поиск среднего значения элементов в массиве 121
4.5.3 Сортировка массива методом пузырька 123
4.5.4 Программная реализация алгоритма сортировки массива методом вставки 124
4.5.5 Программа поиска минимального и максимального элемента массива 1 4.6 Результаты экспериментов 125
4.7 Выводы по главе 4 129
Заключение 130
Список использованной литературы 132
