Мансуров Н. Н., Майлингова О. Л. - Методы формальной спецификации программ - языки MSC и SDL, страница 7
Описание файла
PDF-файл из архива "Мансуров Н. Н., Майлингова О. Л. - Методы формальной спецификации программ - языки MSC и SDL", который расположен в категории "". Всё это находится в предмете "формальная спецификация и верификация программ" из 9 семестр (1 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 7 страницы из PDF
Время между установкой и срабатыванием таймера не меньшедлительности интервала времени, указанной в символе установки таймера.2. В случае сброса таймера, время между установкой и сбросом меньшедлительности интервала времени, указанной в символе установки таймера.3. Семантика длительности интервала не определяется в языке диаграммвзаимодействия.4.2.6. Область неупорядоченных событийОбласть неупорядоченных событий служит для описаниянедетерминированных событий. Например, эта конструкция может бытьиспользована для описания приема двух или более сообщений впроизвольном порядке.
В языке диаграмм взаимодействия существуютограничения на события, которые могут происходить внутри областинеупорядоченных событий: могут быть только области неупорядоченногоприема сообщений и области неупорядоченной посылки сообщений.31Графический синтаксис:<concurrent area> ::= <coregion start symbol>is followed by {<concurrent out area>|<concurrent in area>}is followed by <coregion end symbol><coregion start symbol> ::=<coregion out area> ::= { <message out area>is followed by <coregion symbol> }+<coregion in area> ::= { <message in area>is followed by <coregion symbol> }+<coregion symbol> ::=<coregion end symbol> ::=Семантика:События внутри области неупорядоченных событий не связаны между собойотношением порядка.4.3.
Семантика диаграмм взаимодействияВ диаграммах взаимодействия не подразумевается наличие глобальнойоси времени. Считается, что на оси каждого объекта время движется сверхувниз. Предположений о наличии шкалы времени для каждого объекта такженет. События на оси объекта полностью упорядочены (за исключениемслучая специальной конструкции - неупорядоченной области). Событияразличных объектов упорядочены только за счет обменов сообщениями:сообщение должно быть послано раньше, чем принято. Больше никакихпредположений об упорядоченности событий не делается.Таким образом, диаграмма взаимодействия задает отношениечастичной упорядоченности на множестве сообщений всей системы (всехобъектов, присутствующих на диаграмме, и соответствующего окружения).Отношение частичной упорядоченности - транзитивное, антисимметричное,рефлексивное бинарное отношение.Каждая диаграмма взаимодействия задает обычно множестводопустимых последовательностей событий.
По определению, допустимойпоследовательностью событий является линейная последовательностьпроекций событий на глобальную ось времени (с определенной шкалой).Заметим, что допустимая последовательность событий также может бытьописана при помощи диаграммы взаимодействия (с усиленной семантикой,предполагающей наличие глобальной оси времени с определенной шкалой).32Рассмотрим пример диаграммы взаимодействия с именем ordering,описывающей систему из трех объекта с именами a, b и c.
Типы объектов надиаграмме не указаны.Объект a принимает сообщение с именем m1 из окружения системы;затем посылает сообщение с именем m2 объекту b; затем посылаетсообщение с именем m3 объекту c; затем принимает сообщение с именем m4от объекта b.Объект b принимает сообщение с именем m2 от объекта a; затемпосылает сообщение m4 объекту a.Объект с принимает сообщение m3 от объекта a. Это единственноесобытие объекта с именем c на данной диаграмме.Ниже приводится графическое представление диаграммы ordering:MSC orderingabcm1m2m3m4Рис. 2. Диаграмма взаимодействия orderingРассмотрим текстовое представление диаграммы ordering:MSC ordering;INST a, b, c;INSTANCE a;IN m1 FROM ENV;OUT m2 TO b;OUT m3 TO c;*IN m4 FROM b;ENDINSTANCE;33INSTANCE b;IN m2 FROM a;OUT m4 TO a;ENDINSTANCE;INSTANCE c;IN m3 FROM a;ENDINSTANCE;ENDMSC;Обозначим событие приема сообщения m через in(m), а событие посылкисообщения m через out (m).Множество событий системы на диаграмме ordering:E={in(m1),out(m2),in(m2),out(m3),in(m3),out(m4),in(m4)}Взаимодействия (обмены сообщениями), описанные наordering, задают следующие частичные отношения порядка насобытий E:in(m2) < out(m2)in(m3) < out(m3)in(m4) < out(m4)Трасса объекта A задает следующее отношение порядка насобытий E: out(m1) < out(m2) < out(m3) < in(m4)Трасса объекта B задает следующее отношение порядка насобытий E: in(m2) < out(m4)диаграммемножествемножествемножествеСоответствующее отношение частичного порядка на множестве E можноописать, задав граф предшествования (компактная форма представлениятранзитивного замыкания отношения порядка на множестве E):in(m1)out(m2)out(m3)in(m4)in(m2)in(m3)out(m4)34Заметим, что любая диаграмма взаимодействия допускает наличиедополнительных наблюдаемых событий между событиями, описанными надиаграмме (в том, числе, наличие дополнительных взаимодействий междуобъектами).4.4.
Структурные средстваОсновным структурным средством языка диаграмм взаимодействияявляется композиция и декомпозиция посредством состояний. Композициядиаграмм посредством состояний позволяет описывать сложное множестводопустимых трасс по частям (т.н. горизонтальная композиция).Дополнительным структурным средством является иерархическаядекомпозиция объекта (т.н. вертикальная декомпозиция).4.4.1. СостоянияСостояния предназначены для того, чтобы объединять несколькодиаграмм для описания сложного поведения множества объектов.
Состояние- это особое событие на трассе объекта. В отличие от прочих событий, одно ито же состояние может разделяться одним, двумя и более объектами. Почислу объектов на диаграмме, разделяющих некоторое состояние, различаютглобальные состояния (общее для всех объектов), разделяемые состояния(разделяемые несколькими, но не всеми объектами) и локальные состояния(разделяемое единственным объектом).Состояние называется начальным (для объекта на диаграмме), еслиданное состояние предшествует всем остальным событиям на трассе данногообъекта.
Состояние называется завершающим (для объекта на даннойдиаграмме), если на диаграмме нет событий, которым данное состояниепредшествует. Остальные состояния называются промежуточными (дляобъекта на данной диаграмме).Наибольший интерес для композиции представляют глобальныесостояния. Глобальное состояние называется начальным (на некоторойдиаграмме), если оно является начальным для всех объектов на даннойдиаграмме.
Глобальное состояние называется завершающим (на диаграмме),если оно является завершающим для всех объектов на диаграмме. Остальныеглобальные состояния называются промежуточными глобальнымисостояниями.35Графический синтаксис:<condition area> ::= <local condition area><shared condition area><local condition area> ::= <condition symbol>contains <condition name><condition symbol> ::=<shared condition area> ::= <condition start area>|<condition intermediate area>|<condition end area><condition start area> ::= <condition start symbol>is associated with <condition name>is connected to {<condition intermediate area>| <condition end area> }<condition start symbol> ::=<condition intermediate area>::= <condition intermediate symbol>is connected to {<condition intermediate area>| <condition end area> }<condition intermediate symbol> ::=<condition intermediate symbol1>|<condition intermediate symbol2><condition intermediate symbol1> ::=<condition intermediate symbol2> ::=<condition end area> ::= <condition end symbol><condition end symbol> ::=<condition name> ::= <name>36Дополнительные правила построения диаграмм:Состояния и сообщения:Если два объекта разделяют одно и то же состояние, то сопряженныесобытия приема и посылки сообщений должны происходить либо оба досоответствующего состояния, либо оба после соответствующего состояния(т.е.
символы передачи сообщений не должны пересекать символысостояний).Семантика:1. Состояние является событием для объекта.2. Разделяемые состояния не определяют отношения порядка междусобытиями различных объектов.3. Состояния определяют возможные композиции и декомпозиции диаграммвзаимодействия.4. Семантика диаграммы с состояниями полностью эквивалентна семантикеданной диаграммы с удаленными состояниями.4.4.2.
Декомпозиция диаграммОпределим секцию,как такую диаграмму, у которой имеютсяначальное и завершающее глобальные состояния и не имеетсяпромежуточных состояний. Глобальные состояния разбивают диаграмму насекции (т.е. участки трассы между глобальными состояниями).В общем случае, декомпозиция диаграмм посредством состоянийопределяется следующим образом. Пусть некоторая диаграмма (MSC)содержит промежуточные состояния Si. Тогда MSC может быть разбита надве диаграммы (MSC1 и MSC2) таким образом, что состояния Si становятсязавершающими на MSC1 и начальными на MSC2.4.4.3. Композиция секцийПравило композиции для секций определяется следующим образом.Пусть имеется две секции, причем множества объектов у них совпадают.Тогда, если на первой секции имеется завершающее глобальное состояние снекоторым именем, а на второй секции- начальное состояния с тем жеименем, то вторая секция может служить продолжением первой.Операцию продолжения секции можно уточнить следующим образом:для каждого объекта на новой диаграмме последовательность событий будетсостоять из всех событий, описанных на первой диаграмме (в той же37последовательности); затем всех событий, описанных на второй диаграмме (втой же последовательности).Заметим, что вместе две диаграммы, одна из которых может бытьпродолжением другой, описывают новое поведение соответствующегомножества объектов.В общем случае, правило композиции диаграмм посредствомсостояний формулируется следующим образом.
Пусть две диаграммыописывают некоторое общее множество объектов I (дополнительно, каждаядиаграмма может описывать объекты, отсутствующие на другой диаграмме).Тогда, одна диаграмма (MSC1) может служить продолжением другойдиаграммы (MSC2), если на MSC1 объекты из множества I оканчиваетсясостояниями с именами Si, и объекты из множества I на MSC2 начинаются ссоответствующих состояний. При этом некоторые (или даже все) состоянияSi могут быть разделяемыми.Трассы объектов, не входящие во множество I (на MSC1 и MSC2),добавляются к объединенной диаграмме. Очевидно, что множествовзаимодействий между объектами из MSC1 и MSC2 должно быть пусто дляобъектов, не входящих в общее множество I.Ситуация, когда объект на MSC1 посылает сообщение в окружение, аэто сообщение на самом деле предназначается одному из объектов на MSC2(т.н.
композиция посредством окружения) не выразима средствами языкадиаграмм взаимодействия.4.4.4. Виды композиции диаграммРассмотрим основные способы организации набора диаграмм в целяхописания сложного поведения множества объектов.Последовательная композицияПо определению, последовательной композицией называется такаяорганизация набора диаграмм, при которой каждая диаграмма набора (кромепервой) является продолжением некоторой другой (т.е. начальные состоянияодной диаграммы совпадают с завершающими состояниями другойдиаграммы).Последовательная композицияописывает сложное поведение,состоящее из нескольких последовательных этапов. Заметим, что поведение,описываемое последовательной композицией нескольких диаграмм можно,вообще говоря, описать единственной диаграммой без состояний.38Альтернативная композицияПо определению, альтернативной композицией называется такаяорганизация набора диаграмм, когда все диаграммы набора (кроме первой)имеют одинаковые начальные состояния, совпадающие с завершающимисостояниями первой диаграммы.Альтернативная композиция описывает сложное поведение, состоящееих взаимоисключающих последовательностей событий.