Введение
Глава 1. Исследование проблемы 12
1.1. Задача верификации 12
1.1.1. Экспертиза 15
1.1.2. Статический анализ 17
1.1.3. Динамические методы верификации 18
1.1.4. Синтетические методы верификации 19
1.1.5. Формальные методы верификации 20
1.1.6. Классификация методов верификации программного обеспечения 21
1.1.7. Актуальность верификации 24
1.1.8. Международные стандарты верификации 26
1.2. Model Checking. Верификация больших распределенных программных систем 27
1.2.1. Возникновение больших распределенных программных систем 29
1.2.2. Возникновение метода Model Checking 32
1.2.3. Идея алгоритма Model Checking 32
1.2.4. Логика линейного времени LTL и алгоритм Model Checking 34
1.2.5. Инструменты верификации для метода Model Checking 36
1.2.6. Примеры верификации распределенных программных систем 37
1.3. Проблема избыточности верифицируемого множества вычислительных последовательностей, ускорение процесса верификации БРПС 38
1.3.1. Темпы роста сложности программных систем 38
1.3.2. Ускорение процесса верификации БРПС 40
1.3.3. Избыточность верифицируемых моделей 42
1.4. Выводы по главе 43
Глава 2. Вопросы повышения эффективности верификации больших распределенных программных систем 45
2.1. Метод ограничений верифицируемых моделей 45
2.1.1. Ограничение моделей программных систем 46
2.1.2. Ограничение моделей распределенных программных систем 51
2.1.3. Эффективность метода ограничения моделей 55
2.1.4. Расширение метода ограничений 58
2.2. Распределенный метод верификации моделей 60
2.2.1. Инструмент формальной верификации «Spin» 61
2.2.1.1. Распределенная верификация в Spin. 63
2.2.2. Распределенный алгоритм верификации автоматов Бюхи 66
2.2.2.1. Поиск допустимых состояний 67
2.2.2.2. Поиск циклов из допустимых состояний 68
2.2.2.3. Суперлинейное ускорение 69
2.2.2.4. Результаты 72
2.2.2.5. Сравнение со Spin 76
2.3. Выводы по главе 78
Глава 3. Эквациональная характеристика LTL 81
3.1. Расширение выразительности LTL 82
3.1.1. Эквациональная характеристика операторов LTL (RLTL) 84
3.1.2. Примеры описания свойств в RLTL-нотации 85
3.1.3. Верификация RLTL 88
3.1.4. Формальный вывод 91
3.2. Абстракция моделей на базе RLTL 92
3.3. Выводы по главе 94
Глава 4. Разработка и апробация программного комплекса верификации больших распределенных систем 96
4.1. Реализация системы анализа и метода верификации для больших распределенных программных систем 96
4.1.1. Спецификация системы 97
4.1.1.1. Диаграмма вариантов использования 97
4.1.1.2. Диаграмма классов 98
4.1.1.3. Диаграмма последовательности 101
4.1.1.4. Диаграмма взаимодействия 104
4.1.1.5. Диаграмма активности
4.1.2. Выбор языка программирования 106
4.1.3. Результаты разработки 108
4.2. Апробация комплекса 116
4.2.1. Работа с комплексом и тестирование примеров 116
4.2.1.1. Тестирование примера верификации микроволновой печи 117
4.2.1.2. Тестирование примера верификации большой системы 125
4.2.2. Внедрение комплекса 127
4.3. Выводы по главе 128
Заключение 130
Список сокращений и условных обозначений 133
Список литературы 134
