Инсерционная семантика параллельных процедурных конструктов языка UCM

Предложено математическое описание семантики процедурного конструкта Stub в языке параллельного моделирования UCM с применением инсерционного подхода, основанного на взаимодействии сред и погруженных в них агентов....

Ausführliche Beschreibung

Gespeichert in:

Bibliographische Detailangaben
Datum:	2012
1. Verfasser:	Годлевский, А.Б.
Format:	Artikel
Sprache:	Russian
Veröffentlicht:	Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України 2012
Schriftenreihe:	Управляющие системы и машины
Schlagworte:	Семантика формальных и естественных языков
Online Zugang:	http://dspace.nbuv.gov.ua/handle/123456789/83104
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!
Назва журналу:	Digital Library of Periodicals of National Academy of Sciences of Ukraine
Zitieren:	Инсерционная семантика параллельных процедурных конструктов языка UCM / А.Б. Годлевский // Управляющие системы и машины. — 2012. — № 6. — С. 22-34. — Бібліогр.: 14 назв. — рос.

Institution

Digital Library of Periodicals of National Academy of Sciences of Ukraine

id	irk-123456789-83104
record_format	dspace
spelling	irk-123456789-831042015-06-15T03:01:55Z Инсерционная семантика параллельных процедурных конструктов языка UCM Годлевский, А.Б. Семантика формальных и естественных языков Предложено математическое описание семантики процедурного конструкта Stub в языке параллельного моделирования UCM с применением инсерционного подхода, основанного на взаимодействии сред и погруженных в них агентов. The mathematical description of the semantics of a procedural construct Stub for the parallel modeling language UCM is suggested. This description used the insertion approach that is based on the interaction of environments and agents inserted in them. Запропоновано математичний опис семантики процедурного конструкту Stub у мові паралельного моделювання UCM із застосуванням інсерційного підходу, основаного на взаємодії середовищ та занурених у них агентів. 2012 Article Инсерционная семантика параллельных процедурных конструктов языка UCM / А.Б. Годлевский // Управляющие системы и машины. — 2012. — № 6. — С. 22-34. — Бібліогр.: 14 назв. — рос. 0130-5395 http://dspace.nbuv.gov.ua/handle/123456789/83104 519.7 + 004.436.4 ru Управляющие системы и машины Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України
institution	Digital Library of Periodicals of National Academy of Sciences of Ukraine
collection	DSpace DC
language	Russian
topic	Семантика формальных и естественных языков Семантика формальных и естественных языков
spellingShingle	Семантика формальных и естественных языков Семантика формальных и естественных языков Годлевский, А.Б. Инсерционная семантика параллельных процедурных конструктов языка UCM Управляющие системы и машины
description	Предложено математическое описание семантики процедурного конструкта Stub в языке параллельного моделирования UCM с применением инсерционного подхода, основанного на взаимодействии сред и погруженных в них агентов.
format	Article
author	Годлевский, А.Б.
author_facet	Годлевский, А.Б.
author_sort	Годлевский, А.Б.
title	Инсерционная семантика параллельных процедурных конструктов языка UCM
title_short	Инсерционная семантика параллельных процедурных конструктов языка UCM
title_full	Инсерционная семантика параллельных процедурных конструктов языка UCM
title_fullStr	Инсерционная семантика параллельных процедурных конструктов языка UCM
title_full_unstemmed	Инсерционная семантика параллельных процедурных конструктов языка UCM
title_sort	инсерционная семантика параллельных процедурных конструктов языка ucm
publisher	Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України
publishDate	2012
topic_facet	Семантика формальных и естественных языков
url	http://dspace.nbuv.gov.ua/handle/123456789/83104
citation_txt	Инсерционная семантика параллельных процедурных конструктов языка UCM / А.Б. Годлевский // Управляющие системы и машины. — 2012. — № 6. — С. 22-34. — Бібліогр.: 14 назв. — рос.
series	Управляющие системы и машины
work_keys_str_mv	AT godlevskijab insercionnaâsemantikaparallelʹnyhprocedurnyhkonstruktovâzykaucm
first_indexed	2025-07-06T09:50:20Z
last_indexed	2025-07-06T09:50:20Z
_version_	1836890635083186176
fulltext	22 УСиМ, 2012, № 6 УДК 519.7 + 004.436.4 А.Б. Годлевский Инсерционная семантика параллельных процедурных конструктов языка UCM Предложено математическое описание семантики процедурного конструкта Stub в языке параллельного моделирования UCM с применением инсерционного подхода, основанного на взаимодействии сред и погруженных в них агентов. The mathematical description of the semantics of a procedural construct Stub for the parallel modeling language UCM is suggested. This description used the insertion approach that is based on the interaction of environments and agents inserted in them. Запропоновано математичний опис семантики процедурного конструкту Stub у мові паралельного моделювання UCM із засто- суванням інсерційного підходу, основаного на взаємодії середовищ та занурених у них агентів. 1. Введение. Параллельные вычисления и язы- ки параллельного программирования, по-види- мому, – одно из тех направлений в развитии программирования, которое может служить от- ветом на бурное развитие электронной инже- нерии. Особенно актуально развитие высоко- уровневых языков и языков, приближенных к инженерным разработкам. В частности, в по- следние десятилетия получили развитие языки с графическим представлением, позволяющие в удобных для инженеров формах проводить разработку многокомпонентных программных систем. Их представителями могут служить язы- ки MSC [1], SDL [2], UML [3], UCM [4] и др. В настоящей статье1 рассмотрена семанти- ка исполнения процедурного конструкта стаб (stub) в языке UCM. Описание семантики вы- полнено в рамках инсерционного подхода [5] к вычислениям в многокомпонентных средах. Суть инсерционной модели состоит в том, что поведение отдельных компонент (агентов) опи- сывается на уровне алгебры поведений [6, 7], а их взаимодействие использует функцию по- гружения. Посредством этой функции задается взаимодействие агентов и сред, соответствую- щих разным уровням представления проекти- руемых систем. Средства, используемые в ин- серционном моделировании, позволяют выра- зить все те особенности модели вычислений, что была предложена для языка UCM [4] и в работах [8–12] основных разработчиков этого Ключевые слова: язык UCM, инсерционное програм- мирование. 1 Работа выполнена при поддержке ДФФД по проекту Ф40.1/004. языка. Отличием настоящего описания семан- тики UCM есть использование математического подхода к описанию процессов вызова проце- дур, специфицируемых ими вычислений и про- цессов завершения процедур. Автор статьи в значительной степени при- держивается терминологии, принятой в языке UCM, включая использование оригинальных терминов. Отчасти это сделано для того, чтобы подчеркнуть связь с этим языком, а отчасти потому, что адекватная терминология в рус- ском языке отсутствует. Ключевые понятия, используемые здесь – карта как поведенческий сценарий и стаб как конструкт для вызова про- цедуры. Стаб (конструкт класса Stub) ссылается на совокупность вложенных карт (plug-in map или плагинов), перечисленных в описании стаба (структуры PluginBinding). Коммутация стар- товых и конечных вершин путей вложенных карт с входными и выходными путями стаба задается специальными структурами InBinding и OutBinding. Более детально семантика будет представлена далее – как иллюстративно на примерах, так и в виде атрибутной транзици- онной системы, описанной в рамках инсерци- онного подхода. Отметим, что для понимания языка UCM удобна модель сетей Петри [13], процессы в которых представляются как движение фишек вдоль путей в сетях. Существенное отличие от обычных сетей Петри состоит в том, что про- цессы в языке UCM развиваются над некото- рой памятью, используемой как при вычисле- нии условий (конструктов класса Condition), так и при выполнении действий (конструктов УСиМ, 2012, № 6 23 класса Responsibility). Вычисляемые условия используется внутри некоторых конструктов в качестве барьеров, разрешающих или запре- щающих дальнейшее продвижением фишек. Язык UCM наряду с текстовым обладает так- же развитым графическим представлением. На приведенных рисунках, а также в табл. 2, где специфицируются разные случаи поведения ста- бов, используются некоторые элементы этой графики, например, пути, их стартовые и конеч- ные вершины, стабы и др. Здесь не приведены все графические элементы и пояснения к ним, однако отметим, что помимо стандарта языка UCM [4], где все они детально описаны, в этом тематическом выпуске содержится работа [14], где представлены конструкты UCM плоского (не иерархического) уровня. Здесь же добавлен лишь конструкт стаб. Статья состоит из восьми разделов, включая введение и заключение. Во втором разделе крат- ко описана инсерционная модель, в третьем и четвертом разделах даны содержательная ха- рактеристика стабов и присущие им паралле- лизмы, в пятом описываются виды стабов. В шестом и седьмом разделах приведены семан- тика стабов в рамках инсерционной модели и уравнения, реализующие их поведение. 2. Инсерционная модель Математическую семантику стабов опишем в рамках инсерционной модели, предложенной А.А. Летичевским [5]. Модель состоит из опи- сания среды и агентов; описания функции по- гружения, посредством которой изменяется со- стояние среды и погруженных в нее агентов. В общем случае среда, описывающая конкрет- ный UCM-проект, – многоуровневая и включа- ет в себя (глобальную) среду верхнего уровня E и вложенные в нее среды карт M, визитов V и компонент C, рассматриваемых как агенты, а также процессы P как агенты самого низкого уровня. Уровень компонент может отсутство- вать. Все указанные среды задаются посредст- вом описания их свойств и атрибутов. Атрибу- ты самой внешней среды E будем называть глобальными, все прочие свойства и атрибуты локализуются на уровнях соответствующих вложенных сред. Доступ к атрибуту N, кото- рый относится к локальной среде M, задается в виде M1.M2. … .M.N, где префикс M1.M2. … от- ражает вложенность локальных сред для карт, объемлющих данную карту М. В дальнейшем, если из контекста понятно, к какой среде отно- сится атрибут, префикс перед ним для кратко- сти будем опускать. Другая классификация атрибутов, отличная от их локализации по уровням, заключается в их разделении на два непересекающихся клас- са: пользовательские и управляющие. Пользо- вательские атрибуты соответствуют перемен- ным проекта UCM, введенным его разработчи- ком. Они используются в условиях и в дейст- виях, где вычисляются их значения. Управля- ющие атрибуты создаются с целью обеспечить синхронизацию процессов, соответствующую определяемой семантике. Это происходит на этапе построения модели проекта UCM – тран- сляции проекта в систему сред и агентов. Любой процесс есть либо действием, либо композицией более простых процессов, обра- зованных посредством применения операций префиксинг (точка, отделяющая действие от хвоста процесса) и недетерминированный вы- бор (представляется символом +, который от- личается от обычного знака сложения тем, что его операнды относятся к алгебре поведений). Помимо этих операций алгебра поведений обо- гащена операцией параллельной композиции () \|\| () с семантикой интерливинга. Начальное состояние среды – это параллельная компози- ция E[M1[u1], M2[u2], …] стартовых точек (кон- структов класса StartPoint), рассматриваемых как начальные состояния агентов, погружен- ных в среды карт и, возможно, компонент (ес- ли они к ним привязаны), а также множество начальных значений атрибутов. Переходы в системе определяются уравнениями вида: S = a.S1, S = S1 + S2, S = S1 \|\| S2, в которых S – это текущее поведение агента, S1 и S2 – выражения в алгебре поведений. В каче- стве S рассматривается вершина пути и ассо- циированный с ней конструкт языка UCM. Пер- вое уравнение описывает переход агента от S к поведению S1 после выполнения действий, за- даваемых префиксом a. Выражение S1 в пер- 24 УСиМ, 2012, № 6 вом уравнении может отсутствовать, и тогда такой переход интерпретируется как успешное завершение агента и удаление его из среды, т.е. из числа погруженных в нее агентов. Вто- рое уравнение задает альтернативный переход агента к одному из поведений S1 или S2. В третьем случае S поведение агента заменяется поведениями S1 и S2 уже двух агентов, погру- женных в среду. Если использовать термино- логию сетей Петри, то уравнение S = a.S1 мож- но интерпретировать как переход фишки из начала пути S, представленного вершиной а, к началу пути S1; уравнение S = S1 + S2 – как продвижение фишки через точку ветвления к началу одной из ветвей; и уравнение S = S1 \|\| S2 – как раздвоение фишки и переход ее копий к началам обоих путей S1 и S2. Функция погружения (insertion function) за- дается совокупностью правил, описывающих различные случаи взаимодействия между аген- тами и средами. Поскольку определяемые здесь правила используют фиксированный набор кон- кретных управляющих атрибутов системы, ма- тематическое описание этих правил будет сле- довать после описания системы атрибутов. В [14] описаны правила apply (выполнение дей- ствий над атрибутами), check (проверка вы- полнимости условий), insert (погружение но- вого агента в среду). При описании семантики стабов будут определены правила insertvisit (образование среды визита), movein (переход процесса во вложенную карту) и moveout (вы- ход процесса из вложенной карты в карту верхнего уровня). 3. Содержательная характеристика стабов Описание стаба содержит одну или несколь- ко структур PluginBinding, каждая из которых связывает этот стаб в точности с одной картой. Такая структура специфицирует коммутации входных и выходных путей стаба со стартовыми и конечными вершинами путей в соответст- вующей иерархически подчиненной карте. Коммутация заданной карты М и стаба St зада- ется структурами двух видов, InBinding и OutBinding, которые будем называть также вход- ными и выходными привязками стаба к вложен- ным картам. Каждая InBinding (соответственно, OutBinding) структура описывает соединение од- ного из входных (выходных) путей этого стаба с одной из стартовых (конечных) вершин пу- тей карты М. Входные (выходные) пути стаба представлены вершинами, непосредственно пред- шествующими стабу (следующими за ним). Итак, InBinding структура стаба – это пара (in, sp), где in – входной путь этого стаба, sp – стартовая вершина пути карты. Для стаба St и карты М все пары вида (in, sp) различаются между собой, задавая частичное взаимно одно- значное соответствие между входными путями стаба St и стартовыми вершинами вложенной карты M. Аналогично, OutBinding структура – это пара (ep, out), где ep – конечная вершина пути карты, out – выходной путь стаба. На рис. 1 в левой его части изображена струк- тура стаба St с двумя входными путями от вер- шин S1 и S2, непосредственно предшествую- щими стабу, двумя выходными путями к вер- шинам Т1 и Т2, непосредственно следующими за стабом, карта M с двумя стартовыми и тремя конечными вершинами. Слева и справа от кар- ты изображены структуры стаба IB (InBinding), OB (OutBinding), обеспечивающие соединение входных и выходных путей стаба St со старто- выми и конечными вершинами путей вложен- ной карты. Понятно, что данных, содержащих- ся в структурах IB и OB, достаточно для вос- становления путей от S1 и S2 к стартовым вер- шинам путей карты М и от конечных вершин ее путей к вершинам Т1 и Т2. Эти пути, обозна- ченные пунктирными линиями, используют данные структур IB и OB. OB1 OB2 IB2 IB1 T2 S2 T1 S1 М St Рис. 1. Схема структуры и динамики стаба с одной вложенной картой В правой части этого рисунка изображено, каким образом в карту верхнего уровня будет вложена карта М – плагин для стаба St и как в УСиМ, 2012, № 6 25 результате будут развиваться процессы, специ- фицированные стабом. Прямоугольник, в ко- торый заключена карта М, рассматривается как промежуточный уровень между исходной кар- той со стабом St и картой М. Переход фишки внутрь этого прямоугольника трактуется как ви- зит во вложенную карту. Среду этой карты будем называть средой визита. Ее особенность в том, что в ней будут определяться дополни- тельные управляющие атрибуты, используемые для поддержки семантики стабов. Ромбовидная фигура стаба исключена из рисунка, чем акцен- тируется, что вершина стаба важна на этапе организации дополнительных путей, соединяю- щих карту верхнего и вложенного уровней, но не существенна на этапе, когда реализуется спе- цифицированное стабом поведение. Представленный на рисунке простейший слу- чай стаба с одной вложенной картой позволяет увидеть некоторые аналогии между описанием и вызовом процедур в последовательных язы- ках программирования с одной стороны, и опи- санием и функционированием стабов в языке UCM, с другой. При таком сходстве, представ- ленном в табл. 1, отметим, что стабы отлича- ются значительно более гибкой семантикой, по- зволяющей синхронизировать процессы, проте- кающие как вне вершины стаба, так и внутри локальной среды, инициированной процессами, приходящими на входы стаба. Пояснения к этой таблице и перечисленным в ней понятиям се- мантики языка UCM будут следовать из даль- нейшего изложения, тогда как сама таблица при- ведена для того, чтобы наметить аналогии с известными моделями и отличия от них. Возвращаясь к рис. 1, отметим, что в общем случае у стаба может быть несколько вложен- ных карт. Рассмотрим еще одну иллюстрацию (рис. 2) к описываемой семантике стабов. Пред- полагается, что здесь стаб ссылается на две разные вложенные карты, и на каждую из них – со своей схемой коммутации. Графиче- ская картинка теперь отличается тем, что входы и выходы стаба могут соединяться пунктирными линиями с несколькими стар- товыми и соответственно конечными верши- нами вложенных карт. Таблица 1. Сопоставление понятий процедуры и стаба Последовательные языки UCM Определение процедуры Вложенная карта (Plug-in map) Вызов процедуры Стаб Выполнение вызова процедуры Переход от стаба к его вложенной карте Формальные параметры процедуры Стартовые и конечные вершины путей вложен- ной карты Фактические параметры процедуры Входные и выходные пути стаба Синхронная передача фактических параметров Асинхронная передача фактических параметров Порядок параметров или именован- ные параметры Структуры InBinding и OutBinding Входные параметры InBinding Выходные параметры OutBinding Вызов процедуры по ссылке (и ди- намическое связывание в объектных языках) Аналог PluginBinding С1 th1 th2 С2 Рис. 2. Схема стаба с двумя вложенными картами Промежуточная среда визита содержит все вложенные карты стаба, в данном случае – две. На рисунке опущены имена этих карт, но до- бавлены обозначения C1, C2 и th1, th2. Первые два – это условия, которые задает автор проек- та UCM и которые называются предусловиями структур InBinding. Смысл предусловий в том, что управление с входа стаба может быть пере- дано на стартовые вершины путей вложенной карты, но только если предусловие истинно. За- метим, что стартовые вершины также могут иметь условия, определяющие старт процессов, но это уже другие условия, связанные не с вло- женностью карты, а с ней самой. Выражения th1 и th2, значениями которых могут быть це- лые положительные числа, называются поро- 26 УСиМ, 2012, № 6 гами (threshold) выходных путей стаба2, кото- рые будут рассмотрены далее. Смысл порогов в том, что фишки могут перейти за пределы стаба только после того, как к пути, отмечен- ному пороговым выражением, придет столько фишек, какова величина порога. При этом все последующие фишки, приходящие в рамках дан- ного визита к этому пути, будут игнорировать- ся. Отметим, что даже если выходной путь стаба, отмеченный пороговым выражением, свя- зан только с одной конечной вершиной пути в одной карте, значение этого выражения может быть больше единицы, поскольку одна вложен- ная карта может сгенерировать несколько фи- шек. Если условия привязки не указаны, то по умолчанию это трактуется так, как если они равны true. Если не указаны пороговые значе- ния выходов стаба, то по умолчанию они при- равниваются к числу выходных привязок стаба к этому выходу. Карты UCM могут обладать свойством sin- gleton, фиксирующим, что число их возмож- ных экземпляров равно единице. Это свойство, если оно истинно для данной карты, позволяет синхронизировать процессы в разных стабах, обращающихся к общей вложенной карте. На рис. 3 изображены два стаба, у которых общая вложенная карта. В этом примере про- цессы внутри карты синхронизируются посред- ством конструкта AndJoin и могут продолжиться Рис. 3. Использование singleton карты только по достижении обеими такой вершины. Если бы этой вложенной карте не было присуще свойство singleton, то процессы каждого стаба продолжались бы в своей копии карты, не 2 Только для стабов синхронизирующего и блокирую- щего видов. смогли бы синхронизироваться и пройти вер- шину AndJoin. 4. Параллелизмы, реализуемые в стабах Язык UCM допускает такие параллелизмы процессов, порождаемые стабами:  между процессами, генерируемыми разны- ми стабами, связанными с одними и теми же вложенными картами;  между процессами, генерируемыми раз- ными переходами к одному входу того же ста- ба – это обусловлено возможностью перехода к вложенной карте, не дожидаясь завершения предыдущего перехода;  между процессами, генерируемыми пере- ходами к разным входам того же стаба. Для идентификации разных локальных сред и их процессов, порожденных стабом, использу- ется понятие визита. К i-му визиту относятся процессы во вложенных картах стаба, иниции- рованные i-ми фишками на каждом из его вход- ных путей. После создания визита, можно гово- рить о среде визита и развивающихся в нем процессах. Одновременно могут существовать несколько визитов, в каждом из которых па- раллельно будут развиваться свои процессы. 5. Виды стабов На рис. 1 и 2 проиллюстрированы элементы стабов – совокупности вложенных карт, схемы их привязки к входам и выходам стаба, условия привязки карт к входам стаба и пороговые филь- тры на его выходах, а также описано понятие визита. В языке UCM определяется несколько видов стабов: статические, динамические, син- хронизирующие и блокирующие. Графическое их изображение в языке приведено на рис. 4. [ST] Static stub Dynamic stub Synchronizing stub S [ST] Blocking stub SB Рис. 4. Виды стабов и их графическое изображение Только ромб статического стаба прорисовыва- ется непрерывной линией. В синхронизирую- УСиМ, 2012, № 6 27 щем стабе внутри ромба добавляется буква S, указывающая на синхронизацию, осуществля- емую согласно значению синхронизирующего порога ST. Наконец, в блокирующем стабе до- полнительно появилась буква B как нижний индекс в его спецификации. Охарактеризуем особенности этих стабов. В случае статического стаба число вложенных карт не больше единицы и, если вложенная кар- та отсутствует, то такой стаб интерпретируется как тупик в процессе. В случае динамических стабов нет верхнего ограничения на число вло- женных карт. Синхронизирующий стаб – это частный случай динамического стаба, но отли- чается синхронизацией выхода процессов вло- женных карт из стаба в рамках среды одного визита. Количество синхронизируемых для вы- хода процессов задается (явно или по умолча- нию) пороговыми выражениями. Выход из син- хронизирующего стаба подобен вершине And- Join, поведение которой также специфицирует- ся пороговым выражением. Фишка выходит из синхронизирующего стаба только после нако- пления определенного числа фишек на выходе. В то же время такой выход отличается от вер- шин AndJoin тем, что в AndJoin требовалось по- лучение фишек с каждого входа слияния, а здесь существенно лишь общее количество поступив- ших фишек, но не те пути, по которым они при- ходят. Наконец, блокирующие стабы – такой част- ный случай синхронизирующего стаба, когда в каждый момент времени может выполняться не более одного визита стаба. У таких стабов могут образовываться очереди фишек на их входах, ожидающие завершения текущего ви- зита. Условиями завершения визита будем счи- тать такие:  по всем входным привязкам уже были инициированы процессы;  если все конечные вершины вложенной кар- ты достигнуты и все процессы уровня среды визита завершены. 6. Общая схема реализации семантики стабов Семантика стабов задана правилами 1–16 в табл. 2 для каждого типа стабов группой из че- тырех правил. Эти четыре группы правил впи- сываются в одну общую схему, когда все пер- вые (соответственно, все вторые, третьи, чет- вертые) правила внутри этих групп сходны меж- ду собой в том смысле, что они относятся к оп- ределенному этапу развития процессов, поро- ждаемых стабом. Содержательно эти этапы можно охарактеризовать как (1) от вершины перед стабом к структурам связывания (In- Binding) для этого входа, (2) от структур свя- зывания к стартовым вершинам путей вложен- ных карт, (3) от конечных вершин путей вло- женных карт к выходным структурам связыва- ния (OutBinding), и (4) от выходных структур связывания к вершине после стаба. Структура вложенности сред, использован- ная при реализации семантики стабов, отлича- ется от указанной в стандарте. Это вызвано следующими причинами:  среда визита не используется для статиче- ского и динамического стабов, так как ее свой- ства проявляются только в случае синхронизи- рующего (и блокирующего) стаба;  карты вкладываются в другие карты, но не вкладываются в визиты, а наоборот – визиты вкладываются в карты во избежание дополни- тельного размножения сред карт. Таким образом, структуру сред можно пред- ставить выражением E [M [V [C [ P ] ]]], где М, V, C и P – соответственно среды карт, визитов, компонент, а также процессы. Свойства и управляющие атрибуты для за- дания семантики стабов. Атрибутные транзи- ционные системы задаются описанием множе- ства их состояний и переходов. Состояния этих систем описываются совокупностями значений их атрибутов, переходы – правилами, изменяю- щими значения их атрибутов. В рассматривае- мых транзиционных системах атрибуты отно- сятся к конкретным средам – либо к глобаль- ной, либо к средам карт и визитов. Рассматрива- ются как функциональные атрибуты карт или визитов, и в качестве параметров этих атрибутов используются соответственно имена этих карт и визитов. Атрибуты, значения которых не изме- няются никакими правилами переходов, будем называть свойствами соответствующих сред. 28 УСиМ, 2012, № 6 В среде карт определяется3 следующее мно- жество свойств и атрибутов:  singleton: {MapName} → Bool – свойство, при истинности которого дополни- тельные экземпляры карты не создаются (см. рис. 3); по умолчанию значение true для каж- дой карты;  MapReplica: {MapName} → Int – свойство, указывающее число копий карты при формировании визита; по умолчанию значение 1 на всем множестве параметров; для статичес- ких стабов значение этого свойства всегда рав- но единице; если значение больше единицы, то в среду визита погружается столько экземпля- ров карты, каково для нее значение этого свой- ства;  StubVisit: {StubName} → Int – атрибут, указывающий число визитов стаба; начальное значение ноль;  StubCounter: {StubName}  {In- PathName} → Int – атрибут, указывающий число фишек, поступивших к вершине Stub- Name типа стаб по входному пути InPath- Name; начальное значение атрибута ноль;  threshold:{StubName}  {OutPath- Name} → Int – атрибут, указывающий по- роговое значение выходного пути OutPath- Name для вершины StubName типа стаб; если порог выходного пути OutPathName не ука- зан, то по умолчанию он вычисляется в момент образования визита как число его вложенных карт;  exit: {EndPointName} → {OutPat- hName} – атрибут, реализующий выходные привязки стаба; начальное значение атрибута Nil на всей области определения; его значение формируется при погружении карты и проис- ходит это таким образом, что пара из входного параметра и значения атрибута для него в со- вокупности соответствуют одной из выходных привязок стаба к карте; 3 Фигурные скобки используются для обозначения мно- жеств объектов, например, {MapName} означает множе- ство карт, заданных своими именами.  existvisit: {VisitName} → Bool – атрибут, указывающий наличие в среде теку- щей карты вложенной среды визита с задан- ным именем; начальное значение атрибута false. Отметим, что атрибут exit отличается от остальных тем, что в рамках описания семан- тики стабов он относится к вложенным картам, тогда как все остальные атрибуты относятся к картам, содержащим стаб. Атрибуты визитов локализуются в средах, соответствующих именам стабов, из которых осуществляется обращение к ним:  visit – атрибут, указывающий имя визи- та внутри его среды; для стаба StubName на- чальное значение этого атрибута генерируется при обращении к функции погружения (см. далее правило insertvisit), формирующей среду этого визита как текущее значение атри- бута карты StubVisit(StubName);  OutPathCounter: {OutPathName} → Int – атрибут, указывающий, сколько раз в рамках рассматриваемого визита был достиг- нут выходной путь OutPathName из стаба; начальное значение ноль;  enable: {OutPathName} → Bool – ат- рибут, указывающий для каждого выходного пути OutPathName стаба, был ли он достиг- нут в рамках данного визита хотя бы раз; на- чальное значение false;  past: {OutPathName} → Bool – атри- бут, указывающий для каждого выходного пу- ти OutPathName стаба, был ли он уже прой- ден; начальное значение false. Функция погружения. Особую роль в за- дании правил переходов описываемой транзи- ционной системы выполняет функция погру- жения, посредством которой интегрируются изменения в разных компонентах структури- рованной среды этой системы. В описании се- мантики стабов используются правила погру- жения apply, check и insert, описанные в [14], а также представленные здесь правила insertvisit, movein и moveout. Определяемые далее три новых правила (1–3) связаны с этапами общей схемы реализации ста- бов. Правило (1) применяется на первом этапе – УСиМ, 2012, № 6 29 от входных путей стаба к привязкам InBinding (на рис. 1 они представлены как структуры IB1 и IB2). Правило (2) применяется для моделиро- вания переходов от привязок к стартовым вер- шинам путей вложенных карт. И наконец, пра- вило (3) применяется при переходах от конеч- ных вершин путей вложенных карт к выход- ным привязкам (на рис. 1 они представлены как структуры OB). Правило (1), insertvisit, используется для ди- намического формирования сред визитов (де- вятая и тринадцатая строки в табл. 2): ( ) ( ) . [ \|\| ] \|\| [ _ [ ( , ); ] \|\| ] \|\| insertvisit V insertvisit V u u M u v w M V n initvisit V k u v w   (1) В этом правиле используются следующие обозначения: V – имя стаба, n – текущее значе- ние атрибута StubVisit(V), используемое для именования V_n среды формируемого ви- зита, initvisit – функция, осуществляющая ге- нерацию начальных значений атрибутов в сре- де формируемого визита. Параметр k, исполь- зуемый в приводимом ниже определении функ- ция initvisit – это количество выходных привя- зок (OutBinding структур) стаба V к карте М. ( : ( ), ( ) : ( ) 1, 1.. ( ( _ ( )) : , ( _ ( )) : , ( _ ) : ( , ) visit StabVisit V StabVisit V StabVisit V for K k enable out K V false past out K V false OutPathCounter out K initvisit V k        0 ) )  В результате в текущей среде создается вло- женная среда визита с именем V_n , в которой формируются его локальные атрибуты visit, enable, past, OutPathCounter, первый из кото- рых скалярный. У остальных параметром слу- жат вершины, идентифицируемые с выходны- ми путями out_K(V) стаба V, К = 1..k, и предна- значенные для перехода фишек изнутри этого визита во внешнюю карту, которой принадле- жит сам стаб. Заметим, что порождаемая после применения этого правила среда визита вкла- дывается в карту M. Правило movein представлено в двух вари- антах, (2а) и (2b), разнящихся значением свой- ства singleton погружаемой карты М2:  ( , 2) ( , 2) 1 & ( 2) 0 &( ( 2)) 1[ ] 1[ ( 2 [ ( , 2, ). )] movein V M movein V M u u singleton M r MapReplica M M u v w M copy M initexit V M n u       1 , ( 2 [ ( , 2, ). )]rcopy M initexit V M n u v w   (2a)  ( , 2) ( , 2) 1 & ( 2) 1 &( ( 2)) 1[ ] 1[( 2 [ ( , 2, ). ] movein V M movein V M u u singleton M r MapReplica M M u v w M M initexit V M n u       1 ( 2 [ ( , 2, ). ]rM initexit V M n u v w   . (2b) В обоих случаях параметры перехода uu 2MVmovein   ),( в посылке правила и контекст применения правила имеют следующую интер- претацию. Вершина u – это входная привязка i-го входного пути стаба V, расположенного внут- ри карты М1, к вложенной карте М2, u – соот- ветствующая стартовая вершина пути карты М2. Если обратиться к примеру на рис. 1, то u – это входной путь стаба в одной из структур IB1 или IB2, а u – стартовая вершина пути карты, в которую ведет пунктирная стрелка из u. Прави- ло (2а) погружает r копий карты M2 в среду карты М1, в которой расположен стаб. Функция initexit, формирующая значение ат- рибута exit для карты М2 (или ее копий), опре- деляется соотношением initexit (V, M, n) = = (for K = 1n (exit (EndPoint_K(M), V) := aK)). В среде каждой такой копии посредством об- ращения к функции initexit (V, M, n) = (for K = = 1n (exit (EndPoint_K(M), V) := aK)) форми- руется такое значение функционального атри- бута exit, когда каждой конечной вершине EndPoint_K карты М сопоставляется выходная вершина стаба V, образующая вместе с ней вы- ходную привязку стаба (в обозначениях рис. 1 и 2 – это структуры OB, ассоциированные с кар- той M2). И также в среду каждой такой копии карты M2 погружается u, стартовая вершина процесса в М2. Правило (2b) отличается от пра- вила (2а) истинностью свойства singleton для карты М2. Если это свойство карты М2 истин- но, то погружается сама карта, а не ее копии. Правило (3), moveout, определяет переход фишки из вложенной карты в среду карты верхнего уровня: ( ) . ( ) 1[ 2[ \|\| ] \|\| ] \|\| 1[ 2[ ] \|\| \|\| ] \|\| moveout exit u moveout exit M M u v w z M M v exit w z   (3) 30 УСиМ, 2012, № 6 Контекст этого перехода   )(exitmoveoutu следующий: u – это некоторая конечная вер- шина пути, пусть для определенности ep, вло- женной карты М2, exit – соответствующая ep выходная привязка, определяемая как значение exit(ep) функционального атрибута, ∆ – символ завершения процесса внутри вложенной кар- ты. В результате применения этого правила фишка перемещается из вложенной карты к соответствующей точке выходной привязки (в терминах рис. 1 это некая структура OB, ассо- циированная с картой М2), от которой процесс ее перемещений может продолжиться. 7. Уравнения, реализующие процессы в стабах Далее приводится табл. 2, в которой даны уравнения четырех видов в алгебре поведений, определяющие семантику стабов: уравнения (1)–(4) для статических стабов, уравнения (5)– (8) для динамических стабов, уравнения (9)– (12) – для синхронизирующих динамических стабов, и (13)–(16) – для блокирующих синхро низирующих динамических стабов. Для крат- кости в столбце «Конструкт» этой таблицы бу- дет использована только основная часть назва- ния каждого типа, т.е. статический, динамиче- ский, синхронизирующий или блокирующий. Уравнения (1)–(8), определяющие семанти- ку статических и динамических стабов, доста- точно просты, их легко можно проиллюстри- ровать (см. рис. 1 и 2), поэтому подробные по- яснения к ним здесь опускаются. Уравнения для синхронизирующих и блокирующих ста- бов почти идентичны: в частности (14), (15) и (16) соответственно повторяют уравнения (10), (11) и (12). Уравнение (13) отличается от урав- нения (9) тем, что в нем дополнительно учиты- вается атрибут existvisit, посредством ко- торого блокируется создание новых визитов для заданного стаба. Поэтому после представ- ления табл. 2 будут даны достаточно деталь- ные комментарии к правилам 9–12 и к отличи- ям правила 13 от правила 9. Таблица 2. Уравнения в алгебре поведений, определяющие семантику стабов № Конструкт UCM пред- ставление Уравнение Комментарий 1 2 3 4 5 1 К входной привязке статичес- кого стаба S = T_in T – стаб, in – входной путь T от верши- ны S, T_in – входная привязка 2 От входной привязки статичес- кого стаба к вложен- ной карте S_in = movein(S,m).T S_in – входная привязка стаба S, m – вложенная карта со старто- вой вершиной T 3 От вложен- ной карты к выходной привязке статическо- го стаба S = сheck(c). moveout(exit(out)) S – конечная вершина вложен- ной карты, c – условие завершения S, T – стаб, Т_out – его выходная привязка, соответствующая S 4 От выход- ной при- вязки ста- тического стаба S_out = T S – стаб, out – выходная привязка S 5 К входной привязке динамиче- ского стаба S = insert(T_in_m1, …, T_in_mp) T – стаб, in – входной путь T, m1, …, mp – вложенные карты стаба УСиМ, 2012, № 6 31 Продолжение табл. 2 1 2 3 4 5 6 От входной привязки динамиче- ского стаба к вложен- ной карте S_in_m = check(c).movein(S,m).T S – стаб, in – входной путь S, m – вложенная карта, c – условия привязки карты m, T – стартовая вершина в m 7 От вложен- ной карты к выходной привязке динамиче- ского стаба S = check(c).moveout(exit(out)) S – конечная вершина вложен- ной карты, c – условие завершения S, T – стаб, T_out – выходная привязка T, соответствующая S 8 От выход- ной привяз- ки динами- ческого стаба S_out = T S – стаб, Т – вершина, следующая за S на выходном пути out, S_out – выходная привязка стаба 9 К входной привязке синхрони- зирующего стаба S = check(StubCounter(T, in) = StubVisit(T)). apply(StubCounter(T, in) := StubCounter(T,in)+1, StubVisit(T):=StubVisit(T) + 1).insertvisit(T). (insert(check(visit = StubCoun- ter(T,in1)).(T_in1_m1, …, T_in1_mp)) \|\| … \|\| insert(check(visit = StubCounter(T, ink)).(T_ink_m1, …, T_ink_mp))) + (check(StubCounter(T, in) < Stub- Visit(T)).apply(StubCounter(T, in) := StubCounter(T, in) + 1)) T – стаб c вершиной S, пред- шествующей ему на входном пути in m1, …, mp – вложенные карты, n – количество выходных пу- тей T, in1, …, ink – входные пути T, T_inq_mr – входная привязка пути inq для карты mr 10 От входной привязки синхрони- зирующего стаба к вложенной карте S_in_m = check(c).movein(S,m).T S – стаб с входной привязкой in, m – вложенная карта, c – условие привязки, T – стартовая вершина в карте m 11 От вложен- ной карты к выходной привязке синхрони- зирующего стаба S = check(c & (enable(out) = false) & (past(out) = false)).apply(enable(out) := true, OutPathCoun- ter(out) := OutPathCounter(out) + 1).moveout- (exit(out)) + check(c & (enable(out) = true) & (past(out)= false)).apply(OutPathCounter(out) := OutPathCounter(out) + 1) + check(c & (past(out) = true)) S – конечная вершина пути карты плагина, c – условие завершения S, T – синхронизирующий стаб, out – выходная привязка T, соответствующая S 12 От выход- ной привяз- ки синхро- низирую- щего стаба S_out = check(OutPathCounter(out) >= threshold(S, out)).apply(past(out) := true).T S – стаб, out – выходной путь из S в Т , S_out – выходная привязка 13 К входной привязке блокирую- щего стаба S = check((StubCounter(T,in) <= StubVisit(T)) & ~existvisit(T_1)).apply(StubCounter(T,in):= Stub- Counter(T,in)+1, StubVisit(T):=StubVisit(T)+1). insertvisit(T). (insert(check(StubCounter(T, in1) > 0).(T_in1_m1, …, T_in1_mp)) \|\| … \|\| insert(check(StubCounter(T, ink) > 0).(T_ink_m1, …, T_ink_mp))) + check((StubCounter(T, in) < StubVisit(T)) & exist- visit(T_1)).apply(StubCounter(T,in):=StubCounter( T, in) + 1) T – блокирующий стаб, in – входной путь T из S, m1, …, mp – вложенные карты, n – количество выходных пу- тей T, in1, …, ink – входные пути T 32 УСиМ, 2012, № 6 Продолжение табл. 2 14 От вход- ной при- вязки бло- кирующе- го стаба к вложенной карте S_in_m = check(c).movein(S,m).T S – блокирующий стаб с вход- ным путем in, m – вложенная карта, c – условия привязки для m, T – стартовая вершина пути карты m 15 От вло- женной карты к выходной привязке блоки- рующего стаба S = check(c & (enable(out) = false) & (past(out) = false)).apply(enable(out) := true, OutPathCoun- ter(out) := OutPathCounter(out) + 1).moveout(exit(out)) + check(c & (enable(out) = true) & (past(out) = false)).apply(OutPathCounter(out) := OutPathCoun- ter(out) + 1) + check(c & (past(out) = true)) S – конечная вершина пути вложенной карты, с – условие S, T – блокирующий стаб, out – выходной путь T, T_out – выходная привязка, соответствующая S 16 От выход- ной при- вязки бло- кирующе- го стаба S_out = check(OutPathCounter(out) = threshold(S, out)).apply(past(out) := true).T S – блокирующий стаб, out – выходной путь из S в Т , S_out выходная привязка Комментарий к правилу 9. Правило содер- жит две альтернативы, разделенные знаком +. Одна – описывает случай StubCounter(T,in)= StubVisit(T), когда для фишки, пришедшей к стабу Т по входу in должен быть создан но- вый визит. Другая соответствует случаю Stub- Counter(T,in) < StubVisit(T), когда пришедшая фишка относится к одному из уже созданных визитов. Действие, выполняемое во втором случае, сводится к увеличению счетчи- ка StubCounter(T, in)на единицу. В свою очередь, результат этого действия может сде- лать истинным равенство visit = Stub- Counter(T, in) внутри одного из ранее со- зданных визитов, что позволит осуществлять переходы для других фишек внутри визита. Выполнение равенства StubCounter(T, in)=StubVisit(T)в первой альтернативе вле- чет следующую последовательность действий:  увеличение обоих счетчиков StubCoun- ter(T, in) и StubVisit(T);  создание нового визита обращением к пра- вилу погружения insertvisit(T);  погружение в среду этого визита всех вход- ных привязок T_in1_m1,, T_ink_mp для всех карт этого стаба. Последнее действие представляет собой па- раллельное погружение агентов, соответствую- щих k входам стаба. Рассмотрим ветвь для входа in1. Она начинается с проверки уже упомяну- того равенства visit = StubCounter(T, in1), за которым следует копирование фишки в p параллельных ветвях, по одной для каждой карты m1,, mp. Комментарий к правилу 10. Это правило предполагает два действия: проверку истинно- сти предусловия структуры PluginBinding для карты m и ее погружение в среду визита. Комментарий к правилу 11. Этим правилом специфицируется передача фишки от конеч- ных вершин путей вложенных карт к выход- ным привязкам. Уравнение перехода содержит три альтернативы. Первая альтернатива, когда переход фишки к привязке не состоялся, описывается поведе- нием check(c & enable(out)=false)& &(past(out)=false)).apply(enable(out):= := true, OutPathCounter(out):=OutPath- Counter(out)+1).moveout(exit(out)). После того, как выполнена эта альтернатива, т.е. проверено, что переход может состояться, счетчик числа перешедших фишек увеличивает- ся на единицу и посредством функции move- out фишка переходит к выходной привязке. Вторая альтернатива с поведением check(c & & (enable(out) = true) & (past(out) = УСиМ, 2012, № 6 33 false)).apply(OutPathCounter(out):= := OutPathCounter(out)+1) соответству- ет случаю, когда уже имеются фишки для дан- ной выходной привязки, достигшие конечных вершин путей, но их число еще меньше порого- вого значения, что не позволяет фишке перей- ти к выходной привязке. После проверки ус- ловия этой альтернативы увеличивается на единицу счетчик выходного пути, но фишка к выходной привязке не переходит, посколь- ку она уже перешла туда по первой альтерна- тиве. Наконец, третья альтернатива check(c & & (past(out) = true)) представляет собой случай, когда число достигнутых конечных вер- шин путей для данной выходной привязки уже больше или равно пороговому значению, и фиш- ка перешла из выходной привязки стаба по пу- ти out к следующей за стабом вершине пути. Комментарий к правилу 12. Это правило S_out = check(OutPathCounter(out)>= threshold(S,out)).apply(past(out):= := true).T описывает переход фишки от вы- ходной привязки S_out к вершине Т, непосред- ственно следующей за стабом S на пути out. Комментарий к правилу 13. Это правило отличается от правила 9 тем, что условия вы- полнения каждой из двух его альтернатив до- полнительно предполагают проверку истинно- стного значения existvisit(T_1). Здесь первая поведенческая альтернатива в уравне- нии позволяет формировать новый визит для блокирующего стаба Т только если в среде кар- ты, которой принадлежит стаб, не существует других визитов для этого стаба. Вторая альтер- натива описывает обработку фишки текущего визита, которая пришла по входу in. 8. Заключение. В работе применен инсер- ционный подход для формализованного описа- ния семантики стабов в языке параллельного моделирования UCM. Для каждого из представ- ленных видов стабов (статический, динамиче- ский, синхронизирующий и блокирующий) при- ведено описание семантики в алгебре процес- сов, использующее функцию погружения и сис- тему управляющих атрибутов. В то же время, учитывая все многообразие средств языка UCM и ситуаций, возможных при развитии процес- сов, специфицируемых в нем, некоторые дета- ли в описании семантики опущены. Например, не представлены правила, применяемые при уда- лении сред. Рассматриваемая семантика охватывает раз- личные известные виды параллелизма: парал- лелизм между заданиями, который проявляет- ся как параллелизм между обращениями к од- ной и той же карте из разных стабов; паралле- лизм по данным, поступающими на разные вхо- ды; потоковый, или pipeline параллелизм, ко- торый наблюдается между разными (по време- ни) обращениями к одному и тому же стабу. Стаб – это, наряду с понятием компонент, тот конструкт языка UCM, который привносит в него иерархию сред. Предпринята попытка уви- деть аналогии между стабами UCM и процеду- рами в языках программирования, которые слу- жат испытанным средством для уменьшения повторов в программных текстах. По мнению автора, в стабах можно было бы в полной мере имплементировать и процедурную парадигму, причем сохраняя все многообразие их видов. Достаточно было бы вынести описание стабов в отдельный раздел, провести их именование, а также упорядочение на множестве входов и выходов. Автор выражает признательность А.А. Губе и К.И. Шушпанову за обсуждения по семанти- ке языка UCM. 1. International Telecommunications Union. Recommenda- tion Z.120 – Message Sequence Charts (MSC), 1998. 2. Ibid. Recommendation Z.100 – Specification and De- scription Language (SDL), 1999. – 232 p. – http://www. itu.int/ITU-T/studygroups/com10/languages/Z.1001199. pdf 3. Object Management Group. Unified Modeling Langu- age Specification, 2.0. – 2003. – 624 p. – http;//www. sparxsystems.com.au/bin/UML2SuperStructure.pdf 4. International Telecommunications Union. Recommen- dation Z.151 – User Requirements Notation (URN), 2008. – 190 p. – http://www.itu.int/rec/T-REC-Z.151- 200811-I/en 5. Инсерционное программирование / А.А. Летичевс- кий, Ю.В. Капитонова, В.А. Волков и др. // Киберне- тика и системный анализ. – 2003. – № 1. – С. 12–32. 6. Milner R. Communication and Concurrency // Int. Se- ries in Comp. Sci. – Prentice-Hall, 1989. – 300 p. 7. Hoare C.A.R. Communicating Sequential Processes // Ibid, 1985. – http://www.usingcsp.com/cspbook.pdf 34 УСиМ, 2012, № 6 8. Kealey J., Amyot D. Enhanced Use Case Map Traversal Semantics / 13th SDL Forum (SDL'07). – Paris, France: Springer, LNCS 4745. – P. 133–149. (Sept. 2007). – http://dl.acm.org/citation.cfm?id=1779946 9. Mussbacher G. Aspect-Oriented User Requirements No- tation / Thesis submitted to the Faculty of Graduate and Postdoctoral Studies in partial fulfillment of the require- ments for the degree of Ph.D. in Comp. Sci. University of Ottawa, Ottawa, Canada, Sept. 2010. – P. 326. – http://lo- tos.sci.uottava.ca/ucm/pub/UCM/VirLibGunterPhDThe- sis/AspectOriented_User_Requirements_Notation.pdf 10. Hassine J., Rilling J., Dssouli R. An ASM Operational Semantics for Use Case Maps / 13th IEEE Int. Re- quirement Eng. Conf. (RE’05), IEEE Computer Society Press, Sept. 2005. – P. 467–468. – http://dl.acm.org/cita- tion.cfm/?id=1100666 11. Jameleddine Hassine. Formal semantics and verifica- tion of use case maps / A thesis in The Depart. of Comp. Sci. and Software Eng., Concordia University, Montreal, Quebec, Canada, 2008. – 284 p. – http://lotos.site.uotta- va.ca/ucm/pub/UCM/VirLibJamelPhDThesis/phd_ih.pdf 12. Weiss M., Amyot D. Business Process Modeling with URN // Int. J. of E-Business Research. – July-Sept. 2005. – N 3, 1. – P. 63–90. 13. ISO/IEC. Software and system engineering. High-level Petri nets, part 1, Concepts, definitions and graphical notation, 2004. – 38 p. – http://www.iso.org/iso/iso_ca- talogue/catalogue_tc/catalogue_detail.htm?csnumber= 38225 14. Губа А.А., Шушпанов К.И. Инсерционная семанти- ка плоских многопотоковых моделей языка UCM // УСиМ – № 6. – С. 15–21, 34. Тел. для справок: +38 067 468-6035 (Киeв) © А.Б. Годлевский, 2012 

Инсерционная семантика параллельных процедурных конструктов языка UCM

Institution

Ähnliche Einträge