Введение
Глава 1. Обзор существующих решений 13
1.1. Базовый подход решения задачи статической верификации 13
1.1.1. Постановка задачи статической верификации 14
1.1.2. Внутреннее представление программы 15
1.1.3. Абстрактная модель программы 17
1.1.4. Подход уточнения абстракции по контрпримерам (CEGAR) 18
1.2. Подготовка задачи статической верификации 20
1.2.1. Инструментирование исходного кода 21
1.2.2. Передача модели требования независимо от исходного кода 24
1.3. Системы верификации 25
1.3.1. Система Static Driver Verification 26
1.3.2. Система Linux Driver Verification Tools 26
1.3.3. Метод последовательной верификации 29
1.3.4. Метод пакетной верификации 30
1.4. Методы переиспользования информации в статической верификации 30
1.4.1. Адаптивный статический анализ 31
1.4.2. Условная проверка моделей 32
1.4.3. Регрессионная верификация 35
1.4.4. Перепроверка результатов верификации 39
1.4.5. Комбинирование тестирования и верификации 40
1.4.6. Проверка нескольких требований в смежных областях верификации...41
1.5. Выводы 42
Глава 2. Методы многоаспектной верификации 43
2.1. Подготовка задачи достижимости относительно композиции требований...43
2.1.1. Ограничение множества объединяемых моделей требований 43
2.1.2. Алгоритм объединения моделей требований 45
2.2. Метод обнаружения всех однотипных нарушений 47
2.2.1. Формализация эквивалентности трасс ошибок 50
2.2.2. Автоматическая фильтрация трасс ошибок 51
2.2.3. Полуавтоматическая фильтрация трасс ошибок 53
2.3. Алгоритм многоаспектной верификации 56
2.3.1. Представление утверждений 57
2.3.2. Аппроксимация с одним проверяемым утверждением 58
2.3.3. Остановка проверки утверждения 60
2.3.4. Полнота и корректность алгоритма 62
2.4. Расширения алгоритма многоаспектной верификации 63
2.4.1. Типы верификационных фактов
2.4.2. Стратегии корректировки уровня абстракции 64
2.4.3. Внутренние лимиты 64
2.4.4. Точки смены утверждений 65
2.4.5. Расширение используемой аппроксимации 66
2.4.6. Использование идей алгоритма вне подхода CEGAR 66
2.5. Метод условной многоаспектной верификации 67
2.5.1. Внешняя условная многоаспектная верификация 68
2.5.2. Внутренняя условная многоаспектная верификация
2.6. Метод условной многоаспектной верификации с обнаружением всех однотипных нарушений 72
2.7. Выводы 74
Глава 3. Методы декомпозиции автоматной спецификации 76
3.1. Метод автоматных спецификаций 76
3.1.1. Наблюдательные автоматы 77
3.1.2. Описание языка автоматных спецификаций 78
3.1.3. Сопоставление автоматных спецификаций с инструментированием 82
3.1.4. Автоматные спецификации в адаптивном статическом анализе 82
3.2. Метод декомпозиции автоматной спецификации 84
3.2.1. Общий алгоритм декомпозиции автоматной спецификации 85
3.2.2. Полнота и корректность метода 87
3.3. Стратегии разбиения в методе декомпозиции автоматной спецификации...88
3.3.1. Стратегия Совместная проверка 89
3.3.2. Стратегия Последовательная проверка 89
3.3.3. Стратегия Совместно-последовательная проверка 90
3.3.4. Стратегия Релевантность 91
3.4. Выводы 93
Глава 4. Реализация предложенных методов 95
4.1. Расширения системы верификации 95
4.1.1. Новая архитектура системы верификации 95
4.1.2. Формализация проверяемых требований 97
4.1.3. Объединение моделей требований 98
4.1.4. Поддержка метода условной многоаспектной верификации 99
4.1.5. Поддержка методов, основанных на автоматной спецификации 100
4.1.6. Поддержка методов обнаружения всех однотипных нарушений 101
4.2. Расширения статического верификатора 102
4.2.1. Метод условной многоаспектной верификации 103
4.2.2. Метод декомпозиции автоматной спецификации 107
4.2.3. Сравнение реализаций 107
4.3. Последовательная комбинация предложенных методов 109
4.4. Выводы 111
Глава 5. Экспериментальная оценка предложенных методов 112
5.1. Оценка метода последовательной верификации 115
5.2. Оценка метода пакетной верификации 115
5.3. Оценка метода обнаружения всех однотипных нарушений 116
5.4. Оценка метода условной многоаспектной верификации 118
5.5. Оценка метода условной многоаспектной верификации с обнаружением всех однотипных нарушений 121
5.6. Оценка метода автоматных спецификаций 122
5.7. Оценка метода декомпозиции автоматной спецификации 124
5.8. Сопоставление методов верификации композиции требований 125
5.9. Зависимость результата и ускорения от числа требований 128
5.10. Выводы 131
Заключение 133
Список сокращений и условных обозначений 134
Список используемой литературы 135
