Введение
1 Используемые формализмы 19
1 1 Определения, специфичные для части "Верификация" . 22
1 2 Определения, специфичные для предложенного расширения MSC 24
2 Верификация SDL диаграмм по MSC диаграммам 30
2 2 Постановка задачи 32
2 3 Алгоритм верификации , , , . 35
2 3.1 Обоснование меюда в терминах исходной задачи . 35
2.3.2 Реализация 39
233 Выбор начальной MSC диаграммы 41
2 4 Пример 43
2 5 Обработка сложных случаев . 44
2.5 1 Проверка при наличии в SDL коде конструкции Save 44
2 5.2 Уничтожение сообщений, не обрабатываемых в теку щей ситуации 47
2.5.3 На MSC диаграммах присутствует оператор парал лельного исполнения 48
2 6 Возможные усовершенствования и дальнейшее развитие метода - 49
2.7 Место подхода среди существующих методов . 50
3 Генерация SDL диаграмм no MSC диаграммам 52
З 1 Текущее состояние проблемы 53
ЗЛ1 Однократный перенос 53
ЗЛ.2 Согласование изменяющихся диаграмм 5G
ЗЛ.З Обобщение результатов 57
3 2 Предлагаемый подход 59
3.2Л Статические данные 62
3-2.2 Динамика 62
3 3 Базовый алгоритм генерации 63
3 ЗЛ Требования по корректности автомата 64
3 3.2 Идеи порождения базисных SDL элементов 64
3.3 3 Основная картина расклейки 66
3 3 4 Необходимость появления SDL элементов in основной картины расклейки 69
3 3 о Схема порождения описаний SDL элементов из основ ной картины расклейки 71
3.3,6 Алгоритмы порождения частей дерева кода 73
3.3-7 Алгоритм порождения всего SDL кода 77
3 4 Пример . 78
3 4 1 MSC диаграммы . 78
3 4 2 Недетерминированный автомат 79
3.4.3 Автомат без є-переходов 79
3 4 4 Детерминированный автомат 80
3 4.5 Детерминированный и минимизированный автомат 81
3.4.6 Построенные SDL диаграммы 81
3 5 Сравнение с ручным программированием и оптимизация имеющегося SDL кода 81
3 6 Улучшения базового алгоритма 84
3.6Л Краткий обзор базового алгоритма 84
3-6.2 Косметические улучшения 85
3 6 3 Порождение таймеров . 85
3.6.4 "Макроопределения" 85
3 6.5 Оптимальность автомата, "расщепление" деревьев . 86
366 Выделение процедур 87
3 6 7 Детермшппппацня по выходящим сообщениям . 89
3.6.8 Параллелизм 90
3.6.9 Обобщенный алгоритм разработки динамики системы 92
37 Выводы 94
4 Модификадия MS С диаграмм для описания обратных веток 95
4 1 Пример использования текущего стандарта MSC и его обсуждение 96
4 2 Предложенное решение . 99
4 2 1 Краткое описание расширения НЮ
4 2 2 Неформальное объяснение понятий блок17 и "суперблок" 101
4 2 3 Построение блоков при разборе грамматики . 104
4.2.4 Совместное использование графического и текстового описаний 107
4.2.5 Построение конечного автомата по расширенному МЯО описанию для выделенною обьекта. 108
4 3 Примеры . 111
4.3.1 Построение блоков по коду . 111
4 3 2 Описание примера из раздела
4.1 с помощью предложенного расширения MSC 112
4 4 Замечания к использованию 114
4 4.1 Использование Condition , 115
4.4 2 Корректное проектирование . 115
4 5 Сравнение с существующими работами . 117
4 6 Выводы 120
Заключение 121
Литература
