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

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

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

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

PDF-файл из архива "Мансуров Н. Н., Майлингова О. Л. - Методы формальной спецификации программ - языки MSC и SDL", который расположен в категории "". Всё это находится в предмете "формальная спецификация и верификация программ" из 9 семестр (1 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .

Просмотр PDF-файла онлайн

Текст 11 страницы из PDF

Терминаторы переходов6.5.8.1. Символ перехода в состояниеСимвол перехода в новое состояние определяет, в каком состоянии процессбудет ожидать следующего сигнала. <dash nextstate> означает, что изменениясостояния не происходит. Конструкция <dash nextstate> оказывается особенноценной при организации помеченных участков графа.Графический синтаксис:<nextstate area><nextstate body><dash nextstate><state name> ::=::= <state symbol> contains <nextstate body>::= { <state name> | <dash nextstate> }::= <name>6.5.8.2.

Символ перехода на меткуСимвол перехода на метку осуществляет передачу управления на новыйучасток перехода. Заметим, что явная передача управления на текущий переходявляется единственным средством организации циклов.Графический синтаксис:<merge area> ::= <merge symbol> is connected to<flow line symbol><merge symbol> ::= <flow line symbol><flow line symbol> ::=<out-connector area> ::= <out-connector symbol> contains<connector name><out-connector symbol> ::= <in-connector symbol>6.5.8.3. Символ остановкиВыполнение остановки процесса приводит к уничтожению всех переменныхпроцесса и всех необработанных сигналов из входного порта процесса.Графический синтаксис:<stop symbol> ::=636.5.8.4.

Символ возврата из процедурыВозврат из процедуры означаеткотором произошел вызов процедуры.продолжение того перехода, наГрафический синтаксис:<return area> ::= <return symbol>[ is associated with <expression> ]<return symbol> ::=6.5.9. Действия6.5.9.1.

ПрисваиваниеГрафический синтаксис:<task area> ::= <task symbol> contains <assignment statement><task symbol> ::=6.5.9.2. Создание процессаГрафический синтаксис:<create request area> ::= <create request symbol>contains <create body><create request body> ::= <name> [ <actual parameters> ]<actual parameters> ::= ( <expression> { , <expression> }* )<create request symbol> ::=Динамическое поведение SDL системы описывается внутри процессов.Процессы могут создаваться при запуске системы, а также могут создаватьсяи уничтожаться динамически во время выполнения системы. Можетсуществовать более одного экземпляра одного и того же процесса. Каждыйэкземпляр процесса имеет уникальный идентификатор PId.

Это делаетвозможным посылку сигнала конкретному экземпляру процесса.Формальные параметры процесса получают свои значения при егосоздании. У экземпляров процессов, которые создаются статически, значенияформальных параметров неопределены.64У каждого процесса есть четыре стандартные переменные типа PId:- Собственный идентификатор процесса (переменная self);- Идентификатор родительского процесса (переменная parent);- Идентификатор последнего процесса, порожденного данным процессом(переменная child);- Идентификатор процесса, от которого был получен последнийполученный сигнал (переменная sender).При попытке создания лишних экземпляров процесса (т.е. больше чем<maximum number>, новый экземпляр не создается, переменная offspringполучает значение Null, а выполнение перехода продолжается.6.5.9.3.

Вызов процедурыГрафический синтаксис:<procedure call area> ::= <procedure call symbol> contains<procedure call body><procedure call body> ::= <name> [ <actual parameters> ]<procedure call symbol> ::=6.5.9.4. Посылка сигналаПри посылке сигнала можно явно указать маршрут, по которому долженбыть направлен сигнал (конструкция via), либо процесс-получатель(конструкция to) в одной из двух форм: либо имя процесса-получателя, либоуникальный PId процесса-получателя. Если при посылке сигнала указаноимя процесса-получателя, то сигнал попадет к произвольному экземплярупроцесса с данным именем (если таковые вообще существуют).Графический синтаксис:<output area> ::= <output symbol> contains <output body><output body> ::= <signal name> [ <actual parameters> ][ to <destination> ] [ via <via path> ]<destination> ::= <Pid expression> | <name><via path> ::= <channel name>| <signal route name><signal name> ::= <name><channel name> ::= <name><signal route name> ::= <name><output symbol> ::=656.5.10.

УсловияГрафический синтаксис:<decision area> ::= <decision symbol> contains <question>is followed by{ { <graphical answer part><graphical else part> }*| { <graphical answer part> {<graphical answer part>}+[ <graphical else part> ] }*<decision symbol> ::=<graphical answer part> ::= <flow line symbol>is associated with <graphical answer>is followed by <transition area><graphical else part> ::= <flow line symbol> is associated with<else answer>is followed by <transition area><graphical answer> ::= <range condition><else answer> ::= else6.5.11.

ТаймерыГрафический синтаксис:<timer definition> ::= timer <timer name> [ <sort list> ][ := <Duration ground expression> ]<set area> ::= <task symbol> contains <set><reset area> ::= <task symbol> contains <reset><set> ::= set <set statement><set statement> ::= ( [ <Time expression> ,] <timer name>[ ( <expression list>) ] )<reset> ::= reset ( <reset statement> )<reset statement> ::= <timer name> [ ( <expression list> ) ]<timer name> ::= <name><Time expression> ::= <expression><Duration expression> ::= <expression>66Рис.

14. Пример диаграммы процесса6.6. ДанныеОсновным механизмом описания данных в языке SDL являютсяалгебраические спецификации абстрактных типов данных. Абстрактный типданных – это тип данных, внутреннее устройство которого не определено.Вместо этого, для абстрактного типа данных задаются набор литералов,набор операторов и набор аксиом, которым эти операторы должныудовлетворять. Подробное рассмотрение алгебраических спецификацийабстрактных типов данных в данном пособии не предусмотрено.В языке SDL имеется набор предопределенных типов данных:Integer, Real, Natural, Boolean, Character, Duration, Time, Charstring, PId.Ниже приводится упрощенный синтаксис выражений в языке SDL.Графический синтаксис:<range condition> ::= { <closed range> | <open range> }{ , { <closed range> | <open range> } }*<closed range> ::= <constant> : <constant>67<open range> ::= <constant>| { = | /= | < | > | <= | >= } <constant><expression> ::= <sub expression><sub expression> ::= <operand0> | <sub expression> => <operand0><operand0> ::= <operand1> | <operand0> {or | xor } <operand1><operand1> ::= <operand2> | <operand1> and <operand2><operand2> ::= <operand3>| <operand2> {= | /= | > |>= | < | <= | in } <operand3><operand3> ::= <operand4> | <operand3> { + | - | // } <operand4><operand4> ::= <operand5> |<operand4>{*|/|mod|rem } <operand5><operand5> ::= [ - | not ] <primary><primary> ::= <name>| ( <expression> )6.7.

ЗаключениеВ данном разделе мы подробно рассмотрели основные возможности языкаспецификаций и описаний SDL.Мы рассмотрели основные структурные единицы языка SDL: систему,блок, процесс и процедуру. Мы также рассмотрели организациювзаимодействия процессов через посылки сигналов по статическиммаршрутам, состоящих из межблочных и межпроцессных каналов, связанныхсоединениями. Мы рассмотрели средства описания поведения процесса какрасширенного конечного автомата.Отметим, что некоторые возможности языка остались за рамками нашегорассмотрения:• Структурные типы- Определение структурных типов- Использование типизированных объектов- Наследование структурных типов- Специализация структурных типов- Специализация поведения процессов- Определения пакетов• Алгебраические спецификации абстрактных типов данных• Процедурные определения операторов абстрактных типов данных68Глава 7. Организатор системы SDTДанная часть пособия представляет собой практическое руководство поредактору SDL диаграмм системы SDT.

Предполагается, что все упражнения,описанные в данном разделе, будут проделаны на компьютере. В следующихглавах мы будем разрабатывать MSC и SDL спецификации примера"Игральный автомат".7.1. Пример "Игральный автомат"Внешнее поведение системы выглядит следующим образом. Системавоспринимает четыре типа входных сигналов: Newgame (новая игра),Endgame (конец игры), Probe (ход) и Result (счет).

Первые два сигналаиспользуются для начала и окончание игры. Одновременно может вестисьтолько одна игра, т.е. сигналы Newgame игнорируются в течение игры, асигналы Endgame игнорируются, если игра не началась.Сама игра очень простая. Состояние системы время от временименяется от выигрышного к проигрышному и обратно. Игрок долженугадать, в какой момент состояние выигрышное. Если игрок делает ход(посылает сигнал Probe) в тот момент, когда состояние системывыигрышное, он получает одно очко. Если игрок делает ход в момент, когдасостояние системы проигрышное, он теряет одно очко. Игрок может узнатьтекущий счет, послав сигнал Result.7.2.

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