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

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

PDF-файл Мансуров Н. Н., Майлингова О. Л. - Методы формальной спецификации программ - языки MSC и SDL, страница 16 Формальная спецификация и верификация программ (63942): Книга - 9 семестр (1 семестр магистратуры)Мансуров Н. Н., Майлингова О. Л. - Методы формальной спецификации программ - языки MSC и SDL: Формальная спецификация и верификация программ - PDF, с2020-08-21СтудИзба

Описание файла

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Рис.

Свежие статьи
Популярно сейчас
А знаете ли Вы, что из года в год задания практически не меняются? Математика, преподаваемая в учебных заведениях, никак не менялась минимум 30 лет. Найдите нужный учебный материал на СтудИзбе!
Ответы на популярные вопросы
Да! Наши авторы собирают и выкладывают те работы, которые сдаются в Вашем учебном заведении ежегодно и уже проверены преподавателями.
Да! У нас любой человек может выложить любую учебную работу и зарабатывать на её продажах! Но каждый учебный материал публикуется только после тщательной проверки администрацией.
Вернём деньги! А если быть более точными, то автору даётся немного времени на исправление, а если не исправит или выйдет время, то вернём деньги в полном объёме!
Да! На равне с готовыми студенческими работами у нас продаются услуги. Цены на услуги видны сразу, то есть Вам нужно только указать параметры и сразу можно оплачивать.
Отзывы студентов
Ставлю 10/10
Все нравится, очень удобный сайт, помогает в учебе. Кроме этого, можно заработать самому, выставляя готовые учебные материалы на продажу здесь. Рейтинги и отзывы на преподавателей очень помогают сориентироваться в начале нового семестра. Спасибо за такую функцию. Ставлю максимальную оценку.
Лучшая платформа для успешной сдачи сессии
Познакомился со СтудИзбой благодаря своему другу, очень нравится интерфейс, количество доступных файлов, цена, в общем, все прекрасно. Даже сам продаю какие-то свои работы.
Студизба ван лав ❤
Очень офигенный сайт для студентов. Много полезных учебных материалов. Пользуюсь студизбой с октября 2021 года. Серьёзных нареканий нет. Хотелось бы, что бы ввели подписочную модель и сделали материалы дешевле 300 рублей в рамках подписки бесплатными.
Отличный сайт
Лично меня всё устраивает - и покупка, и продажа; и цены, и возможность предпросмотра куска файла, и обилие бесплатных файлов (в подборках по авторам, читай, ВУЗам и факультетам). Есть определённые баги, но всё решаемо, да и администраторы реагируют в течение суток.
Маленький отзыв о большом помощнике!
Студизба спасает в те моменты, когда сроки горят, а работ накопилось достаточно. Довольно удобный сайт с простой навигацией и огромным количеством материалов.
Студ. Изба как крупнейший сборник работ для студентов
Тут дофига бывает всего полезного. Печально, что бывают предметы по которым даже одного бесплатного решения нет, но это скорее вопрос к студентам. В остальном всё здорово.
Спасательный островок
Если уже не успеваешь разобраться или застрял на каком-то задание поможет тебе быстро и недорого решить твою проблему.
Всё и так отлично
Всё очень удобно. Особенно круто, что есть система бонусов и можно выводить остатки денег. Очень много качественных бесплатных файлов.
Отзыв о системе "Студизба"
Отличная платформа для распространения работ, востребованных студентами. Хорошо налаженная и качественная работа сайта, огромная база заданий и аудитория.
Отличный помощник
Отличный сайт с кучей полезных файлов, позволяющий найти много методичек / учебников / отзывов о вузах и преподователях.
Отлично помогает студентам в любой момент для решения трудных и незамедлительных задач
Хотелось бы больше конкретной информации о преподавателях. А так в принципе хороший сайт, всегда им пользуюсь и ни разу не было желания прекратить. Хороший сайт для помощи студентам, удобный и приятный интерфейс. Из недостатков можно выделить только отсутствия небольшого количества файлов.
Спасибо за шикарный сайт
Великолепный сайт на котором студент за не большие деньги может найти помощь с дз, проектами курсовыми, лабораторными, а также узнать отзывы на преподавателей и бесплатно скачать пособия.
Популярные преподаватели
Добавляйте материалы
и зарабатывайте!
Продажи идут автоматически
5173
Авторов
на СтудИзбе
436
Средний доход
с одного платного файла
Обучение Подробнее