Введение
Глава 1. Проблема разработки требований к поведению программ ных систем логического управления 9
1.1. Методы разработки требований к поведению программных систем логического управления
1.2. Постановка задачи разработки функциональных требований к поведению программных систем логического управления 18
1.3. Описание контекстных требований на языке LTL 26
1.4. Пример программной системы логического управления 32
Выводы по главе 1 35
Глава 2. Выявление и формализация контекстных требований 36
2.1. Проблема выявления темпоральных требований методом схем целей 36
2.2. Модификация метода схем целей для выявления контекстных требований 40
2.3. Трансляция схем контекстных требований в LTL–формулы 47
Выводы по главе 2 54
Глава 3. Символьный алгоритм трансляции LTL–формулы в автомат Бюхи 56
3.1. Постановка задачи трансляции LTL-формулы в автомат Бюхи 57
3.2. Символьная трансляция LTL-формулы в обобщенный автомат Бюхи 67
3.3. MINCFG: алгоритм построения сокращенной ДНФ в бинарных решающих диаграммах 80
3.4. Детали реализации алгоритма SymLTL2BA 89
3.5. Тестирование и сравнительный анализ реализации SymLTL2BA 99
Выводы по главе 3 104
Глава 4. Применение метода разработки формальных контекстных требований при верификации СУЭС 106
4.1. Объединение этапов метода разработки формальных контекстных требований 107
4.2. Разработка контекстных требований к СУЭС 112
4.3. Верификация контекстных требований к СУЭС 122
Выводы по главе 4 132
Заключение 134
Список сокращений и условных обозначений 135
Словарь терминов 136
Предметный указатель 137
Список литературы
