Введение
Глава 1. Анализ методов повышения качества и надежности СПО ИУС 8
1.1. Специфика СПО ИУС 8
1.2. Методы повышения качества и надежности ПО ИУС 16
1.2.1. Использование образцов17
1.2.2. Тестирование. 18
1.2.3. Повторное использование компонент 20
1.2.4. Использование средств автоматической генерации кода 20
1.2.5. Использование средств сквозного цикла разработки 22
1.2.6. Использование систем контроля требований 22
1.2.7. Построение и верификация моделей 23
1.3. Построение и верификация моделей СПО ИУС 25
1.3.1. Модель СПО 25
1.3.2. Моделирование СПО 27
1.3.3. Верификация моделей СПО 32
1.3.4. Современные средства построения и верификации моделей ПО 36
1.4. Постановка задачи 45
Глава 2. Методы построения и верификации моделей СПО ИУС... 48
2.1. Основные понятия. Классификация объектов СПО ИУС 48
2.2. Выбор базового метода построения и верификации моделей 56
2.3. Анализ базового метода построения и верификации моделей ПО 58
2.4. Метод построения и верификации моделей СПО ИУС 64
2.4.1. Входные данные метода 64
2.4.2. Выходные данные метода 65
2.4.3. Определение и классификация требований 66
2.4.4. Общая последовательность этапов метода 68
2.4.5. Специфика этапов метода в зависимости от типа модели СПО 73
2.4.5.1. Особенности при исследовании архитектуры СПО 73
2.4.5.2. Особенности при исследовании КВМ СПО 75
2.5. Особенности метода построения и верификации моделей СПО ИУС 77
2.5.1. Выбор форматов для этапа построения моделей 77
2.5.2. Выбор форматов отчетов верификации 82
2.5.3. Дополнительные операции темпоральной логики 84
2.5.4. Образцы требований с различными областями видимости 85
2.5.5. Интеграция cMSDev 87
2.5.6. Интеграция с системой контроля версий 88
2.5.7. Классификация элементов моделей 89
2.5.8. Выбор формата описания элементов моделей 90
2.5.9. Таблица описания библиотеки элементов 91
2.6. Библиотека элементов моделей 93
Выводы 106
Глава 3. Исследование характеристик методов построения и верификации моделей СПО ИУС 107
3.1. Исследование базового и расширенного методов 108
3.2. Исследование расширенного метода и метода на основе SMV 114
Выводы 118
Глава 4. Исследование и разработка моделей СПО ИУС 120
4.1. Исследование архитектуры СПО (модель драйвера Windows NT)... 120
4.2. Исследование критически важного механизма арбитража активности резервированных модулей 125
Выводы , 131
Заключение 132
Список литературы 135
Приложение 1 145
Приложение 2 147
Приложение 3 152
