Мансуров Н. Н., Майлингова О. Л. - Методы формальной спецификации программ - языки MSC и SDL, страница 2

596.5.2. Стартовый символ............................................................................... 596.5.3. Состояние............................................................................................. 606.5.4. Прием сигнала ..................................................................................... 606.5.5. Сохранение сигнала ............................................................................

616.5.6. Метки.................................................................................................... 626.5.7. Переход ................................................................................................ 626.5.8. Терминаторы переходов..................................................................... 636.5.9. Действия............................................................................................... 646.5.10. Условия .............................................................................................. 666.5.11.

Таймеры.............................................................................................. 666.6. Данные......................................................................................................... 676.7. Заключение ................................................................................................. 68Глава 7. Организатор системы SDT ....................................................................

697.1. Пример "Игральный автомат"................................................................... 697.2. Запуск системы SDT .................................................................................. 697.3. Работа с Организатором ............................................................................ 707.3.1. Окно Организатора .............................................................................

707.3.2. Настройка областей Организатора.................................................... 717.4. Работа с деревом SDL системы ............................................................... 727.4.1. Добавление корневого узла в дерево системы................................. 727.4.2. Сохранение дерева системы............................................................... 737.5.

Заключение ................................................................................................. 745Глава 8. Редактор диаграмм взаимодействия..................................................... 758.1. Создание диаграмм взаимодействия........................................................ 758.2. Редактирование диаграмм взаимодействия............................................. 768.3.

Заключение ................................................................................................. 80Глава 9. Редактор SDL диаграмм......................................................................... 819.1. Диаграмма системы ................................................................................... 819.1.1. Создание диаграммы системы ........................................................... 819.1.2. Редактирование диаграммы системы................................................ 839.1.3.

Добавление новых блоков.................................................................. 849.1.4. Перемещение символов и изменение их размеров.......................... 859.1.5. Создание каналов между блоками .................................................... 859.1.6. Создание каналов к окружению ........................................................ 869.1.7. Создание текстового символа ............................................................ 869.1.8. Сохранение диаграммы ...................................................................... 879.2.

Проверка синтаксиса диаграммы системы.............................................. 889.2.1. Запуск Анализатора ............................................................................ 889.2.2. Где искать сообщения о синтаксических ошибках ......................... 909.2.3. Как интерпретировать синтаксические ошибки .............................. 909.3. Диаграммы блоков .....................................................................................

919.3.1. Создание диаграммы блока из Организатора .................................. 919.3.2. Создание диаграммы блока по существующей копии .................... 939.4. Работа с несколькими диаграммами ........................................................ 959.5. Диаграммы процессов ............................................................................... 969.5.1. Создание диаграммы процесса .........................................................

969.5.2. Редактирование диаграммы процесса Demon................................. 969.5.3. Редактирование процесса Game ...................................................... 1009.5.4. Редактирование процесса Main ...................................................... 1039.6. Полный анализ системы .......................................................................... 1049.7. Заключение ............................................................................................... 105Глава 10.

Выполнение SDL спецификаций ...................................................... 10610.1. Создание исполняемой системы........................................................... 10610.2. Запуск спецификации на выполнение.................................................. 10710.3.

Выполнение переходов.......................................................................... 10810.3.1. Установка уровня детальности трассировки................................ 10910.3.2. Выполнение стартовых переходов системы ................................ 10910.3.3. Посылка сигналов из окружения системы ................................... 11010.3.4. Выполнение переходов................................................................... 11210.4. Исследование внешнего поведения системы ...................................... 11410.4.1. Протокол внешних сигналов.......................................................... 11410.4.2. Добавление новых кнопок к интерфейсу Монитора ...................

11510.4.3. Взаимодействие с системой ........................................................... 11610.4.4. Просмотр протокола внешних сигналов ..................................... 117610.5. Генерация диаграмм взаимодействия .................................................. 11710.5.1. Инициализация диаграммы взаимодействия .............................. 11810.5.2. Трассировка ..................................................................................... 11910.5.3. Переход к SDL символам ...............................................................

12310.5.4. Завершение трассировки ................................................................ 12410.6. Заключение ............................................................................................. 1247Глава 1. ВведениеНастоящий курс посвящен практическому применению формальныхметодов разработки программного обеспечения.

В курсе принята такназываемая прагматическая точка зрения на формальные методы, котораязаключается в том, что формальные методы применяются, в первую очередь,для достижения точности описаний разрабатываемой системы и, в меньшейстепени, для автоматического вывода и доказательства свойств системы. Врамках прагматического подхода, формальные спецификации представляютсобой форму документирования понимания системы.Важно помнить, что в современном процессе разработки сложнойпрограммной системы участвует большое количество специалистов, причемодновременно над одним проектом могут работать несколько географическираспределенных групп.

Кроме того, разработка предполагает проведениеразнообразныхвидовдеятельности,требующихвзаимодействияспециалистов различного профиля. Это означает, что окончательный продукт(т.е. исходные тексты системы, тесты, вспомогательные программы сборки иустановки и т.д.) отделены от исходного замысла системы большимколичествоммоделей.Отсюдаследуетактуальностьзадачидокументирования моделей, т.е. воплощения моделей в некоторую форму длясохранения, распространения среди коллектива разработчиков, а также дляанализа и верификации этих моделей.Назначение метода разработки (формального, строгого, илиструктурного) заключается, в первую очередь, в определении конкретнойформы моделей и последовательность их построения. В настоящее времяобщепризнана так называемая фазированная разработка, основанная напостроении формальных спецификаций и описаний системы.Мы будем рассматривать процесс разработки программногообеспечения, состоящий из пяти основных видов деятельности (фаз):Анализ требованийАнализ системыСистемное проектированиеДетальное проектированиеРеализацияНазначение фазы анализа требований (requirements analysis) состоит висследовании предметной области, для которой разрабатывается система, атакже в уточнении требований к системе.