Мансуров Н. Н., Майлингова О. Л. - Методы формальной спецификации программ - языки MSC и SDL, страница 16
Описание файла
PDF-файл из архива "Мансуров Н. Н., Майлингова О. Л. - Методы формальной спецификации программ - языки MSC и SDL", который расположен в категории "". Всё это находится в предмете "формальная спецификация и верификация программ" из 9 семестр (1 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 16 страницы из PDF
Графическая трасса показывает некоторое будущеесобытие, которое произойдет при выполнении следующего перехода (причемпервый символ нового перехода может оказаться на диаграмме другогопроцесса).2.Выполните очередной переход процесса Game, нажав на кнопкуTransition. Процесс Game переходит в состояние Losing и графическаятрасса возвращается в процесс Demon.3.Выполните очередной переход (на котором должно произойтисрабатывание таймера). На данном переходе таймер посылает сигналпроцессу, который произвел установку данного таймера. Срабатываниетаймера считается отдельным переходом.
Обратите внимание на то, что наданном переходе произошло увеличение модельного времени.*** TIMER signal was sent*Timer:T*Receiver:Demon:1*** NOW: 1.00004. Выполните очередной переход. Исходное состояние данного переходахарактеризуестя состоянием Generate и получением сигнала таймера T.На данном переходе происходит посылка сигнала Bump процессу Game:*** TRANSITION START*Pid: Demon:1*State: Generate*Input: T*Sender : Demon:1*Now: 1.0000*OUTPUT ofBump to Game:1*SET on timer T at 2.0000*** NEXTSTATEGenerateГрафическая трасса показывает, что следующим символом будет приемсигнала Bump в процессе Game.
Как видно на диаграмме, после получения113сигнала Bump процесс Game попадет в состоянии Winning, в котором будетожидать приема сигнала Probe (либо нового сигнала Bump).5. Выполните очередной переход для перевода процесса Game в состояниеWinning. Графическая трасса возвращается в процесс Demon ипоказывает, что при отсутствии внешних сигналов следующим событиембудет срабатывание таймера T, Вместо этого, пошлем сигнал Probe изокружения системы:6. Пошлите сигнал Probe, используя кнопку Send Via. Графическая трассавозвращается в процесс Game.7.
Выполните следующий переход. На данном переходе происходит приемсигнала Probe и посылка сигнала Win в окружение системы. ПроцессGame возвращается в состояние Winning и ждет сигнала Probe илисигнала Bump.*************TRANSITION STARTPId: Game:1State: WinningInput: ProbeSender : env:1Now:1.0000OUTPUT of Win to env:1ASSIGN Count := 1NEXTSTATE Winning10.4. Исследование внешнего поведения системыПосле выполнения упражнений данного раздела вы должны научиться:- перезапускать исполняемую систему;- использовать возможность протоколирования внешних сигналов;- добавлять новые кнопки на панель управления Монитором;- выполнять все переходы в течение заданного интервала времени.10.4.1. Протокол внешних сигналов1.
Перезапустите исполняемую систему: выберите команду Restart из менюFile окна Монитора. Дополнительный диалог запросит подтверждениязавершения текущей трассы. Нажмите кнопку OK. Окно сообщений114Монитора очищается и исполняемая система приводится в начальноесостояние.2. Установите уровень детальности трассы равный 1. Это означает, чтотрасса будет показывать только взаимодействие системы с окружением,т.е. сигналы из окружения и в окружение.3. Для включения протокола внешних сигналов введите команду signal-log вполе ввода команды и нажмите клавишу <Return>. Для данной командыне существует стандартной кнопки на панели управления Монитором.Команда имеет два параметра, значения которых запрашиваются вдополнительных диалогах.
Первый параметр – это имя SDL объекта, длякоторого нужен протокол сигналов. В окне представлен список всехобъектов в системе.4. Введите название объекта env в текстовое поле ввода в нижней частиокна. Этот объект означает окружение системы.Рис. 56. Включение протокола внешних сигналов5. Второй параметр команды signal-log является именем файла, вкоторый направляется протокол внешних сигналов. Появляетсястандартный диалог выбора файла. Введите имя файла signal.log вполе File.10.4.2. Добавление новых кнопок к интерфейсу МонитораГрафический интерфейс Монитора позволяет добавлять новые кнопки напанель управления Монитором и связывать с ними произвольные команды.1151. Выберите группу кнопок Send Signal.
Выберите команду Add из менюGroup для данной группы.Рис. 57. Добавление новой кнопки к группе2. В дополнительном диалоге введите Newgame как метку новой кнопки вполе Label. Не нажимайте клавишу <Return> !. Введите output-vianewgame – в поле Definition. Последний параметр “-“ в команде output-viaозначает значение по-умолчанию (эквивалент нажатию на кнопку OK) всоответствующем диалоге.Рис. 58. Добавление кнопки3. Завершите выполнение команды, нажав на кнопку Apply. Новая кнопкапоявляется в группе, диалог может быть использован для определенияновой кнопки.4. Добавьте кнопку для посылки сигналов Probe, Result и Endgame.5.
Завершите диалог, нажав кнопку OK.10.4.3. Взаимодействие с системой1. Пошлите сигнал Newgame, нажав на новую кнопку Newgame.1162. Выполните все переходы до достижения модельного времени равного 5.5.Для этого нажмите кнопку Until Time в группе Execute. Введите значение5.5.3. Пошлите сигнал Probe.4. Выполните все переходы до достижения модельного времени 10.3.Обратите внимание на то, какой сигнал был послан системой в окружение(Win или Lose?).5. Пошлите два сигнала Probe подряд.6. Пошлите сигнал Result.7. Выполните все переходы до достижения модельного времени 13.5.Обратите внимание на то, какие сигналы были посланы системой вокружение.10.4.4.
Просмотр протокола внешних сигналов1. Завершите выполнение исполняемой программы, нажав кнопку Stop Sim вгруппе Execute. По этой команде выключится протокол внешних событий.Окно Монитора при этом остается активным.2. Файл signal.log должен содержать протокол внешних сигналовисполняемой системы:Signal log for system Demongame with unit Process envon file …0.0000 Newgame from env:1 to Main:15.5000Probe from env:1 to Game:15.5000Win from Game:1 to env:110.3000 Probe from env:1 to Game:110.3000 Probe from env:1 to Game:110.3000 Result from env:1 to Game:110:3000 Lose from Game:1 to env:110:3000 Lose from Game:1 to env:110:3000 Score from Game:1 to env:1Parameter(s) : 110.5.
Генерация диаграмм взаимодействияВ данном упражении мы рассмотрим способы автоматической генерациидиаграмм взаимодействия по исполняемой системы. Монитор SDL позволяетпредставлять основные события SDL системы в виде событий диаграмм117взаимодействия. Это позволяет визуализировать трассу SDL системы в видедиаграммы взаимодействия.После выполнения упражнений данного урока вы должны научиться:- включать и выключать генерацию диаграммы взаимодействия;- переходить от символов диаграммы взаимодействия к символам SDL;- выполнять отдельный SDL символ.10.5.1. Инициализация диаграммы взаимодействия1. Перезапустите исполняемую систему.2. Отключите графическую трассу для того, чтобы избежать появления окнаредактора SDL диаграмм.
Для этого нажмите на кнопку SDL Level : Show вгруппе Trace и убедитесь, что уровень детальности графической трассы(GR Trace) установлен в 0.3. Для включения генерации диаграмм взаимодействия нажмите кнопку MSCTrace : Start в группе Trace. Выполнение данной команды приводит кпоявлению дополнительного диалога для задания уровни детальностидиаграммы взаимодействия. Выберите 1 для генерации диаграммвзаимодействия с символами состояний. Завершите выполнение команды,нажав кнопку OK.Рис. 59. Выбор уровня детальности диаграммы взаимодействия1184.
Через несколько секунд появится редактор диаграмм взаимодействия, вкотором открыта диаграмма с именем”SimulatorTrace”.Надиаграмме присутствуют три объекта: процессы Main_1_1, Demon_1_2и процесс env_0 (представляющий собой окружение системы):Рис. 60. Начальный вид диаграммы взаимодействия10.5.2. Трассировка1. Пошлите сигнал Newgame из окружения системы. Посылка сигналапредставляется на диаграмме взаимодействия как сообщение от объектаenv_0 к объекту Main_1_1. На данном этапе, сообщение помеченозвездочкой на конце, означающей, что сообщение еще не принятопроцессом - получателем. (В ряде случаев появление звездочки можетозначать возникновение ошибки в спецификации, например, посылкасигнала несуществующему процессу).
Заметим, что символ посылкисообщения, помеченный звездочкой, является расширением языкадиаграмм взаимодействия, принятым в системе SDT.2. Выполните очередной переход. На оси объекта процесса Main появляетсясимвол состояния Game_Off. Данный символ означает, что процесс Mainзавершил переход и находится в соответствующем SDL состоянии.3. Выполните очередной переход. На данном переходе процесс Demonустанавливает таймер T.4. Выполните очередной SDL символ. Для этого нажмите на кнопкуSymbol в группе Execute на панели управления монитора. ПроцессMain принимает сигнал Newgame. На диаграмме взаимодействия это119представляется как снятие звездочки.
Обратите внимание на то, что точкипосылки и приема сообщения Newgame находятсяна разныхвертикальных уровнях, т.к. таймер T был установлен после того, как былопослано сообщение.5. Выполните следующий SDL символ (нажав на кнопку Symbol в группеExecute). Происходит создание экземпляра процесса Game. На диаграммевзаимодействия это представляется как появление нового объекта.Диаграмма взаимодействия на данный момент должна выглядетьследующим образом.Рис. 61.
Вид диаграммы взаимодействия после создания процесса Game.6. Завершите текущий переход и выполните следующий переход, нажав двараза на кнопку Transition. Второй переход переводит процесс Game всостояние Losing.7. Выполните следующие три перехода. Происходит прием сигнала таймераT, а также прием и посылка сигнала Bump. Процесс Game находится в120состоянии Winning. Обратите внимание на представление обменасообщениями на диаграмме взаимодействия.8.
Покажем, как на диаграмме взаимодействия представляется немедленныйприем сообщения. Пошлите сигнал Probe из окружения системы ивыполните следующий SDL символ. Сначала появляется символсообщения, помеченный звездочкой, а затем отметка снимается, носимвол сохраняет горизинтальное положение.9. Завершите текущий переход.
Система посылает сигнал Win своемуокружению.10.Пошлите сигнал Result из окружения системы и выполните очереднойпереход. На диаграмме взаимодействия появится сообщение Score спараметром 1.11.Завершите игру, послав сигнал Endgame и выполнив два перехода.Происходит остановка процесса Game.121Рис.