Мансуров Н. Н., Майлингова О. Л. - Методы формальной спецификации программ - языки MSC и SDL, страница 10
Описание файла
PDF-файл из архива "Мансуров Н. Н., Майлингова О. Л. - Методы формальной спецификации программ - языки MSC и SDL", который расположен в категории "". Всё это находится в предмете "формальная спецификация и верификация программ" из 9 семестр (1 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 10 страницы из PDF
<maximum number> задает максимальное число одновременносуществующих экземпляров данного процесса.Конструкция <valid input signal set> позволяет явно специфицировать множестводопустимых сигналов процесса (интерфейс процесса). Если эта конструкция незадана явно, интерфейс процесса вычисляется как множество всех входных55сигналов, указанных во всех межпроцессных каналов, присоединенных к данномупроцессу на соответствующей диаграмме блока.6.3.4. ПроцедураПроцедура позволяет объединять набор состояний и переходов в единоецелое и вводит некоторое имя для последующей работы с этим набором.Графический синтаксис:<procedure diagram> ::= <frame symbol>contains { <procedure heading>{ <procedure text area>| <procedure area> }*<procedure graph area> }<procedure area> ::= <graphical procedure reference><procedure text area> ::= <text symbol> contains{ <variable definition>| <data definition> }*<graphical procedure reference> ::=<procedure symbol> contains{ <procedure preamble> <procedure name> }<procedure symbol> ::=<procedure heading> ::= procedure <name>[<procedure formal parameters>][<procedure result>]<procedure graph area> ::= [<procedure start area>]{ <state area> | <in-connector area> }*<procedure start area> ::= <procedure start symbol>is followed by <transition area><procedure start symbol> ::=<procedure formal parameters> ::= fpar<formal variable parameter>{ , <formal variable parameter> }*<formal variable parameter> ::=<parameter kind> <parameter of sort><parameter kind> ::=[ in/out | in ]<procedure result> ::= returns <variable name>6.4.
Взаимодействие56<sort>Рис. 13. Посылка сигнала между двумя процессамиВ языке SDL нет глобальных данных. Передача информации междупроцессами или между процессами и окружением системы осуществляется черезпосылку сигналов (возможно с параметрами). Сигналы передаются от одногопроцесса (процесса-отправителя) во входной порт другого процесса (процессаполучателя).
Процесс-отправитель и процесс-получатель могут совпадать. Посылкасигнала является асинхронной, т.е. процесс-отправитель продолжает работу, неожидая подтверждения о получении сигнала процессом-получателем. Сигналыпередаются по статически определенной сети межблочных и межпроцессныхканалов, связанных соединениями. Заметим, что в каждом соединении могутучаствовать по несколько каналов как с внешней, так и с внутренней стороны.6.4.1. Сигнал57Графический синтаксис:<signal definition> ::= signal <name> [<sort list>]<sort list> ::= ( <sort> { , <sort> }* )6.4.2.
Список сигналовСписок сигналов позволяет объединять несколько сигналов в единую группу ииспользовать имя этой группы в определениях каналов и т.д.Графический синтаксис:<signal list area> ::= <signal list symbol>contains <signal list><signal list symbol> ::=<signal list definition> ::= signallist <name> = <signal list> ;<signal list> ::= <signal list item> { , <signal list item> }*<signal list item> ::= { <signal name>| ( <signal list name> )| <timer name><signal name> ::= name<signal list name> ::= name<timer name> ::= <name>6.4.3. КаналКанал описывает маршрут передачи сигналов между двумя блоками или медублоком и его окружением. Каналы могут быть однонаправленные илидвунаправленные.
С каждым направлением может быть связан свой списокдопустимых сигналов.Графический синтаксис:<channel definition area> ::= <channel symbol>is associated with { <channel name><signal list area>[ <signal list area> ] }is connected to { <block area>{ <block area> | <frame symbol> }<channel symbol> ::=<channel symbol 1>| <channel symbol 2>| <channel symbol 3>58<channel symbol 1> ::=<channel symbol 2> ::=<channel symbol 3> ::=6.4.4.
Межпроцессный каналГрафический синтаксис:<signal route definition area> ::= <signal route symbol>is associated with <name>{ <signal list area> [ <signal list area>] }is connected to { <process area>{<process area | <frame symbol> }<signal route symbol> ::= <signal route symbol 1>| <signal route symbol 2><signal route symbol 1> ::=<signal route symbol 2> ::=6.5.
Поведение6.5.1. Определение переменныхКаждый процесс (и процедура) могут статически определять локальныепеременные. Дополнительно, процесс (и процедура) могут иметь формальныепараметры. Все переменные создаются при порождении экземплярапроцесса (вызове процедуры) и уничтожаются при остановке процесса(возврате из процедуры).Графический синтаксис:<variable definition> ::= dcl <name> <sort>[:= <expression>] ;Примечание:При определении переменной можно указать выражение для инициализациипеременной при создании.6.5.2. Стартовый символ59Стартовый символ определяет стартовый переход процесса, т.е.последовательность действий, выполняемую при порождении экземпляра данногопроцесса (статически или динамически).Графический синтаксис:<start area> ::= <start symbol>is followed by <transition area><start symbol> ::=6.5.3. СостояниеСостояние определяет набор реакций на сигналы (переходы).
Каждоесостояние имеет имя. Состояние с именем «*» является особым: это способопределить переходы, общие для всех обычных состояний.<state area> ::=<state symbol> contains <state name> is associated with{ <input association area>| <save association area> } *<state name> ::=<asterisk> ::= *<name> | <asterisk><state symbol> ::=<input association area> ::= <solid association symbol>is connected to<input area><save association area> ::= <solid association symbol>is connected to<save area>6.5.4.
Прием сигналаСимвол приема сигнала определяет реакцию на данный сигнал (вданном состоянии). Непосредственно при получении сигнала переменные,указанные в символе приема сигнала, получают значения параметровсигнала.60Графический синтаксис:<input area> ::= <input symbol> contains { <stimulus> }is followed by <transition area><stimulus> ::= { <signal name> | <timer name> }[ ( <variable> { , <variable> }* ) ]<input symbol> ::=6.5.5. Сохранение сигналаСигналы, указанные в символе сохранения сигнала в некоторомсостоянии, игнорируются процессом в данном состоянии.
Эти сигналыостаются во входном порте процесса (в порядке поступления) дляпоследующей обработки в другом состоянии. Наличие механизма сохранениясигналов является важным, потому что в каждом состоянии определенастандартная реакция на любой сигнал, которая состоит в том, что сигнализымается из очереди и уничтожается, тогда как процесс остается в старомсостоянии.Графический синтаксис:<save area> ::= <save symbol> { contains <save list> }<save list> ::= { <signal list> | <asterisk> }<save symbol> ::=616.5.6. МеткиМетки позволяют определять участки переходов, общие для несколькихсостояний.Графический синтаксис:<in-connector area> ::= <in-connector symbol>contains <connector name>is followed by <transition area><connector name> ::= <name><in-connector symbol> ::=6.5.7.
ПереходПереход определяет последовательность действий, выполняемую процессом вкачестве реакции на получение некоторого сигнала в некотором состоянии. Вовремя выполнения перехода процесс может осуществлять доступ к переменным,посылать сигналы, а также порождать экземпляры процессов.
Переходзаканчивается либо тем, что процесс попадает в новое состояние и ожидает тамследующего сигнала, либо остановкой процесса (возврат в случае процедуры), либопередачей управления на другой переход.Графический синтаксис:<transition area> ::= [<transition string area>] is followed by{ <state area>| <nextstate area>| <decision area>| <stop symbol>| <merge area>| <out-connector area>| <return area> }<transition string area> ::={ <task area>| <output area>| <set area>| <reset area>| <create request area>| <procedure call area> }[ is followed by <transition string area> ]626.5.8.