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

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

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

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

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Альтернативная композицияПо определению, альтернативной композицией называется такаяорганизация набора диаграмм, когда все диаграммы набора (кроме первой)имеют одинаковые начальные состояния, совпадающие с завершающимисостояниями первой диаграммы.Альтернативная композиция описывает сложное поведение, состоящееих взаимоисключающих последовательностей событий.

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