Формальные методы анализа дискретных систем с использованием языка спецификаций
Описано реалізацію алгоритму переведення набору діаграм MSC (документа MSC) в подійно еквівалентну йому мережу Петрі, наведено доказ коректності зазначеного алгоритму. Мережа, що отримана таким чином, може бути використана для аналізу властивостей вихідного документа MSC. Наведений алгоритм є складо...
Збережено в:
| Опубліковано в: : | Кибернетика и системный анализ |
|---|---|
| Дата: | 2009 |
| Автори: | , |
| Формат: | Стаття |
| Мова: | Russian |
| Опубліковано: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2009
|
| Теми: | |
| Онлайн доступ: | https://nasplib.isofts.kiev.ua/handle/123456789/44382 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Цитувати: | Формальные методы анализа дискретных систем с использованием языка спецификаций/ С.Л. Крывый, А.В. Чугаенко // Кибернетика и системный анализ. — 2009. — № 4. — С. 31-48. — Бібліогр.: 13 назв. — рос. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
nasplib_isofts_kiev_ua-123456789-44382 |
|---|---|
| record_format |
dspace |
| spelling |
Крывый, С.Л. Чугаенко, А.В. 2013-05-31T20:20:20Z 2013-05-31T20:20:20Z 2009 Формальные методы анализа дискретных систем с использованием языка спецификаций/ С.Л. Крывый, А.В. Чугаенко // Кибернетика и системный анализ. — 2009. — № 4. — С. 31-48. — Бібліогр.: 13 назв. — рос. 0023-1274 https://nasplib.isofts.kiev.ua/handle/123456789/44382 51.681.3 Описано реалізацію алгоритму переведення набору діаграм MSC (документа MSC) в подійно еквівалентну йому мережу Петрі, наведено доказ коректності зазначеного алгоритму. Мережа, що отримана таким чином, може бути використана для аналізу властивостей вихідного документа MSC. Наведений алгоритм є складовою частиною системи аналізу та верифікації документів MSC. The paper describes the realization of the algorithm for translating an MSC diagram set (MSC document) to Petri net modulo event equivalence and proves the correctness of the algorithm. The net obtained by this method can be used to analyze the properties of the original MSC document. The algorithm is a part of a system of MSC document verification and analysis. ru Інститут кібернетики ім. В.М. Глушкова НАН України Кибернетика и системный анализ Кибернетика Формальные методы анализа дискретных систем с использованием языка спецификаций Формальні методи аналізу дискретних систем з використанням мови специфікацій Formal methods of discrete systems analysis using a specification language Article published earlier |
| institution |
Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| collection |
DSpace DC |
| title |
Формальные методы анализа дискретных систем с использованием языка спецификаций |
| spellingShingle |
Формальные методы анализа дискретных систем с использованием языка спецификаций Крывый, С.Л. Чугаенко, А.В. Кибернетика |
| title_short |
Формальные методы анализа дискретных систем с использованием языка спецификаций |
| title_full |
Формальные методы анализа дискретных систем с использованием языка спецификаций |
| title_fullStr |
Формальные методы анализа дискретных систем с использованием языка спецификаций |
| title_full_unstemmed |
Формальные методы анализа дискретных систем с использованием языка спецификаций |
| title_sort |
формальные методы анализа дискретных систем с использованием языка спецификаций |
| author |
Крывый, С.Л. Чугаенко, А.В. |
| author_facet |
Крывый, С.Л. Чугаенко, А.В. |
| topic |
Кибернетика |
| topic_facet |
Кибернетика |
| publishDate |
2009 |
| language |
Russian |
| container_title |
Кибернетика и системный анализ |
| publisher |
Інститут кібернетики ім. В.М. Глушкова НАН України |
| format |
Article |
| title_alt |
Формальні методи аналізу дискретних систем з використанням мови специфікацій Formal methods of discrete systems analysis using a specification language |
| description |
Описано реалізацію алгоритму переведення набору діаграм MSC (документа MSC) в подійно еквівалентну йому мережу Петрі, наведено доказ коректності зазначеного алгоритму. Мережа, що отримана таким чином, може бути використана для аналізу властивостей вихідного документа MSC. Наведений алгоритм є складовою частиною системи аналізу та верифікації документів MSC.
The paper describes the realization of the algorithm for translating an MSC diagram set (MSC document) to Petri net modulo event equivalence and proves the correctness of the algorithm. The net obtained by this method can be used to analyze the properties of the original MSC document. The algorithm is a part of a system of MSC document verification and analysis.
|
| issn |
0023-1274 |
| url |
https://nasplib.isofts.kiev.ua/handle/123456789/44382 |
| citation_txt |
Формальные методы анализа дискретных систем с использованием языка спецификаций/ С.Л. Крывый, А.В. Чугаенко // Кибернетика и системный анализ. — 2009. — № 4. — С. 31-48. — Бібліогр.: 13 назв. — рос. |
| work_keys_str_mv |
AT kryvyisl formalʹnyemetodyanalizadiskretnyhsistemsispolʹzovaniemâzykaspecifikacii AT čugaenkoav formalʹnyemetodyanalizadiskretnyhsistemsispolʹzovaniemâzykaspecifikacii AT kryvyisl formalʹnímetodianalízudiskretnihsistemzvikoristannâmmovispecifíkacíi AT čugaenkoav formalʹnímetodianalízudiskretnihsistemzvikoristannâmmovispecifíkacíi AT kryvyisl formalmethodsofdiscretesystemsanalysisusingaspecificationlanguage AT čugaenkoav formalmethodsofdiscretesystemsanalysisusingaspecificationlanguage |
| first_indexed |
2025-11-25T20:15:38Z |
| last_indexed |
2025-11-25T20:15:38Z |
| _version_ |
1850522649649741824 |
| fulltext |
ÓÄÊ 51.681.3
Ñ.Ë. ÊÐÛÂÛÉ, À.Â. ×ÓÃÀÅÍÊÎ
ÔÎÐÌÀËÜÍÛÅ ÌÅÒÎÄÛ ÀÍÀËÈÇÀ ÄÈÑÊÐÅÒÍÛÕ ÑÈÑÒÅÌ
Ñ ÈÑÏÎËÜÇÎÂÀÍÈÅÌ ßÇÛÊÀ ÑÏÅÖÈÔÈÊÀÖÈÉ
Êëþ÷åâûå ñëîâà: ñåòè Ïåòðè, ÿçûê MSC, âåðèôèêàöèÿ.
ÂÂÅÄÅÍÈÅ
Ñîâðåìåííûå êîìïüþòåðíûå ñèñòåìû ýâîëþöèîíèðóþò â ñòîðîíó óñëîæíåíèÿ
ñâîåé ñòðóêòóðû, è ïîýòîìó â ïðîöåññå èõ ðàçðàáîòêè è ïðîåêòèðîâàíèÿ âîçíè-
êàåò ïîòðåáíîñòü â èñïîëüçîâàíèè ôîðìàëüíûõ ìåòîäîâ âåðèôèêàöèè øàãîâ
ïðîåêòèðîâàíèÿ, â îáîñíîâàíèè ïðèíÿòûõ ðåøåíèé, ïðîâåðêå âûïîëíèìîñòè ñïå-
öèôèêàöèé è ò.ï. Èññëåäîâàíèÿ â ýòîé îáëàñòè ïðèâåëè ê òîìó, ÷òî âåðèôèêà-
öèÿ êîìïüþòåðíûõ ñèñòåì âûäåëèëàñü â îòäåëüíóþ ïðîáëåìó. Çà ïîñëåäíåå
äâàäöàòèëåòèå èìååòñÿ ñóùåñòâåííûé ïðîãðåññ, îáóñëîâëåííûé ïðåæäå âñåãî
âîçíèêíîâåíèåì è áûñòðûì ðàçâèòèåì ìåòîäà ïðîâåðêè íà ìîäåëè (model
checking). Áëàãîäàðÿ ýòîìó ìåòîäó ñòàëà âîçìîæíîé âåðèôèêàöèÿ ðåàêòèâíûõ
ñèñòåì, êîòîðàÿ, â ÷àñòíîñòè, ñâîäèòñÿ ê ïðîâåðêå âûïîëíèìîñòè ñïåöèôèêàöèé,
îïèñûâàþùèõ îæèäàåìûå ïîâåäåíèÿ ñèñòåìû. Ïðè ýòîì ñïåöèôèêàöèè çàïèñû-
âàþòñÿ â îïðåäåëåííîì ôîðìàëüíîì ëîãè÷åñêîì ÿçûêå, â òî âðåìÿ êàê ñàìà ñè-
ñòåìà âûñòóïàåò â êà÷åñòâå ìîäåëè, íà êîòîðîé ïðîâåðÿåòñÿ âûïîëíèìîñòü åå
ñïåöèôèêàöèé.
Íàñòîÿùàÿ ñòàòüÿ îòíîñèòñÿ ê îáëàñòè âåðèôèêàöèè, â êîòîðîé ïðåäëàãàåòñÿ
çàïèñûâàòü ñïåöèôèêàöèè ïðîãðàììíîé ñèñòåìû â îäíîì èç ÿçûêîâ òåìïîðàëüíîé
ëîãèêè, à ñàìó ñèñòåìó ìîäåëèðîâàòü ñðåäñòâàìè ÿçûêà MSC (Message Sequence
Charts) [1], ò.å. ïðåäñòàâëÿòü â âèäå MSC-äèàãðàìì. Èññëåäîâàíèå ñòðóêòóðíûõ
ñâîéñòâ MSC-äèàãðàìì, ïðåäñòàâëÿþùèõ äàííóþ ïðîãðàììíóþ ñèñòåìó, âûïîëíÿ-
åòñÿ ïóòåì êîíâåðòàöèè MSC-äèàãðàììû â ñåòü Ïåòðè (ÑÏ), à ïðîâåðêà âûïîëíè-
ìîñòè ñïåöèôèêàöèè îñóùåñòâëÿåòñÿ ïîñòðîåíèåì òðàíçèöèîííîé ñèñòåìû äëÿ ïî-
ëó÷åííîé â ðåçóëüòàòå êîíâåðòàöèè ÑÏ.  ÷àñòíîñòè, îïèñûâàåòñÿ àëãîðèòì êîí-
âåðòàöèè MSC-äèàãðàìì â ÑÏ, êîòîðûé ïðèìåíèì ïðàêòè÷åñêè êî âñåìó
ìíîæåñòâó îïåðàòîðîâ, âêëþ÷åííûõ â ñòàíäàðò ýòîãî ÿçûêà (ñ èñïîëüçîâàíèåì
ñòðîãîé ïîñëåäîâàòåëüíîé êîìïîçèöèè äèàãðàìì). Óñòàíàâëèâàåòñÿ ñîáûòèéíàÿ ýê-
âèâàëåíòíîñòü èñõîäíûõ MSC-îïèñàíèé è ïîëó÷åííîé ïî íèì ÑÏ. Äåòàëüíûé àíà-
ëèç ÿçûêà MSC ïîêàçàë, ÷òî êîíâåðòèðóåìûé âàðèàíò ýòîãî ÿçûêà ïî âûðàçèòåëü-
íûì ñâîéñòâàì ýêâèâàëåíòåí îðäèíàðíûì ÑÏ (ÿçûê MSC ìîæåò èñïîëüçîâàòüñÿ
êàê íàäñòðîéêà íàä ïðîèçâîëüíûì ÿçûêîì ïðîãðàììèðîâàíèÿ, çà ñ÷åò êîòîðîãî
äîñòèãàåòñÿ åãî àëãîðèòìè÷åñêàÿ ïîëíîòà). Äàííàÿ ñòàòüÿ ïðèìûêàåò ê ðàáîòàì ïî
êîíâåðòàöèè êîíñòðóêöèé ÿçûêà MSC â ÑÏ [2, 3] è çàâåðøàåò öèêë ðàáîò [4–8].
Âñå âûøåñêàçàííîå ñîñòàâëÿåò åäèíûé òåõíîëîãè÷åñêèé ïðîöåññ èññëåäîâàíèÿ
ñâîéñòâ èñõîäíîé ìîäåëè ñèñòåìû.
1. ÍÅÎÁÕÎÄÈÌÛÅ ÎÏÐÅÄÅËÅÍÈß È ÏÎÍßÒÈß
1.1. Êðàòêèå ñâåäåíèÿ ïî ñåòÿì Ïåòðè [9]. Îïðåäåëåíèå 1. Ñåòü Ïåòðè — ýòî
óïîðÿäî÷åííàÿ ïÿòåðêà ( , , , , )P T F W M 0 , ãäå P — íåïóñòîå êîíå÷íîå ìíîæåñòâî,
ýëåìåíòû êîòîðîãî íàçûâàþòñÿ ìåñòàìè ñåòè; T — íåïóñòîå êîíå÷íîå ìíîæå-
ñòâî, ýëåìåíòû êîòîðîãî íàçûâàþòñÿ ïåðåõîäàìè ñåòè; F P T T P� � � � — îòíî-
øåíèå èíöèäåíòíîñòè ìåæäó ïåðåõîäàìè è ìåñòàìè; W F: \� � { }0 è M P0 : ��
— äâå ôóíêöèè, íàçûâàåìûå êðàòíîñòüþ äóã è íà÷àëüíîé ðàçìåòêîé ñîîòâåò-
ñòâåííî. Ïðè ýòîì âûïîëíÿþòñÿ ñëåäóþùèå óñëîâèÿ:
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2009, ¹ 4 31
� Ñ.Ë. Êðûâûé, À.Â. ×óãàåíêî, 2009
• P T� � (ìíîæåñòâà ìåñò è ïåðåõîäîâ íå ïåðåñåêàþòñÿ);
•
� � � � �
x P T y P T xFy yFx: (ëþáîé ýëåìåíò ñåòè èíöèäåíòåí õîòÿ áû
îäíîìó ýëåìåíòó äðóãîãî òèïà).
Äëÿ óäîáñòâà ìíîæåñòâà ìåñò è ïåðåõîäîâ áóäåì ñ÷èòàòü ñòðîãî óïîðÿäî÷åí-
íûìè, ò.å. P p p n Pn� �( , , ), | |1 � , T t t m Tm� �( , , ), | |1 � .
Îïðåäåëåíèå 2. Ñåòü Ïåòðè, êðàòíîñòü âñåõ äóã êîòîðîé ðàâíà åäèíèöå, íàçû-
âàåòñÿ îðäèíàðíîé.
Ãðàôè÷åñêè ñåòü Ïåòðè ïðåäñòàâëÿåòñÿ â âèäå äâóäîëüíîãî îðèåíòèðîâàííîãî
ãðàôà ñ äâóìÿ òèïàìè âåðøèí: ìåñòàìè è ïåðåõîäàìè. Ìåñòà èçîáðàæàþòñÿ â âèäå
êðóæêîâ, à ïåðåõîäû — â âèäå ïðÿìîóãîëüíèêîâ. Äóãè ãðàôà ñîåäèíÿþò èíöèäåíò-
íûå âåðøèíû. Åñëè êðàòíîñòü êàêîé-ëèáî äóãè áîëüøå åäèíèöû, òî åå îáîçíà÷àþò
÷èñëîì, ñòîÿùèì ðÿäîì ñ äóãîé, èëè (äëÿ íåáîëüøîé êðàòíîñòè) çàìåíÿþò ñîîòâåò-
ñòâóþùèì ïó÷êîì äóã. Ðàçìåòêó èçîáðàæàþò öèôðîé âíóòðè êðóæêà èëè (äëÿ íå-
áîëüøèõ çíà÷åíèé) ñîîòâåòñòâóþùèì êîëè÷åñòâîì òî÷åê âíóòðè êðóæêà. Òî÷êè,
îáîçíà÷àþùèå ðàçìåòêó ñåòè, òàêæå íàçûâàþò ôèøêàìè.
Ðàçìåòêó ñåòè N ïðåäñòàâëÿåò ôóíêöèÿ M P: � � . Ó÷èòûâàÿ, ÷òî ìíîæåñòâî
ìåñò ñåòè óïîðÿäî÷åíî, ðàçìåòêó ìîæíî çàäàòü âåêòîðîì ÷èñåë M m mn� ( , , )1 � ,
ãäå m M p i ni i� �( ), , ,1 � .
Ââåäåì ïîíÿòèå ôóíêöèè èíöèäåíòíîñòè f P T T P: � � � � � :
f x y
n xFy W x y n
xFy
( , )
, ( ( , ) ),
, ( ).
�
� �
�
�
�
�0
 ýòîì ñëó÷àå êàæäîìó ïåðåõîäó t T� ìîæíî ñîïîñòàâèòü äâà âåêòîðà:
* ( ) ( , , ), ( , )F t b b b f p tn i i� �1 � ,
F t b b b f t pn i i( ) ( , , ), ( , )* � �1 � ,
ïðè ýòîì ïåðåõîä t ìîæåò ñðàáîòàòü ïðè ðàçìåòêå M òîãäà è òîëüêî òîãäà, êîãäà
M F t�* ( ) è åãî ñðàáàòûâàíèå ïåðåâåäåò ðàçìåòêó M â ðàçìåòêó M� ïî ñëåäóþ-
ùåìó ïðàâèëó:
M M F t F t� � � �* *( ) ( ) .
 ñëó÷àå, åñëè ïðè äàííîé ðàçìåòêå â ñåòè ìîæåò ñðàáîòàòü íåñêîëüêî ïåðåõî-
äîâ, òî îíè ñðàáàòûâàþò â ïðîèçâîëüíîì ïîðÿäêå íåçàâèñèìî îäèí îò äðóãîãî.
Åñëè ïåðåõîä t ìîæåò ñðàáîòàòü ïðè ðàçìåòêå M è â ðåçóëüòàòå ïîëó÷èòñÿ ðàç-
ìåòêà M�, òî ãîâîðÿò, ÷òî ðàçìåòêà M� íåïîñðåäñòâåííî äîñòèæèìà èç M ïóòåì ñðà-
áàòûâàíèÿ ïåðåõîäà t (M M
t
� �).
Îòíîøåíèå íåïîñðåäñòâåííîé äîñòèæèìîñòè ìîæíî îáîáùèòü. Ñ÷èòàåòñÿ, ÷òî
ðàçìåòêà M� äîñòèæèìà èç ðàçìåòêè M, åñëè ñóùåñòâóåò ïîñëåäîâàòåëüíîñòü ïåðå-
õîäîâ � � t t k1 � òàêàÿ, ÷òî M M M
t t tk
� � � �
1 2
1 � (M M� �
�
) .
Îáîçíà÷èì R N M( , ) ìíîæåñòâî ðàçìåòîê â ñåòè N , äîñòèæèìûõ èç ðàçìåòêè M.
Ìíîæåñòâî R N R N M( ) ( , )� 0 îçíà÷àåò ìíîæåñòâî äîñòèæèìûõ ðàçìåòîê ñåòè N èç
íà÷àëüíîé ðàçìåòêè M 0 . Î÷åâèäíî, ÷òî M R N M� ( , ) è M R N0 � ( ) .
Ïóñòü T * — ìíîæåñòâî âñåõ ïîñëåäîâàòåëüíîñòåé âîçìîæíûõ ïåðåõîäîâ â
ñåòè N , òîãäà ñâîáîäíûì ÿçûêîì ñåòè N íàçûâàþò ìíîæåñòâî L N T( ) |*� �{�
� � �M R N M M( ): 0
�
}, ò.å. ìíîæåñòâî âñåõ âîçìîæíûõ ïîñëåäîâàòåëüíîñòåé ñðà-
áàòûâàíèé ïåðåõîäîâ ñåòè N , íà÷èíàÿ ñ íà÷àëüíîé ðàçìåòêè.
Îïðåäåëåíèå 3. Ïîìå÷åííàÿ ñåòü Ïåòðè — ýòî ïàðà ( , )N � , ãäå N — ñåòü Ïåò-
ðè, à �: T A� — ïîìå÷àþùàÿ ôóíêöèÿ íàä íåêîòîðûì àëôàâèòîì A. Åñëè � —
÷àñòè÷íàÿ ôóíêöèÿ, òî ïåðåõîäû, íà êîòîðûõ îíà íå îïðåäåëåíà, ïîìå÷àþò ñïåöè-
àëüíûì ñèìâîëîì � è íàçûâàþò �-ïåðåõîäàìè.
32 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2009, ¹ 4
Ïîìå÷àþùàÿ ôóíêöèÿ åñòåñòâåííûì îáðàçîì ðàñøèðÿåòñÿ íà ïîñëåäîâàòåëü-
íîñòè ñðàáàòûâàíèé ïåðåõîäîâ:
�
� � �
�
( )
( ) ( ) ( )
( )
�
�
�
t
t t
�
, åñëè îïðåäåëåíî,
â ïðîòèâíîì ñëó àå,
�
�
�
ãäå t — ïåðåõîä è � — ïîñëåäîâàòåëüíîñòü ïåðåõîäîâ.
Îïðåäåëåíèå 4. Åñëè ��T * — ïîñëåäîâàòåëüíîñòü ñðàáàòûâàíèé ïåðåõîäîâ
ñåòè N , à ( , )N � — ïîìå÷åííàÿ ñåòü, òî �( ) *� � A íàçûâàþò ïîìå÷àþùåé ïîñëåäî-
âàòåëüíîñòüþ, ãäå A * — ìíîæåñòâî âñåõ ñëîâ â àëôàâèòå A. Åñëè L N( ) — ñâîáîä-
íûé ÿçûê ñåòè N , òî ìíîæåñòâî { }�( )| ( )� ��L N íàçûâàþò ïðåôèêñíûì ÿçûêîì ïî-
ìå÷åííîé ñåòè ( , )N � .
Ìåñòî p â ñåòè N íàçûâàþò îãðàíè÷åííûì, åñëè ñóùåñòâóåò n òàêîå, ÷òî
� �M R N M p n( ): ( ) . Ñåòü Ïåòðè N íàçûâàåòñÿ îãðàíè÷åííîé, åñëè âñå åå ìåñòà
îãðàíè÷åíû.  ñëó÷àå, åñëè n �1, òî ìåñòà ÑÏ íàçûâàþòñÿ áåçîïàñíûìè, à ñàìà
ñåòü — áåçîïàñíîé.
Ñåòü N íàçûâàåòñÿ êîíñåðâàòèâíîé, åñëè ñóììàðíîå ÷èñëî ôèøåê â ñåòè îñòà-
åòñÿ íåèçìåííûì ïðè ëþáûõ ñðàáàòûâàíèÿõ ïåðåõîäîâ, ò.å.
�M M R N
1 2
, ( ):
M p M p
p P p P
1 2( ) ( )
� �
� �� .
Ïåðåõîä t â ñåòè N íàçûâàåòñÿ ïîòåíöèàëüíî æèâûì ïðè ðàçìåòêå M, åñëè
� �� � �M R N M M F t( , ): ( )* . Åñëè M M� 0 , òî t â ñåòè N íàçûâàåòñÿ ïîòåíöèàëüíî
æèâûì. Ïåðåõîä t — ìåðòâûé ïðè ðàçìåòêå M, åñëè îí íå ÿâëÿåòñÿ ïîòåíöèàëüíî
æèâûì ïðè M. Ïåðåõîä t — ìåðòâûé, åñëè îí ìåðòâûé ïðè ëþáîé äîñòèæèìîé â
ñåòè ðàçìåòêå.
Ïåðåõîä t â ñåòè N íàçûâàåòñÿ æèâûì, åñëè
�M R N( ) � ��M R N M( , ):
M F t� �* ( ) . Ïåðåõîä t — ïîòåíöèàëüíî ìåðòâûé, åñëè � �
��M R N M R N M( ): ( , ):
M F t� ��* ( ) . Ðàçìåòêà M â ýòîì ñëó÷àå íàçûâàåòñÿ t-òóïèêîâîé. Åñëè ðàçìåòêà ÿâëÿ-
åòñÿ t-òóïèêîâîé äëÿ âñåõ ïåðåõîäîâ, åå íàçûâàþò òóïèêîâîé. Ñåòü íàçûâàåòñÿ
æèâîé, åñëè âñå åå ïåðåõîäû æèâûå.
1.1.1. Ïîêðûâàþùåå äåðåâî ÑÏ. Ïîêðûâàþùåå äåðåâî ÑÏ — ýòî êîíå÷íûé
îðèåíòèðîâàííûé àöèêëè÷åñêèé ãðàô, âåðøèíàìè êîòîðîãî ÿâëÿþòñÿ ðàçìåòêè ÑÏ,
äîñòèæèìûå èç íà÷àëüíîé ðàçìåòêè è óäîâëåòâîðÿþùèå îïðåäåëåííûì óñëîâèÿì.
Ýòè óñëîâèÿ ïðîâåðÿþòñÿ â ïðîöåññå ïîñòðîåíèÿ ïîêðûâàþùåãî äåðåâà è îïèñàíû
â âèäå ñëåäóþùåãî àëãîðèòìà.
1. Èçíà÷àëüíî äåðåâî ïîêðûòèÿ ñîñòîèò èç îäíîãî êîðíÿ, êîòîðûé ñîäåðæèò
ðàçìåòêó M 0 è íå èìååò äóã.
2. Ïóñòü M — âåðøèíà äåðåâà, åùå íå îáúÿâëåííàÿ ëèñòîì, èç êîòîðîé ïîêà íå
èñõîäèò íè îäíà äóãà. Äëÿ ðàçìåòêè M âîçìîæíû ñëåäóþùèå ñëó÷àè:
à) íà ïóòè èç êîðíÿ äåðåâà â âåðøèíó M óæå ñóùåñòâóåò âåðøèíà M� òàêàÿ,
÷òî M M� �.  ýòîì ñëó÷àå âåðøèíà M îáúÿâëÿåòñÿ ëèñòîì;
á) íà ïóòè èç êîðíÿ äåðåâà â âåðøèíó M ñóùåñòâóþò âåðøèíû � �M M n1 , ,� òà-
êèå, ÷òî � � �M M i ni , , ,1 � .  ýòîì ñëó÷àå â ðàçìåòêå M êàæäûé ýëåìåíò,
ñîîòâåòñòâóþùèé ìåñòó p, äëÿ êîòîðîãî � � �i M p M pi: ( ) ( ) , çàìåíÿåòñÿ íà
� è âåðøèíà îáúÿâëÿåòñÿ �-ëèñòîì;
â) ïðè ðàçìåòêå M íå ìîæåò ñðàáîòàòü íè îäèí èç ïåðåõîäîâ ñåòè, â ýòîì ñëó-
÷àå âåðøèíà M îáúÿâëÿåòñÿ ëèñòîì.
 îñòàëüíûõ ñëó÷àÿõ äëÿ êàæäîãî ïåðåõîäà t, êîòîðûé ìîæåò ñðàáîòàòü ïðè
ýòîé ðàçìåòêå, ñîçäàåòñÿ íîâàÿ âåðøèíà M� òàêàÿ, ÷òî M M
t
� �, è M ñîåäèíÿåòñÿ
ñ íåé äóãîé, ïîìå÷åííîé ñèìâîëîì t. Ïîêðûâàþùåå äåðåâî ïîçâîëÿåò èññëåäîâàòü
ñëåäóþùèå ñâîéñòâà ñåòè.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2009, ¹ 4 33
÷
1. Ñåòü ÿâëÿåòñÿ îãðàíè÷åííîé, åñëè åå ïîêðûâàþùåå äåðåâî íå ñîäåðæèò
�-ëèñòîâ.
2. Ñåòü ÿâëÿåòñÿ áåçîïàñíîé, åñëè âñå âåðøèíû â åå äåðåâå ïîêðûòèÿ ñîäåðæàò
ðàçìåòêè, ñîñòîÿùèå ëèøü èç íóëåé è åäèíèö.
3. Åñëè õîòÿ áû â îäíîé èç âåðøèí ïîêðûâàþùåãî äåðåâà ïîçèöèÿ â ðàçìåòêå,
ñîîòâåòñòâóþùàÿ ìåñòó p, ñîäåðæèò ÷èñëî, áîëüøåå íóëÿ, ìåñòî p ìîæåò ïîëó÷èòü
ôèøêó â ïðîöåññå ôóíêöèîíèðîâàíèÿ ñåòè.
4. Åñëè ñèìâîë ïåðåõîäà t ïîìå÷àåò õîòÿ áû îäíó äóãó ïîêðûâàþùåãî äåðåâà,
ïåðåõîä t ÿâëÿåòñÿ ïîòåíöèàëüíî æèâûì.
1.1.2. Óðàâíåíèå ñîñòîÿíèÿ ÑÏ è èíâàðèàíòû ÑÏ. Ïîïóëÿðíûì ìåòîäîì
àíàëèçà ñåòè ÿâëÿåòñÿ òàêæå ìåòîä âû÷èñëåíèÿ èíâàðèàíòîâ ÑÏ ïóòåì ðåøåíèÿ åå
óðàâíåíèÿ ñîñòîÿíèÿ.
Îïðåäåëåíèå 5. Óðàâíåíèåì ñîñòîÿíèÿ ÑÏ äëÿ ïðîèçâîëüíîé ðàçìåòêè M [10]
íàçûâàþò äèîôàíòîâî óðàâíåíèå âèäà Ax M M� �
0
, ãäå A ai j� | |, — ìàòðèöà èíöè-
äåíòíîñòè ýòîé ñåòè, a f t p f p ti j j i i j, ( , ) ( , )� � .
 [10] ïîêàçàíî, ÷òî åñëè íåêàÿ ðàçìåòêà M äîñòèæèìà èç íà÷àëüíîé, òî ñîîò-
âåòñòâóþùåå óðàâíåíèå ñîñòîÿíèÿ Ax M M� � 0 èìååò ðåøåíèå. Óòâåðæäåíèå
î òîì, ÷òî åñëè óðàâíåíèå ñîñòîÿíèÿ Ax M M� � 0 èìååò ðåøåíèå, òî ðàçìåòêà M
äîñòèæèìà èç íà÷àëüíîé, â îáùåì ñëó÷àå íåâåðíî, íî åñëè óðàâíåíèå ñîñòîÿíèÿ íå-
ñîâìåñòíî, òî ðàçìåòêà íå äîñòèæèìà èç íà÷àëüíîé.
Îïðåäåëåíèå 6. T-èíâàðèàíòàìè ÑÏ íàçûâàþòñÿ ïîëîæèòåëüíûå öåëî÷èñëåí-
íûå ðåøåíèÿ ñèñòåìû Ax � 0 ; S-èíâàðèàíòàìè — ïîëîæèòåëüíûå öåëî÷èñëåííûå
ðåøåíèÿ ñèñòåìû A xt � 0 , ãäå A t — òðàíñïîíèðîâàííàÿ ìàòðèöà èíöèäåíòíîñòè.
Âåêòîð x ÿâëÿåòñÿ T-èíâàðèàíòîì òîãäà è òîëüêî òîãäà, êîãäà ñóùåñòâóåò ðàç-
ìåòêà M 0 è ïîñëåäîâàòåëüíîñòü ïåðåõîäîâ �, âåäóùàÿ îò M 0 ê M 0 òàêàÿ, ÷òî � � x.
Ñëåäîâàòåëüíî, íåôîðìàëüíî T-èíâàðèàíòû ñîîòâåòñòâóþò ñîâîêóïíîñòè ñðàáàòû-
âàþùèõ ïåðåõîäîâ ÑÏ, ñîõðàíÿþùèõ ðàçìåòêó. Åñëè õîòÿ áû â îäíîì èç T-èíâàðè-
àíòîâ ïåðåõîäó ñîîòâåòñòâóåò íåíóëåâàÿ êîîðäèíàòà, ýòîò ïåðåõîä ÿâëÿåòñÿ
ïîòåíöèàëüíî æèâûì â èñõîäíîé ÑÏ.
Äëÿ ðåøåíèÿ óðàâíåíèÿ ñîñòîÿíèÿ ÑÏ (ïîñòðîåíèÿ ìíîæåñòâà åå èíâàðèàíòîâ)
ìîæåò áûòü èñïîëüçîâàí TSS-àëãîðèòì ïîñòðîåíèÿ óñå÷åííîãî ìíîæåñòâà ðåøåíèé
ñèñòåìû ëèíåéíûõ îäíîðîäíûõ äèîôàíòîâûõ óðàâíåíèé. Äàííûé àëãîðèòì ïîä-
ðîáíî îïèñàí è îáîñíîâàí â [11], à îñîáåííîñòè åãî ðåàëèçàöèè — â [12].
1.1.3. Óïðîùåíèå ÑÏ. Äëÿ óñêîðåíèÿ àíàëèçà ÑÏ åå íåîáõîäèìî (åñëè âîç-
ìîæíî) óïðîñòèòü, ò.å. ïîäâåðãíóòü ïðåîáðàçîâàíèÿì äëÿ ñîêðàùåíèÿ êîëè÷åñòâà
ìåñò, ïåðåõîäîâ èëè äóã ïðè ñîõðàíåíèè èññëåäóåìûõ ñâîéñòâ èñõîäíîé ñåòè.
 ÷àñòíîñòè, ïðåîáðàçîâàíèå, ïîêàçàííîå íà ðèñ.1,à ñîõðàíÿåò ÿçûê ñåòè, à ïîêà-
çàííûå íà ðèñ. 1,á–æ (ââåäåíû â [10]), ñîõðàíÿþò ñâîéñòâà æèâîñòè, îãðàíè÷åííî-
ñòè è áåçîïàñíîñòè.
1.2. Êðàòêèå ñâåäåíèÿ î ÿçûêå MSC. Ñòàíäàðò ÿçûêà MSC ïðèâåäåí â [1],
à åãî îïåðàöèîííàÿ ñåìàíòèêà — â ïðèëîæåíèè ê ñòàíäàðòó [13]. Íèæå ïðèâåäåíû
âûäåðæêè èç ñòàíäàðòà â îïðåäåëåííîì îáúåìå.
MSC — ýòî ÿçûê äëÿ îïèñàíèÿ âçàèìîäåéñòâèÿ ìåæäó íåçàâèñèìûìè ñóùíî-
ñòÿìè, êîòîðûå îáìåíèâàþòñÿ ñîîáùåíèÿìè. Îí èìååò êàê òåêñòîâîå, òàê è ãðàôè-
÷åñêîå ïðåäñòàâëåíèå, ÷òî äåëàåò åãî óäîáíûì è äëÿ ðó÷íîé, è äëÿ ìàøèííîé îáðà-
áîòêè. Âûïîëíåíèå äîêóìåíòà MSC ïðåäñòàâëÿåò ñîáîé ïîñëåäîâàòåëüíîñòü òàêèõ
ñîáûòèé, êàê ïîñûëêà èëè ïðèåì ñîîáùåíèÿ, âûïîëíåíèå äåéñòâèÿ è ò.ï. Òàêàÿ ïî-
ñëåäîâàòåëüíîñòü ñîáûòèé, ïðîèñõîäÿùèõ ïðè âûïîëíåíèè äèàãðàììû èëè äîêó-
ìåíòà MSC, íàçûâàåòñÿ òðàññîé. Ïîñêîëüêó ÿçûê MSC ñîäåðæèò èòåðàöèþ, òðàññû
ìîãóò áûòü è áåñêîíå÷íûìè. Êàæäàÿ òðàññà îïèñûâàåò îïðåäåëåííûé ñöåíàðèé ðà-
áîòû èñõîäíîé ñèñòåìû. Ìîæíî ãîâîðèòü î ñòàòè÷åñêè (èëè ñòðóêòóðíî) âîçìîæ-
íûõ òðàññàõ, êîòîðûå îïðåäåëÿþòñÿ òîëüêî ñòðóêòóðîé MSC, è äèíàìè÷åñêè âîç-
ìîæíûõ òðàññàõ, íà êîòîðûå îêàçûâàåò âëèÿíèå òàêæå è ñîñòîÿíèå ìîäåëèðóåìîé
34 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2009, ¹ 4
ñèñòåìû ÷åðåç çíà÷åíèÿ óñëîâèé. Ïîñêîëüêó ëþáàÿ äèíàìè÷åñêè âîçìîæíàÿ òðàññà
äîëæíà áûòü òàêæå è ñòàòè÷åñêè âîçìîæíîé, òî ìíîæåñòâî äèíàìè÷åñêèõ òðàññ
åñòü ïîäìíîæåñòâîì ìíîæåñòâà ñòàòè÷åñêèõ. Ïðèâåäåííûé â ñòàòüå àëãîðèòì
ðàññìàòðèâàåò òîëüêî ìíîæåñòâî ñòàòè÷åñêè âîçìîæíûõ òðàññ, ò.å. ñòðóêòóðíûå
ñâîéñòâà äîêóìåíòà MSC.
×àñòî èñïîëüçóåìûå ýëåìåíòû ÿçûêà MSC îïèñàíû íèæå (ãðàôè÷åñêèé âàðè-
àíò). Ïîëíûé ñïèñîê ýëåìåíòîâ MSC è èõ òåêñòîâîé âàðèàíò ïðèâåäåíû â [1].
Äîêóìåíò MSC (MSC document) (ðèñ. 2, à), ÿâëÿþùèéñÿ íàèáîëåå êðóïíûì
îáúåêòîì MSC, îïèñûâàåò ïîâåäåíèå ñèñòåìû â öåëîì. Îí îïðåäåëÿåò ïðèñóòñòâó-
þùèå â ñèñòåìå ñóùíîñòè è âêëþ÷àåò â ñåáÿ äèàãðàììû MSC è HMSC (High-level
Message Sequence Chart).
Äèàãðàììà MSC (MSC diagram) (ðèñ. 2, â) îïèñûâàåò íåêîòîðûé ôðàãìåíò ïî-
âåäåíèÿ ñèñòåìû è ïðåäñòàâëÿåò ñîáîé ñöåíàðèé âçàèìîäåéñòâèÿ ìåæäó ñóùíîñòÿ-
ìè (ñì. íèæå). Íå ñóùåñòâóåò êàêèõ-ëèáî ïðàâèë îòíîñèòåëüíî òîãî, ÷òî â äàííîì
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2009, ¹ 4 35
Ðèñ. 1. Òèïû óïðîùåíèÿ ÑÏ
a
á â
ã ä
å æ
Óäàëèòü ëèøíåå ìåñòî
Óäàëèòü ïðîìåæóòî÷íûé
ïåðåõîä
Óäàëèòü ïðîìåæóòî÷íîå
ìåñòî
Ñêëåéêà ìåñò Ñêëåéêà ïåðåõîäîâ
Óäàëèòü ýëåìåíòàðíûé öèêë-ìåñòî
Óäàëèòü ýëåìåíòàðíûé öèêë-ïåðåõîä
ñëó÷àå ñ÷èòàòü ôðàãìåíòîì ïîâåäåíèÿ, ïîýòîìó ðàçáèåíèå èñõîäíîé ñèñòåìû íà
äèàãðàììû MSC âûïîëíÿåòñÿ ðàçðàáîò÷èêîì, èñõîäÿ èç óäîáñòâà ðàáîòû. Íàçâà-
íèå «äèàãðàììà MSC» çàïèøåì ïðîñòî êàê MSC. Äèàãðàììà îäíîçíà÷íî îïðåäåëÿ-
åòñÿ â ïðåäåëàõ äîêóìåíòà ñâîèì èìåíåì.
Ñóùíîñòü (instance), îáîçíà÷åííàÿ êàê (4) íà ðèñ. 2, ïðåäñòàâëÿåò àãåíòà âçàè-
ìîäåéñòâèÿ â äîêóìåíòå MSC. Âçàèìîäåéñòâèå ìåæäó ñóùíîñòÿìè îïèñûâàåòñÿ â
äèàãðàììàõ MSC, íî ñàìè ñóùíîñòè îïðåäåëÿþòñÿ íà óðîâíå äîêóìåíòà MSC. Îíè
ñ÷èòàþòñÿ äåéñòâóþùèìè íåçàâèñèìî è èìåþùèìè íåçàâèñèìîå äèñêðåòíîå âðå-
ìÿ, ïðè ýòîì ñóùíîñòü ìîæåò ñóùåñòâîâàòü êàê íà ïðîòÿæåíèè âñåãî âðåìåíè äåé-
ñòâèÿ äîêóìåíòà, òàê è äèíàìè÷åñêè ñîçäàâàòüñÿ è óíè÷òîæàòüñÿ (ñì. íèæå). Ñóù-
íîñòü îäíîçíà÷íî îïðåäåëÿåòñÿ â ïðåäåëàõ äîêóìåíòà ñâîèì èìåíåì, à òàêæå ñâîèì
ýêçåìïëÿðîì, åñëè îí èñïîëüçóåòñÿ. Ýêçåìïëÿðû ñóùíîñòåé (ðàâíî êàê è ñîîáùå-
íèé) èñïîëüçóþò äëÿ òîãî, ÷òîáû ïðåäñòàâèòü íåñêîëüêî àãåíòîâ ñ îäèíàêîâûì
èìåíåì. Ñ ñóùíîñòüþ ñâÿçûâàåòñÿ åå îñü (instance line), íà êîòîðîé ðàñïîëàãàþòñÿ
ñâÿçàííûå ñ ýòîé ñóùíîñòüþ (ðàçäåëÿåìûå ýòîé ñóùíîñòüþ) ñîáûòèÿ è äðóãèå
ýëåìåíòû MSC.
Ñîîáùåíèå (message) (ðèñ. 2, (6)) — îñíîâíîé ñïîñîá âçàèìîäåéñòâèÿ ìåæäó
ñóùíîñòÿìè. Ñîîáùåíèå èìååò èìÿ, à òàêæå ìîæåò èìåòü èìÿ ýêçåìïëÿðà (instance)
(÷òîáû ðàçëè÷àòü ñîîáùåíèÿ ñ îäèíàêîâûì èìåíåì) è ïðèêðåïëåííûå äàííûå. Ñîîá-
ùåíèå ïðåäñòàâëÿåòñÿ äâóìÿ ñîáûòèÿìè: ïîñûëêîé ñîîáùåíèÿ è ïðèåìîì ñîîáùåíèÿ,
ïðè÷åì ïðèåì ñîîáùåíèÿ ïðîèñõîäèò ñòðîãî ïîñëå åãî ïîñûëêè. Åñëè ñîîáùåíèå ñî-
ñòîèò òîëüêî èç ïðèåìà èëè òîëüêî èç ïîñûëêè, îíî íàçûâàåòñÿ íåïîëíûì (incomplete).
Ïîñûë ñîîáùåíèé ìîæåò ïðîèñõîäèòü êàê ìåæäó ñóùíîñòÿìè â ïðåäåëàõ îäíîé äèà-
ãðàììû (ðèñ. 2, ñîîáùåíèÿ m1, m2), òàê è ìåæäó ðàçíûìè äèàãðàììàìè ñ ïîìîùüþ
øëþçîâ (ðèñ. 2, ñîîáùåíèå m3).  ïðåäåëàõ äèàãðàììû MSC ñîîáùåíèå îäíîçíà÷íî
îïðåäåëÿåòñÿ ñâîèì èìåíåì, ýêçåìïëÿðîì, ïðèåìíûì è ïåðåäàþùèì àäðåñàìè. Àäðåñ
ìîæåò áûòü èìåíåì ñóùíîñòè, øëþçà èëè óêàçûâàòü íà íåïîëíîòó ñîîáùåíèÿ.
Øëþç (gate) (ðèñ. 2, (7)) èñïîëüçóåòñÿ äëÿ îáìåíà ñîîáùåíèÿìè ìåæäó äèà-
ãðàììàìè MSC èëè äëÿ óñòàíîâêè ÿâíîãî ïîðÿäêà ìåæäó ýëåìåíòàìè, íàõîäÿùè-
ìèñÿ â ðàçíûõ äèàãðàììàõ MSC.
36 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2009, ¹ 4
Ðèñ. 2. Ýëåìåíòû ÿçûêà MSC
a
á â
Óñëîâèå (condition) (ðèñ. 2, (5)) èñïîëüçóåòñÿ äëÿ îãðàíè÷åíèÿ ìíîæåñòâà äî-
ïóñòèìûõ òðàññ. Óñëîâèÿ áûâàþò äâóõ òèïîâ — óñòàíîâî÷íûå (setting conditions) è
îãðàæäàþùèå (guarding conditions). Ïåðâûå ôèêñèðóþò íåêîòîðîå ãëîáàëüíîå ñî-
ñòîÿíèå ñèñòåìû íà ìîìåíò ñâîåãî âûïîëíåíèÿ, à âòîðûå ðåãóëèðóþò âîçìîæíîñòü
âûïîëíåíèÿ òðàññ â çàâèñèìîñòè îò ñîñòîÿíèÿ ñèñòåìû. Ñëåäóåò çàìåòèòü, ÷òî
ÿçûê, íà êîòîðîì çàïèñûâàåòñÿ ñîñòîÿíèå ñèñòåìû äëÿ óñëîâèé, íå îïðåäåëåí è âû-
áèðàåòñÿ ðàçðàáîò÷èêàìè. Ñâîéñòâîì óñëîâèé ÿâëÿåòñÿ òàêæå èõ ñèíõðîíèçèðóþ-
ùåå äåéñòâèå: åñëè äâå ñóùíîñòè ðàçäåëÿþò îäíî óñëîâèå, òî ëþáîå ñîîáùåíèå
ìåæäó íèìè, ïîñûëàåìîå äî ýòîãî óñëîâèÿ, äîëæíî áûòü ïðèíÿòî òàêæå äî óñëî-
âèÿ. Íàïðèìåð, ñîîáùåíèå m1 íà ðèñ. 2 ïîñûëàåòñÿ è ïðèíèìàåòñÿ äî óñëîâèÿ A.
Ñîçäàíèå ñóùíîñòè (instance creation) (ðèñ. 2, (10)) ÿâëÿåòñÿ ñïåöèàëüíûì âà-
ðèàíòîì ñîîáùåíèÿ, â ðåçóëüòàòå ïîñûëêè êîòîðîãî ñîçäàåòñÿ íîâàÿ ñóùíîñòü.
Óäàëåíèå ñóùíîñòè (instance stop) (ðèñ. 2, (11)) îñòàíàâëèâàåò åå âûïîëíåíèå.
Íèêàêîå ñîáûòèå, ðàçäåëÿþùåå ñóùíîñòü, íå ìîæåò áûòü âûïîëíåíî ïîñëå åå
óäàëåíèÿ.
Äåéñòâèå (action) (ðèñ. 2, (12)) — ñîáûòèå, ñâÿçàííîå ñ âûïîëíåíèåì êàêî-
ãî-ëèáî ïðîãðàììíîãî äåéñòâèÿ. Ñîäåðæèìîå äåéñòâèÿ çàäàåòñÿ ðàçðàáîò÷èêîì
â ïðîèçâîëüíîé ôîðìå.
Îáëàñòü ïðîèçâîëüíîãî âûïîëíåíèÿ (coregion) (ðèñ. 2, (13)) îòìå÷àåò íà îñè
ñóùíîñòè îòðåçîê, â ïðåäåëàõ êîòîðîãî ñîáûòèÿ âûïîëíÿþòñÿ â ïðîèçâîëüíîì ïî-
ðÿäêå (äåéñòâèå B è ïðèåì ñîîáùåíèÿ m11 íà ðèñ. 2). Â ïðèëîæåíèè ê ñòàíäàðòó
[13] ðåêîìåíäóåòñÿ èíòåðïðåòèðîâàòü îáëàñòü ïðîèçâîëüíîãî âûïîëíåíèÿ êàê ïà-
ðàëëåëüíóþ êîìïîçèöèþ âñåõ íàõîäÿùèõñÿ â íåé ñîáûòèé.
Ïîñëåäîâàòåëüíîñòü ñîáûòèé â äèàãðàììå MSC îïðåäåëÿåòñÿ èõ ÿâíûì è íå-
ÿâíûì óïîðÿäî÷åíèåì.
Íåÿâíîå óïîðÿäî÷åíèå (implicit ordering), îïðåäåëÿþùåå ïîðÿäîê âûïîëíåíèÿ
ñîáûòèé â ïðåäåëàõ äèàãðàììû, âûïîëíÿåòñÿ ñîãëàñíî ñëåäóþùèì ïðàâèëàì:
— åñëè äâà ñîáûòèÿ ðàçäåëÿþò îäíó è òó æå ñóùíîñòü è íå íàõîäÿòñÿ â îäíîé
îáëàñòè ïðîèçâîëüíîãî âûïîëíåíèÿ, âåðõíåå ñîáûòèå íàñòóïàåò ñòðîãî ðàíüøå
íèæíåãî;
— ïðèåì ñîîáùåíèÿ ïðîèñõîäèò ñòðîãî ïîçæå åãî ïîñûëêè;
— ñîçäàíèå ñóùíîñòè ïðîèñõîäèò ñòðîãî ïîçæå ñîáûòèÿ «ñîçäàòü ñóùíîñòü».
ßâíîå óïîðÿäî÷åíèå (explicit ordering) ïîçâîëÿåò óïîðÿäî÷èòü ñîáûòèÿ äèà-
ãðàììû MSC â äîïîëíåíèå ê îïèñàíîìó âûøå íåÿâíîìó óïîðÿäî÷åíèþ (implicit
ordering) è èçîáðàæàåòñÿ ïóíêòèðíîé ñòðåëêîé, âåäóùåé îò ïðåäøåñòâóþùåãî ñî-
áûòèÿ íåïîñðåäñòâåííî ê ïîñëåäóþùåìó (íà ðèñóíêå îòñóòñòâóåò).
Ññûëêà íà äèàãðàììó MSC (MSC reference) — êîíñòðóêöèÿ, ïîçâîëÿþùàÿ
ññûëàòüñÿ îäíîé äèàãðàììå MSC èëè HMSC íà äðóãóþ äèàãðàììó. Ïðè ýòîì
óïðàâëåíèå ïåðåäàåòñÿ äèàãðàììå, íà êîòîðóþ ññûëàþòñÿ, è âîçâðàùàåòñÿ ïî îêîí-
÷àíèè âûïîëíåíèÿ ýòîé äèàãðàììû. Ñïèñîê ñóùíîñòåé, ðàçäåëÿåìûõ ññûëêîé íà
MSC, äîëæåí ñîâïàäàòü ñî ñïèñêîì ñóùíîñòåé, ïðèñóòñòâóþùèõ â äèàãðàììå, íà
êîòîðóþ ññûëàþòñÿ (ðèñ. 2, (8)). Èç ññûëîê íà äèàãðàììû MSC ìîãóò ñîñòàâëÿòüñÿ
ññûëî÷íûå âûðàæåíèÿ.
Ññûëî÷íîå âûðàæåíèå (reference expression) — âûðàæåíèå íàä ññûëêàìè íà
MSC, ïîëó÷åííîå ñ ïîìîùüþ îïåðàòîðîâ alt, par, seq, loop, opt è exc. Ðàçìåùåíèå è
èñïîëüçîâàíèå ññûëî÷íûõ âûðàæåíèé ñîâïàäàþò ñ òàêîâûìè äëÿ ññûëîê íà MSC
(ðèñ. 2, (9)). Ññûëêó íà MSC ìîæíî ðàññìàòðèâàòü êàê ýëåìåíòàðíîå ññûëî÷íîå
âûðàæåíèå. Îïåðàòîðû â ññûëî÷íîì âûðàæåíèè ñîãëàñíî ñòàíäàðòó èìåþò
ñëåäóþùåå çíà÷åíèå:
• alt — àëüòåðíàòèâíîå âûïîëíåíèå, âûïîëíÿåòñÿ òîëüêî îäèí îïåðàíä;
• par — ïàðàëëåëüíîå âûïîëíåíèå, îïåðàíäû âûïîëíÿþòñÿ ïàðàëëåëüíî, â òå-
êóùåé ñåìàíòèêå ìîæíî ðàññìàòðèâàòü êàê ïðîèçâîëüíîå ÷åðåäîâàíèå ñîáûòèé èç
ðàçíûõ îïåðàíäîâ;
• seq — ïîñëåäîâàòåëüíîå âûïîëíåíèå, îïåðàíäû âûïîëíÿþòñÿ ïîñëåäîâàòåëüíî;
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2009, ¹ 4 37
• loop — èòåðàöèÿ, îïåðàíä âûïîëíÿåòñÿ íåñêîëüêî ðàç, â òåêóùåé ñåìàíòèêå
èòåðàöèÿ ðàññìàòðèâàåòñÿ êàê ïîñëåäîâàòåëüíîå âûïîëíåíèå íåñêîëüêèõ
ýêçåìïëÿðîâ îïåðàíäà;
• opt — íåîáÿçàòåëüíîå (îïöèîíàëüíîå) âûïîëíåíèå, îïåðàíä âûïîëíÿåòñÿ èëè
ïðîïóñêàåòñÿ, ÿâëÿåòñÿ ìîäèôèêàöèåé îïåðàòîðà alt, äëÿ êîòîðîé âòîðîé îïåðàíä
ïóñòîé;
• exc — èñêëþ÷åíèå, âûïîëíÿåòñÿ ëèáî îïåðàíä, ëèáî îñòàâøàÿñÿ ÷àñòü äèà-
ãðàììû, ÿâëÿåòñÿ ìîäèôèêàöèåé îïåðàòîðà alt, äëÿ êîòîðîé âòîðîé îïåðàíä ïðåä-
ñòàâëÿåò îñòàâøóþñÿ ÷àñòü äèàãðàììû.
Êðîìå ýòèõ îïåðàòîðîâ â ññûëî÷íîì âûðàæåíèè èñïîëüçóåòñÿ ñëîâî empty, êî-
òîðîå ðàññìàòðèâàåòñÿ êàê ññûëêà íà ïóñòóþ äèàãðàììó.
Âñòðîåííîå âûðàæåíèå (inline expression) àíàëîãè÷íî ññûëî÷íîìó, íî âìåñòî
ññûëîê íà äèàãðàììû â âûðàæåíèå âêëþ÷àþòñÿ íåïîñðåäñòâåííî èõ òåëà (òàêèì
îáðàçîì, âñòðîåííîå âûðàæåíèå ìîæíî ðàññìàòðèâàòü êàê ññûëî÷íîå âûðàæåíèå
íàä àíîíèìíûìè MSC) (ðèñ. 2, (14)). Ïðè ïîñòðîåíèè âñòðîåííûõ âûðàæåíèé èñ-
ïîëüçóþòñÿ òå æå îïåðàòîðû, ÷òî è â ññûëî÷íûõ âûðàæåíèÿõ.
Äèàãðàììà HMSC (âûñîêîóðîâíåâàÿ MSC, HMSC) (ðèñ. 2, á) îïèñûâàåò âçàè-
ìîäåéñòâèå îòäåëüíûõ äèàãðàìì MSC â ðàìêàõ äîêóìåíòà MSC. Îíà ïðåäñòàâëÿåò
ñîáîé îðèåíòèðîâàííûé ãðàô (íàïðàâëåíèå ðåáåð, èäóùèõ ñâåðõó âíèç, îáû÷íî
ñòðåëêàìè íå îáîçíà÷àåòñÿ). Òèïû âåðøèí HMSC:
• ñòàðò (start, start symbol) — òî÷êà íà÷àëà âûïîëíåíèÿ äîêóìåíòà; â êàæäîé
äèàãðàììå HMSC åñòü ðîâíî îäíà òàêàÿ âåðøèíà (ðèñ. 2, (15));
• ñòîï (end, end symbol) — òî÷êà çàâåðøåíèÿ âûïîëíåíèÿ äîêóìåíòà (ðèñ. 2, (20));
• ññûëî÷íîå âûðàæåíèå (àíàëîãè÷íî èñïîëüçóåìîìó â MSC, ðèñ. 2, (16));
• óñëîâèå (àíàëîãè÷íî èñïîëüçóåìîìó â MSC);
• òî÷êà ñîåäèíåíèÿ (conneñtion point) — â çàâèñèìîñòè îò íàïðàâëåíèÿ ðåáåð
îáðàçóåò êîìïîçèöèþ àëüòåðíàòèâíîãî âûïîëíåíèÿ (ðèñ. 2, (17)) ëèáî òî÷êó îáú-
åäèíåíèÿ ðàçíûõ âåòâåé àëüòåðíàòèâíîãî âûïîëíåíèÿ (ðèñ. 2, (18));
• ïàðàëëåëüíîå âûïîëíåíèå (parallel frame) — êîíñòðóêöèÿ, ñîäåðæàùàÿ íå-
ñêîëüêî HMSC, êîòîðûå âûïîëíÿþòñÿ ïàðàëëåëüíî (ðèñ. 2, (19)).
2. ÀËÃÎÐÈÒÌ ÏÐÅÎÁÐÀÇÎÂÀÍÈß MSC-ÄÈÀÃÐÀÌÌ Â ÑÏ
Àëãîðèòì îñíîâàí íà ñëåäóþùèõ ñîîáðàæåíèÿõ. Ñîãëàñíî ñåìàíòèêå MSC ([13] ñ
ó÷åòîì ðàñøèðåíèÿ, ïðèâåäåííîãî â [5]) äîêóìåíò MSC ìîæíî ðàññìàòðèâàòü êàê
ìíîæåñòâî ñîáûòèé, ñîåäèíåííûõ ïîñëåäîâàòåëüíîé, ïàðàëëåëüíîé, àëüòåðíàòèâíîé
êîìïîçèöèÿìè. Òèï èñïîëüçóåìîé êîìïîçèöèè îïðåäåëÿåòñÿ óïðàâëÿþùèìè êîí-
ñòðóêöèÿìè MSC. Òàêèì îáðàçîì, àëãîðèòì êîíâåðòàöèè MSC-äèàãðàìì â ÑÏ ñî-
ñòîèò â ñèìóëÿöèè ýòèõ óïðàâëÿþùèõ êîíñòðóêöèé ñ ïîìîùüþ ÑÏ. Â ðåçóëüòàòå
ïîëó÷åíà ÑÏ, êîòîðàÿ ãåíåðèðóåò ÿçûê, ÿâëÿþùèéñÿ ñîáûòèéíî ýêâèâàëåíòíûì
ìíîæåñòâó òðàññ, ãåíåðèðóåìûõ èñõîäíûì äîêóìåíòîì MSC.
2.1. Îáîçíà÷åíèÿ è íà÷àëüíûå äîïóùåíèÿ. Ïðåäïîëîæèì, ÷òî âõîäíîé äî-
êóìåíò MSC ÿâëÿåòñÿ ñèíòàêñè÷åñêè âåðíûì è óäîâëåòâîðÿåò ñòàòè÷åñêèì òðåáî-
âàíèÿì, óêàçàííûì â [1]. Òåëà âñòðîåííûõ âûðàæåíèé ðàññìàòðèâàþòñÿ êàê àíî-
íèìíûå äèàãðàììû MSC (â ñîîòâåòñòâèè ñ [13]). Ñîãëàñíî ñòàòè÷åñêèì òðåáîâàíè-
ÿì [1] ïðåäïîëîæèì, ÷òî âñå ñîáûòèÿ äîêóìåíòà MSC óíèêàëüíû (ïðè
íåîáõîäèìîñòè ýòîãî ìîæíî äîñòè÷ü ñîîòâåòñòâóþùèì ïåðåèìåíîâàíèåì
ñîáûòèé).
 îòëè÷èå îò ïîäõîäà â [13] ìû èíòåðïðåòèðóåì îïåðàòîð seq êàê ñòðîãóþ ïî-
ñëåäîâàòåëüíóþ êîìïîçèöèþ äèàãðàìì MSC (ò.å. åñëè äâå äèàãðàììû MSC ñîåäè-
íåíû ïîñëåäîâàòåëüíî, òî âñå ñîáûòèÿ ïåðâîé äèàãðàììû áóäóò âûïîëíåíû äî
òîãî, êàê íà÷íåò âûïîëíÿòüñÿ ïåðâîå ñîáûòèå âòîðîé äèàãðàììû). Ïîëó÷åííàÿ â
ðåçóëüòàòå âûïîëíåíèÿ ïðåäñòàâëåííîãî àëãîðèòìà ÑÏ ïðåäñòàâëÿåò òîëüêî ñòðóê-
òóðó è ñòàòè÷åñêèå ñâîéñòâà äîêóìåíòà MSC. Òàêèì îáðàçîì, èíôîðìàöèÿ,
ñîäåðæàùàÿñÿ â ýëåìåíòàõ òèïà óñëîâèå, èãíîðèðóåòñÿ.
38 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2009, ¹ 4
Ïðè îïèñàíèè àëãîðèòìà è åãî äî-
êàçàòåëüñòâå èñïîëüçóþòñÿ ñëåäóþùèå
îáîçíà÷åíèÿ:
1) ñîáûòèÿ MSC (âêëþ÷àÿ ýëåìåíò
òèïà óñëîâèå), êàê è ñîîòâåòñòâóþùèå
èì ôðàãìåíòû ÑÏ, îáîçíà÷àåì e i� ;
2) ïîñëåäîâàòåëüíîñòè è íåóïîðÿ-
äî÷åííûå ãðóïïû ñîáûòèé MSC, êàê è
ñîîòâåòñòâóþùèå èì ôðàãìåíòû ÑÏ,
îáîçíà÷àåì se i� ;
3) ôðàãìåíòû ÑÏ, èñïîëüçóåìûå äëÿ
ïðåäñòàâëåíèÿ óïðàâëÿþùèõ êîíñòðóê-
öèé MSC, íàçûâàåì êîíñòðóêöèÿìè;
4) â ïîëó÷åííîé ÑÏ ìåòêè ïåðåõîäîâ áóäóò ðàçìåùàòüñÿ ðÿäîì ñî çíàêîì ïå-
ðåõîäà, â òî âðåìÿ êàê äîïîëíèòåëüíàÿ ñëóæåáíàÿ èíôîðìàöèÿ áóäåò ïîìåùàòüñÿ
âíóòðè çíà÷êîâ ïåðåõîäà èëè ìåñòà;
5) L ap ( ) — ïðåôèêñíûé ÿçûê ðàçìå÷åííîé ñåòè a, êîòîðûé íàçîâåì ÿçûêîì
ÑÏ [9];
6) �( )b — ìíîæåñòâî òðàññ, ãåíåðèðóåìûõ äîêóìåíòîì MSC b.
 îïèñàíèè àëãîðèòìà èñïîëüçóåòñÿ èçëîæåííîå íèæå ïîíÿòèå ñîáûòèéíîé ýê-
âèâàëåíòíîñòè.
Ðàññìîòðèì ñõåìó îòíîøåíèé ýêâèâàëåíòíîñòè, èñïîëüçóåìûõ â àëãîðèòìå
(ðèñ. 3).
• Îòíîøåíèå ýêâèâàëåíòíîñòè R1 èíäóöèðóåòñÿ ôóíêöèåé � è îïðåäåëåíî íà
ìíîæåñòâå äîêóìåíòîâ MSC: pR q p q1 � �� �( ) ( ) . Îòíîøåíèå R1 îáúåäèíÿåò â
îäèí êëàññ ýêâèâàëåíòíîñòè äîêóìåíòû MSC, ãåíåðèðóþùèå îäèíàêîâûå
ìíîæåñòâà òðàññ.
• Îòíîøåíèå ýêâèâàëåíòíîñòè R2 èíäóöèðóåòñÿ ôóíêöèåé L
p
è îïðåäåëåíî íà
ìíîæåñòâå ñåòåé Ïåòðè: pR q L p L q
p p
2 � �( ) ( ) . Îòíîøåíèå R2 îáúåäèíÿåò â îäèí
êëàññ ýêâèâàëåíòíîñòè ñåòè Ïåòðè, èìåþùèå îäèíàêîâûé ïðåôèêñíûé ÿçûê.
• Îòíîøåíèå R3 óñòàíàâëèâàåò âçàèìíî îäíîçíà÷íîå ñîîòâåòñòâèå ìåæäó ìíî-
æåñòâàìè òðàññ äîêóìåíòîâ MSC è ïðåôèêñíûìè ÿçûêàìè ñåòåé Ïåòðè, ïîñòðîåí-
íûõ ñ ïîìîùüþ ðàññìàòðèâàåìîãî àëãîðèòìà. Îòíîøåíèå R3 îïðåäåëåíî êàê
pR q w p w q w r w w q w p w r w3 1 2 1 2 2 1 1 2�
� � � � �
� � � �( : ( )) ( : ( )) , ãäå r w( )
— ôóíêöèÿ ïåðåèìåíîâàíèÿ.
Îïðåäåëåíèå 7. Äîêóìåíò MSC a è ñåòü Ïåòðè b ñîáûòèéíî ýêâèâàëåíòíû,
åñëè âûïîëíÿåòñÿ óñëîâèå �( ) ( )a R L bp
3
.
2.2. Îïèñàíèå àëãîðèòìà. Ïîñòðîåíèå ÑÏ èç èñõîäíîãî äîêóìåíòà MSC
âêëþ÷àåò ñëåäóþùèå øàãè.
1. Êàæäàÿ äèàãðàììà MSC (âêëþ÷àÿ àíîíèìíûå äèàãðàììû, íàõîäÿùèåñÿ â òå-
ëàõ âñòðîåííûõ âûðàæåíèé) ïåðåâîäèòñÿ â êîíñòðóêöèþ, ïîêàçàííóþ íà ðèñ. 4,à,
ãäå se se n� �1 , ,� — ïîñëåäîâàòåëüíîñòè ñîáûòèé è êîíñòðóêöèé, ïðèíàäëåæàùèõ
ýòîé äèàãðàììå. Åñëè äîêóìåíò MSC ñîäåðæèò íåñêîëüêî ññûëîê íà îäíó è òó æå
äèàãðàììó, òî êàæäàÿ èç íèõ ðàññìàòðèâàåòñÿ â îòäåëüíîñòè, à ïðè íåîáõîäèìîñòè
ñîçäàåòñÿ íåñêîëüêî åå êîïèé.
2. Äëÿ êàæäîãî ñîáûòèÿ MSC e i� ñòðîèòñÿ Pre e i� �( ) — ìíîæåñòâî ñîáûòèé è
êîíñòðóêöèé (âêëþ÷àÿ ïðîïóùåííûå ñêâîçü øëþçû), êîòîðûå íåïîñðåäñòâåííî
ïðåäøåñòâóþò äàííîìó ñîáûòèþ (àëãîðèòì ïîñòðîåíèÿ ìíîæåñòâà Pre e i� �( ) ïðè-
âåäåí íèæå). Çàòåì e i� ïåðåâîäèòñÿ â êîíñòðóêöèþ, ïîêàçàííóþ íà ðèñ. 4,á, ãäå
n Pre e i�| ( )|� � , è âõîäíûå ìåñòà p pn1 , ,� ñîåäèíÿþòñÿ ñ ñîîòâåòñòâóþùèìè ñî-
áûòèÿìè è êîíñòðóêöèÿìè èç Pre e i� �( ) .
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2009, ¹ 4 39
Ðèñ. 3. Ñõåìà îòíîøåíèÿ ýêâèâàëåíòíîñòè äîêó-
ìåíòîâ MSC è ñåòåé Ïåòðè
Lp
�
3. Ïàðàëëåëüíàÿ êîìïîçèöèÿ äèàãðàìì MSC (ïðåäñòàâëåíà êîíñòðóêöèåé par
â ññûëî÷íîì ëèáî âñòðîåííîì âûðàæåíèè MSC èëè êîíñòðóêöèåé parallel frame
â HMSC) ïåðåâîäèòñÿ â êîíñòðóêöèþ, ïîêàçàííóþ íà ðèñ. 4,â, ãäå n — êîëè÷åñòâî
àëüòåðíàòèâ â êîìïîçèöèè.
4. Àëüòåðíàòèâíàÿ êîìïîçèöèÿ äèàãðàìì MSC (ïðåäñòàâëåíà êîíñòðóêöèÿìè
alt, opt, exc â ññûëî÷íîì ëèáî âñòðîåííîì âûðàæåíèè MSC èëè ðàñùåïëåíèåì ëè-
íèè â HMSC) ïåðåâîäèòñÿ â êîíñòðóêöèþ, ïîêàçàííóþ íà ðèñ. 4,ã, ãäå n — êîëè÷å-
ñòâî àëüòåðíàòèâ â êîìïîçèöèè.
5. Ïîñëåäîâàòåëüíàÿ êîìïîçèöèÿ äèàãðàìì MSC (ïðåäñòàâëåíà êîíñòðóêöèåé
seq â ññûëî÷íîì âûðàæåíèè MSC èëè ëèíèåé â HMSC) ïåðåâîäèòñÿ â êîíñòðóê-
öèþ, ïîêàçàííóþ íà ðèñ. 4,ä.
6. Èòåðàöèÿ äèàãðàììû MSC (ïðåäñòàâëåíà êîíñòðóêöèåé loop â ññûëî÷íîì
èëè âñòðîåííîì âûðàæåíèè MSC) ðàññìàòðèâàåòñÿ êàê âàðèàíò àëüòåðíàòèâíîé
êîìïîçèöèè è ïåðåâîäèòñÿ â êîíñòðóêöèþ, ïîêàçàííóþ íà ðèñ. 4,å.
7. Ïîñëåäíèå ýëåìåíòû è êîíñòðóêöèè äèàãðàììû MSC (êðîìå ñîáûòèÿ stop)
ñîåäèíÿþòñÿ ñ ñîîòâåòñòâóþùåé êîíñòðóêöèåé msc_out.
8. Ïîñëåäíèå ýëåìåíòû è êîíñòðóêöèè áëîêîâ, ñâÿçàííûõ ñ ññûëî÷íûìè èëè
âñòðîåííûìè âûðàæåíèÿìè (êðîìå ñîáûòèÿ stop) ñîåäèíÿþòñÿ ñ ñîîòâåòñòâóþùåé
êîíñòðóêöèåé _out.
9. Ýëåìåíò HMSC start ïåðåâîäèòñÿ â êîíñòðóêöèþ, ïîêàçàííóþ íà ðèñ. 4,æ,
ýëåìåíò HMSC stop ïåðåâîäèòñÿ â êîíñòðóêöèþ, ïîêàçàííóþ íà ðèñ. 4,ç.
10. Ýëåìåíò MSC coregion ðàññìàòðèâàåòñÿ êàê ïàðàëëåëüíàÿ êîìïîçèöèÿ
(â ñîîòâåòñòâèè ñ [13]) è ïåðåâîäèòñÿ â êîíñòðóêöèþ, ïîêàçàííóþ íà ðèñ. 4,è.
2.3. Ïîñòðîåíèå ìíîæåñòâà Pre e i� �( ) . Äëÿ êàæäîãî ñîáûòèÿ e i� ñòðîèòñÿ
ìíîæåñòâî Pre e i� �( ) , êîòîðîå ñîñòîèò èç ñëåäóþùèõ ñîáûòèé è êîíñòðóêöèé.
1. Ñîáûòèÿ, èìåþùèå îáùóþ ñ e i� ñóùíîñòü è ðàñïîëîæåííûå íåïîñðåäñòâåí-
íî ïåðåä e i� ïî ýòîé ñóùíîñòè.
2 Êîíñòðóêöèÿ msc_in ýòîé äèàãðàììû, åñëè e i� íàõîäèòñÿ â íà÷àëå äèàãðàì-
ìû è íå ÿâëÿåòñÿ ñîáûòèåì òèïà create in.
3. Ñîáûòèå message out, create out, call out èëè reply out, åñëè e i� ïðèíàäëåæèò
òèïàì message in, create in, call in èëè reply in ñîîòâåòñòâåííî.
40 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2009, ¹ 4
i
Ðèñ. 4. Ôðàãìåíòû ÑÏ, ñîîòâåòñòâóþùèå êîíñòðóêöèÿì MSC
a á â ã
ä å æ ç è
4. Ñîáûòèÿ, êîòîðûå ðàñïîëîæåíû íåïîñðåäñòâåííî ïåðåä e i� ñîãëàñíî ÿâíî-
ìó óïîðÿäî÷åíèþ, âûðàæåííîìó êîíñòðóêöèÿìè before èëè after.
×òîáû óìåíüøèòü ðàçìåð ðåçóëüòèðóþùåé ÑÏ, èç ìíîæåñòâà Pre e i� �( ) ìîæíî
èñêëþ÷èòü ýëåìåíòû, êîòîðûå íå óäîâëåòâîðÿþò îòíîøåíèþ äîìèíèðîâàíèÿ îòíî-
ñèòåëüíî ïîðÿäêà ñîáûòèé è êîíñòðóêöèé. Çàìåòèì, ÷òî ýòà îïåðàöèÿ íå âëèÿåò íà
ÿçûê, ãåíåðèðóåìûé ðåçóëüòèðóþùåé ÑÏ, à òîëüêî óìåíüøàåò åå ðàçìåð (ñîîòâåò-
ñòâóåò óïðîùåíèþ ÑÏ, ïîêàçàííîìó íà ðèñ. 1,à.
Îïðåäåëåíèå 8. Ìíîæåñòâîì Pre e Pre e Pre Pre ei i i� � � � � � �( ) ( ) ( ( ))* � � ��
áóäåì íàçûâàòü òðàíçèòèâíîå çàìûêàíèå Pre e i� �( ) îòíîñèòåëüíî ïðåäøåñòâîâàíèÿ.
3. ÎÁÎÑÍÎÂÀÍÈÅ ÀËÃÎÐÈÒÌÀ ÊÎÍÂÅÐÒÀÖÈÈ
Ïóñòü S1 — äîêóìåíò MSC, à S A S2 1� ( ) — ñåòü Ïåòðè, ïîñòðîåííàÿ ïî ýòîìó äîêó-
ìåíòó ñîîòâåòñòâåííî ñ âûøåîïèñàííûì àëãîðèòìîì. Ïîêàæåì, ÷òî r S L Sp( ( )) ( )�
1 2� ,
äîêàçàâ âêëþ÷åíèÿ r S L Sp( ( )) ( )� 1 2� è r S L Sp( ( )) ( )� 1 2� .
3.1. Äîêàçàòåëüñòâî âêëþ÷åíèÿ r S L S
p( ( )) ( )� 1 2� . Îïðåäåëåíèå 9. Äîêó-
ìåíò MSC áóäåì íàçûâàòü àöèêëè÷åñêèì, åñëè â íåì îòñóòñòâóþò óïðàâëÿþùèå
êîíñòðóêöèè loop è åãî HMSC ïðåäñòàâëÿþò àöèêëè÷åñêèå ãðàôû.
Ëåãêî óâèäåòü, ÷òî âñå òðàññû, ñîîòâåòñòâóþùèå àöèêëè÷åñêîìó äîêóìåíòó
MSC, êîíå÷íû è èõ êîëè÷åñòâî òàêæå êîíå÷íî.
Òåîðåìà 1. Äëÿ àöèêëè÷åñêîãî äîêóìåíòà MSC ñåòü Ïåòðè, ïîñòðîåííàÿ âû-
øåïðèâåäåííûì àëãîðèòìîì, ãåíåðèðóåò ÿçûê, âêëþ÷àþùèé ìíîæåñòâî ñòàòè÷åñ-
êèõ òðàññ, êîòîðûå ãåíåðèðóþòñÿ èñõîäíûì äîêóìåíòîì MSC.
Äîêàçàòåëüñòâî òåîðåìû âûïîëíèì ìåòîäîì ìàòåìàòè÷åñêîé èíäóêöèè ïî êî-
ëè÷åñòâó ñîáûòèé n â èñõîäíîì äîêóìåíòå MSC.
Áàçèñ èíäóêöèè. Äîêóìåíò MSC ñ îäíèì ñîáûòèåì èçîáðàæåí íà ðèñ. 5,à, ãäå
e�1 — íåêîòîðîå ñîáûòèå (íà äèàãðàììå èçîáðàæåíî èñïîëüçîâàí øòðèõîâûì ýëëèï-
ñîì). Ìíîæåñòâî òðàññ òàêîãî äîêóìåíòà âêëþ÷àåò òîëüêî îäíó òðàññó { }e�1 . ÑÏ, ïî-
ñòðîåííàÿ äëÿ òàêîãî äîêóìåíòà, ïîêàçàíà íà ðèñ. 5,á, îòêóäà âèäíî, ÷òî åå ÿçûê ñîñòî-
èò èç îäíîãî ñëîâà ( )e�1 ; òàêèì îáðàçîì, ïðè n �1 óñëîâèå òåîðåìû âûïîëíÿåòñÿ.
Øàã èíäóêöèè. Ïðåäïîëîæèì, ÷òî èìååòñÿ äîêóìåíò MSC, ñîñòîÿùèé èç n
ñîáûòèé, è ñîîòâåòñòâóþùàÿ åìó ÑÏ Pn , äëÿ êîòîðîé âûïîëíÿåòñÿ óñëîâèå òåîðå-
ìû. Ðàññìîòðèì íîâûé äîêóìåíò MSC, ïîëó÷åííûé âñëåäñòâèå äîáàâëåíèÿ íîâîãî
ñîáûòèÿ e n� �1 ê èñõîäíîìó äîêóìåíòó, è ñîîòâåòñòâóþùóþ åìó ÑÏ Pn�1. Êàæäîå
ñîáûòèå e i ni� , ,�1 , èç èñõîäíîãî äîêóìåíòà íàõîäèòñÿ â îäíîì èç òðåõ âîçìîæ-
íûõ îòíîøåíèé ê e n� �1.
— Ïîñëåäîâàòåëüíîå âûïîëíåíèå: e ei n� �� �1 — â ìíîæåñòâå òðàññ äîêóìåí-
òà èìåþòñÿ ñëîâà âèäà ( )� � �e ei n� � �1 è íåò ñëîâ âèäà ( )� � �e en i� ��1 .
— Ïàðàëëåëüíîå âûïîëíåíèå (÷åðåäîâàíèå): e ei n� �| | �1 — â ìíîæåñòâå òðàññ äî-
êóìåíòà èìåþòñÿ ñëîâà êàê âèäà ( )� � �e ei n� � �1 , òàê è âèäà
( )� � �e en i� ��1 .
— Àëüòåðíàòèâíîå âûïîëíåíèå (êîíôëèêò): e ei n� �# �1 — â ìíîæåñòâå òðàññ
äîêóìåíòà èìåþòñÿ ñëîâà âèäà ( )� �e i� èëè ( )� �e n� �1 è íå èìååòñÿ ñëîâ
âèäà ( )� � �e ei n� � �1 èëè ( )� � �e en i� ��1 .
Ïîêàæåì, ÷òî äëÿ êàæäîãî èç ïåðå÷èñëåííûõ ñëó÷àåâ ÿçûê ñåòè Pn�1 âêëþ÷àåò
ìíîæåñòâî ñòàòè÷åñêèõ òðàññ, ãåíåðèðóåìûõ èñõîäíûì äîêóìåíòîì MSC.
1. Ïîñëåäîâàòåëüíîå âûïîëíåíèå. Ïðåäïîëîæèì, ÷òî èìååò ìåñòî ñèòóàöèÿ
e ei n� �� �1. Ðàññìîòðèì âîçìîæíûå ñëó÷àè ïîñëåäîâàòåëüíîãî âûïîëíåíèÿ ñîáû-
òèé e i� è e n� �1 â äîêóìåíòå MSC.
1 o . Êàê e i� , òàê è e n� �1 ïðèíàäëåæàò îäíîé è òîé æå äèàãðàììå MSC, ðàçäå-
ëÿþò ìåæäó ñîáîé îäíó ñóùíîñòü è íå íàõîäÿòñÿ â îáëàñòè ïðîèçâîëüíîãî âûïîë-
íåíèÿ. Êðîìå òîãî, ñîáûòèå e i� ðàñïîëîæåíî íåïîñðåäñòâåííî ïåðåä e n� �1 ïî ýòîé
ñóùíîñòè. Òîãäà e Pre ei n� � �� �( )1 ïî ïîñòðîåíèþ Pre e n� �( )�1 è ýòèì ñîáûòèÿì
ñîîòâåòñòâóåò ôðàãìåíò ÑÏ, ïîêàçàííûé íà ðèñ. 5,â. Òàêèì îáðàçîì, â L Pp
n( )�1 áó-
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2009, ¹ 4 41
äóò ïðèñóòñòâîâàòü ñëîâà âèäà ( )� �e ei n� � �1 è íå áóäåò ñëîâ âèäà
( )� � �e en i� ��1 .  äàííîì ñëó÷àå óñëîâèå òåîðåìû âûïîëíÿåòñÿ.
2 o . Ñîáûòèÿ e i� è e n� �1 ïðèíàäëåæàò ðàçíûì äèàãðàììàì MSC, êîòîðûå ñîå-
äèíåíû ïîñëåäîâàòåëüíî. Ñîîòâåòñòâóþùèé ôðàãìåíò ÑÏ ïîêàçàí íà ðèñ. 5,ã. Òà-
êèì îáðàçîì, â L Pp
n( )�1 áóäóò ïðèñóòñòâîâàòü ñëîâà âèäà ( )� � �e ei n� � �1 è íå
áóäåò ñëîâ âèäà ( )� � �e en i� ��1 .  äàííîì ñëó÷àå óñëîâèå òåîðåìû âûïîëíÿåòñÿ.
3 o . Ñîáûòèå e i� ÿâëÿåòñÿ ïîñûëêîé ñîîáùåíèÿ, à e n� �1 — ïðèåìîì ýòîãî ñî-
îáùåíèÿ. Òîãäà e Pre ei n� � �� �( )1 ïî ïîñòðîåíèþ ìíîæåñòâà Pre e n� �( )�1 , è ïðè-
õîäèì ê ñèòóàöèè, îïèñàííîé â ï. 1o .
4 o . Ñîáûòèå e i� ÿâëÿåòñÿ ñîáûòèåì òèïà ñîçäàòü ñóùíîñòü, à e n� �1 — ñîçäà-
íèåì ýòîé ñóùíîñòè. Òîãäà e Pre ei n� � �� �( )1 ïî ïîñòðîåíèþ ìíîæåñòâà
Pre e n� �( )�1 , è ïðèõîäèì ê ñèòóàöèè, îïèñàííîé â ï. 1o .
5 o . Ñîáûòèÿ e i� è e n� �1 óïîðÿäî÷åíû â ñîîòâåòñòâèè ñ ÿâíûì ïîðÿäêîì, ïðè
ýòîì e i� íåïîñðåäñòâåííî ïðåäøåñòâóåò e n� �1. Òîãäà e Pre ei n� � �� �( )1 ïî ïîñòðî-
åíèþ ìíîæåñòâà Pre e n� �( )�1 , è ïðèõîäèì ê ñèòóàöèè, îïèñàííîé â ï. 1o .
6 o . Ñîáûòèÿ e i� è e n� �1 íå óïîðÿäî÷åíû íåïîñðåäñòâåííî, íî ñóùåñòâóåò ïî-
ñëåäîâàòåëüíîñòü e e k� �1� �, ,� òàêàÿ, ÷òî e e e ei k n� � � �� � � � � � �1 1� , ãäå çíàê �
ñîîòâåòñòâóåò îäíîìó èç îòíîøåíèé, îïèñàííûõ â ïï.1o –3o . Òîãäà â ñîîòâåòñòâèè ñ âûøå-
42 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2009, ¹ 4
Ðèñ. 5. Äîêóìåíò MSC ñ îäíèì ñîáûòèåì (à) è ôðàãìåíòû ÑÏ äëÿ ïîñëåäîâàòåëüíîé êîìïîçèöèè (á–ã)
ãâáà
ñêàçàííûì â L Pp
n( )�1 áóäóò ïðèñóòñòâîâàòü ñëîâà âèäà ( )� � �e ei n� � �1 è íå áóäåò
ñëîâ âèäà ( )� � �e en i� ��1 .  äàííîì ñëó÷àå óñëîâèå òåîðåìû âûïîëíÿåòñÿ.
2. Ïàðàëëåëüíîå âûïîëíåíèå. Ïðåäïîëîæèì, ÷òî èìååò ìåñòî ñèòóàöèÿ
e ei n� �| | �1. Ðàññìîòðèì âîçìîæíûå ñëó÷àè ïàðàëëåëüíîãî âûïîëíåíèÿ ñîáûòèé e i�
è e n� �1 â äîêóìåíòå MSC.
1 o . Êàê e i� , òàê è e n� �1 ïðèíàäëåæàò îäíîé è òîé æå äèàãðàììå MSC, íî íå
ðàçäåëÿþò ìåæäó ñîáîé íè îäíîé ñóùíîñòè. Êðîìå òîãî, e i� è e n� �1 íå óïîðÿäî÷å-
íû ïîñëåäîâàòåëüíî êàêèì-ëèáî èç îïèñàííûõ â ï. 1 ìåòîäîâ (e Pre ei n� � �� �( )*
1 è
e Pre en i� � �� �1 ( )* ). Ñîîòâåòñòâóþùèé ôðàãìåíò Pn�1 ïîêàçàí íà ðèñ. 6,à (â íåì
îòñóòñòâóþò ïóòè ìåæäó ïåðåõîäàìè e i� è e n� �1). Ñîãëàñíî ïðèíöèïó íåçàâèñèìî-
ãî ñðàáàòûâàíèÿ ïåðåõîäîâ â ñåòè Ïåòðè ÿçûê L Pp
n( )�1 áóäåò ñîäåðæàòü ñëîâà êàê
âèäà ( )� � �e ei n� � �1 , òàê è âèäà ( )� � �e en i� ��1 .  äàííîì ñëó÷àå óñëî-
âèå òåîðåìû âûïîëíÿåòñÿ.
2 o . Ñîáûòèÿ e i� è e n� �1 ïðèíàäëåæàò ðàçíûì äèàãðàììàì MSC, êîòîðûå íå-
ïîñðåäñòâåííî ñîåäèíåíû ïàðàëëåëüíîé êîìïîçèöèåé. Êðîìå òîãî, e i� è e n� �1 íå
óïîðÿäî÷åíû ïîñëåäîâàòåëüíî êàêèì-ëèáî èç îïèñàííûõ â ï. 1 ìåòîäîâ
( ( )*e Pre ei n� � �� �1 è e Pre en i� � �� �1 ( )* ) . Ñîîòâåòñòâóþùèé ôðàãìåíò ïîêàçàí
íà ðèñ. 6,á (â íåì îòñóòñòâóþò ïóòè ìåæäó ïåðåõîäàìè e i� è e n� �1). Ñîãëàñíî
ïðèíöèïó íåçàâèñèìîãî ñðàáàòûâàíèÿ ïåðåõîäîâ â ñåòè Ïåòðè ÿçûê L Pp
n( )�1 áóäåò
ñîäåðæàòü ñëîâà êàê âèäà ( )� � �e ei n� � �1 , òàê è âèäà ( )� � �e en i� ��1 .
 äàííîì ñëó÷àå óñëîâèå òåîðåìû âûïîëíÿåòñÿ.
3 o . Ñîáûòèÿ e i� è e n� �1 ïðèíàäëåæàò ðàçíûì äèàãðàììàì MSC, êîòîðûå êîñ-
âåííî ñîåäèíåíû ïàðàëëåëüíîé êîìïîçèöèåé (íàïðèìåð, e i� �msc1, e n� � �1 msc2 è
äîêóìåíò MSC ñîäåðæèò ñëåäóþùåå ññûëî÷íîå âûðàæåíèå: msc1 par (msc3 seq
msc2)). Êðîìå òîãî, e i� è e n� �1 íå óïîðÿäî÷åíû ïîñëåäîâàòåëüíî êàêèì-ëèáî èç
îïèñàííûõ â ï. 1 ìåòîäîâ (e Pre ei n� � �� �( )*
1 è e Pre en i� � �� �1 ( )* ).  ýòîì ñëó-
÷àå ñîîòâåòñòâóþùèé ôðàãìåíò Pn�1 òàêîé æå, êàê è äëÿ ï. 2o . Ñîîòâåòñòâåííî
óñëîâèå òåîðåìû âûïîëíÿåòñÿ.
3. Àëüòåðíàòèâíîå âûïîëíåíèå. Ïðåäïîëîæèì, ÷òî èìååò ìåñòî ñèòóàöèÿ
e ei n� �# �1 . Â äîêóìåíòå MSC àëüòåðíàòèâíîå âûïîëíåíèå ñîáûòèé e i� è e n� �1 âîç-
ìîæíî òîëüêî â ñëó÷àå, êîãäà îíè ïðèíàäëåæàò ðàçíûì äèàãðàììàì MSC, íåïîñðåä-
ñòâåííî èëè êîñâåííî ñîåäèíåííûõ àëüòåðíàòèâíîé êîìïîçèöèåé.  îáîèõ ñëó÷àÿõ ñî-
îòâåòñòâóþùèé ôðàãìåíò Pn�1 ïîêàçàí íà ðèñ. 6,â. Çäåñü L Pp
n( )�1 ñîäåðæèò ñëîâà
âèäà ( )� �e i� èëè ( )� �e n� �1 , íî íå ñîäåðæèò ñëîâ âèäà ( )� � �e ei n� � �1
èëè ( )� � �e en i� ��1 .  äàííîì ñëó÷àå óñëîâèå òåîðåìû âûïîëíÿåòñÿ.
Êàê âèäèì, äëÿ âñåõ âîçìîæíûõ êîìïîçèöèé e i� è e n� �1 êàæäîé èç ìíîæåñòâà
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2009, ¹ 4 43
Ðèñ. 6. Ôðàãìåíòû ÑÏ äëÿ ïàðàëëåëüíîé (à, á) è àëüòåðíàòèâíîé (â) êîìïîçèöèé
à á â
òðàññ äîêóìåíòà MSC ñîîòâåòñòâóåò ñëîâî â ÿçûêå, ãåíåðèðóåìîì ïîñòðîåííîé ÑÏ. Òà-
êèì îáðàçîì, ïî èíäóêöèè èìååì r S L Sp( ( )) ( )� 1 2� , ÷òî è òðåáîâàëîñü äîêàçàòü.
Òåîðåìà 2. Äîáàâëåíèå êîíñòðóêöèé èòåðàöèè (óïðàâëÿþùèõ êîíñòðóêöèé
loop èëè öèêëè÷åñêèõ ðåáåð â HMSC) â äîêóìåíò MSC ñîãëàñíî âûøåïðèâåäåííî-
ìó àëãîðèòìó íå íàðóøàåò âêëþ÷åíèÿ ìíîæåñòâà ñòàòè÷åñêèõ òðàññ, ãåíåðèðóåìî-
ãî èñõîäíûì äîêóìåíòîì MSC â ÿçûê ïîñòðîåííîé ïî íåìó ÑÏ.
Äîêàçàòåëüñòâî. Èòåðàöèè ïîñëåäîâàòåëüíîñòè ñîáûòèé ( )se��
� â ìíîæåñòâå
òðàññ äîêóìåíòà ñîîòâåòñòâóþò ñëîâà âèäà ( )� �se�1 , ( )� �se se� �1 1 ,
( )� �se se se� � �1 1 1 è ò.ä.
Ïóñòü èìåþòñÿ äîêóìåíò MSC M è ñåòü Ïåòðè P òàêèå, ÷òî ìíîæåñòâî ñòàòè÷åñ-
êèõ òðàññ äîêóìåíòà M âêëþ÷àåòñÿ â ïðåôèêñíûé ÿçûê ñåòè P. Ðàññìîòðèì äîêóìåíò
M�, ïîëó÷åííûé äîáàâëåíèåì â M èòåðàöèè, è ñîîòâåòñòâóþùóþ åìó ñåòü P�.
Èòåðàöèÿ â MSC ìîæåò áûòü ïðåäñòàâëåíà ëèáî êîíñòðóêöèåé loop â ññûëî÷íîì èëè
âñòðîåííîì âûðàæåíèè, ëèáî öèêëè÷åñêîé ññûëêîé â HMSC. Ðàññìîòðèì ýòè ñëó÷àè.
Êîíñòðóêöèÿ loop. Ñîãëàñíî ðàçä. 1.2 âñòðîåííîå âûðàæåíèå, èñïîëüçóþùåå
loop, ìîæíî ðàññìàòðèâàòü êàê ññûëî÷íîå âûðàæåíèå íàä àíîíèìíîé äèàãðàì-
ìîé MSC. Ïîýòîìó îáúåäèíèì äîêàçàòåëüñòâà äëÿ êîíñòðóêöèè loop êàê äëÿ ññû-
ëî÷íîãî, òàê è äëÿ âñòðîåííîãî âûðàæåíèé. Àðãóìåíòîì êîíñòðóêöèè loop áóäåò
íåêîòîðîå ññûëî÷íîå âûðàæåíèå ref1, êîòîðîìó ñîîòâåòñòâóåò ïîñëåäîâàòåëüíîñòü
ñîáûòèé se�1.  íîâîì äîêóìåíòå M� îíî çàìåíÿåòñÿ íà ññûëî÷íîå âûðàæåíèå
loop < 1, inf > (ref1). Ñîãëàñíî àëãîðèòìó â P� åìó áóäåò ñîîòâåòñòâîâàòü ôðàãìåíò,
ïîêàçàííûé íà ðèñ. 7,à. Êàê âèäèì, â ÿçûêå L Pp ( )� áóäóò ïðèñóòñòâîâàòü ñëîâà
âèäà ( )� �se�1 , ( )� �se se� �1 1 , ( )� �se se se� � �1 1 1 , ... Ñëåäîâàòåëüíî, ïðè
äîáàâëåíèè â äîêóìåíò MSC êîíñòðóêöèè loop óñëîâèå òåîðåìû âûïîëíÿåòñÿ.
Öèêëè÷åñêàÿ ññûëêà â HMSC. Ïóñòü â M èìååòñÿ íåêîòîðàÿ ïîñëåäîâàòåëü-
íîñòü êîíñòðóêöèé (ïóòü) e e n� �1 � �� , ê êîòîðîé ïðè ïîñòðîåíèè M� äîáàâëÿåò-
ñÿ öèêëè÷åñêàÿ ññûëêà e en� �� 1. Äàííîìó ïóòè ñîîòâåòñòâóåò ïîñëåäîâàòåëü-
íîñòü ñîáûòèé se�1. Ðàññìîòðèì ñåòü P�, ïîëó÷åííóþ ñîãëàñíî àëãîðèòìó. Äàííîìó
ïóòè â íåé áóäåò ñîîòâåòñòâîâàòü
êîíñòðóêöèÿ, ïîêàçàííàÿ íà ðèñ.
7,á. Êàê âèäèì, â ÿçûêå L Pp ( )�
áóäóò ïðèñóòñòâîâàòü ñëîâà âèäà
( )� �se�1 , ( )� �se se� �1 1 ,
( )� �se se se� � �1 1 1 , ... Ñëåäîâà-
òåëüíî, ïðè äîáàâëåíèè â HMSC
öèêëè÷åñêîé ññûëêè óñëîâèå òåî-
ðåìû âûïîëíÿåòñÿ.
Òàêèì îáðàçîì, äîáàâëåíèå
èòåðàöèè ñîõðàíÿåò âêëþ÷åíèå
ìíîæåñòâà òðàññ äîêóìåíòà MSC
â ÿçûê ïîñòðîåííîé ïî íåìó ÑÏ,
÷òî è òðåáîâàëîñü äîêàçàòü.
Èç òåîðåì 1 è 2 ñëåäóåò, ÷òî ìíîæåñòâî òðàññ, ãåíåðèðóåìûõ äîêóìåíòîì
MSC, âêëþ÷àåòñÿ â ÿçûê ïîñòðîåííîé ïî íåìó ÑÏ äëÿ ëþáîãî äîêóìåíòà MSC.
3.2. Äîêàçàòåëüñòâî âêëþ÷åíèÿ r S L S
p( ( )) ( )� 1 2� . Òåîðåìà 3. Äëÿ äîêó-
ìåíòà MSC S1 è ïîñòðîåííîé ïî ýòîìó äîêóìåíòó ÑÏ S A S2 1� ( ) âûïîëíÿåòñÿ
âêëþ÷åíèå r S L Sp( ( )) ( )� 1 2� , ò.å. êàæäîìó ñëîâó ÿçûêà ïîñòðîåííîé ÑÏ ñîîòâåò-
ñòâóåò òðàññà â èñõîäíîì äîêóìåíòå.
Äîêàçàòåëüñòâî. Ðàññìîòðèì ñëîâà ÿçûêà L Sp ( )2 . Ïî ïîñòðîåíèþ ÑÏ, ìíî-
æåñòâî ñèìâîëîâ, èç êîòîðûõ ñîñòîÿò ýòè ñëîâà, âêëþ÷àåòñÿ â ìíîæåñòâî ñîáûòèé
èñõîäíîãî äîêóìåíòà (ñ òî÷íîñòüþ äî ïåðåèìåíîâàíèÿ). Äëÿ ëþáîé ïàðû ñèìâîëîâ
e e� �1 2, âîçìîæíû ñëåäóþùèå âàðèàíòû âçàèìíîãî ðàñïîëîæåíèÿ. Ðàññìîòðèì èõ.
44 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2009, ¹ 4
Ðèñ. 7. Ôðàãìåíòû ÑÏ äëÿ èòåðàöèè
áà
1 o . Â ÿçûêå ïðèñóòñòâóþò ñëîâà âèäà ( )� � �e e� �1 2 è îòñóòñòâóþò ñëîâà
âèäà ( )� � �e e� �2 1 . Ýòî èìååò ìåñòî ëèøü â ñëó÷àå, êîãäà ÑÏ ñîäåðæèò ôðàã-
ìåíò, ïîêàçàííûé íà ðèñ. 8,à. Ñîãëàñíî àëãîðèòìó ïîñòðîåíèÿ ÑÏ òàêîé ôðàãìåíò
ìîæåò âîçíèêíóòü òîëüêî â ñëó÷àÿõ, ïîêàçàííûõ íà ðèñ. 5,â (â ñëó÷àå
e Pre e� � �1 2
� ( )* ) è ðèñ. 5,ã (â ñëó÷àå, êîãäà e i� è e n� �1 ïðèíàäëåæàò ðàçíûì äèà-
ãðàììàì MSC, êîòîðûå ñîåäèíåíû ïîñëåäîâàòåëüíî). Îáà âàðèàíòà ïðèâîäÿò ê ïî-
ÿâëåíèþ â ìíîæåñòâå òðàññ èñõîäíîãî äîêóìåíòà MSC ïîñëåäîâàòåëüíîñòè ñîáû-
òèé ( )� � �e e� �1 2 . Òàêèì îáðàçîì, êàæäîå ñëîâî èç L Sp ( )2 èìååò ñîîòâåòñòâó-
þùóþ åìó òðàññó â �( )S1 .
2 o . Â ÿçûêå ïðèñóòñòâóþò êàê ñëîâà âèäà ( )� � �e e� �1 2 , òàê è ñëîâà âèäà
( )� � �e e� �2 1 . Ýòî èìååò ìåñòî ëèøü â ñëó÷àå, êîãäà ÑÏ ñîäåðæèò ôðàãìåíò, ïî-
êàçàííûé íà ðèñ. 8,á. Ñîãëàñíî àëãîðèòìó ïîñòðîåíèÿ ÑÏ òàêîé ôðàãìåíò ìîæåò âîç-
íèêíóòü òîëüêî â ñëó÷àÿõ, ïîêàçàííûõ íà ðèñ. 6,à (íåçàâèñèìîå èñïîëíåíèå äâóõ ñóù-
íîñòåé) è ðèñ. 6,á (êîíñòðóêöèÿ ïàðàëëåëüíîé êîìïîçèöèè). Ñîãëàñíî ñåìàíòèêå MSC
îáà ýòè âàðèàíòà ïðèâåäóò ê ïîÿâëåíèþ â ìíîæåñòâå òðàññ èñõîäíîãî äîêóìåíòà MSC
ïîñëåäîâàòåëüíîñòåé ñîáûòèé âèäà ( )� � �e e� �1 2 è ( )� � �e e� �2 1 . Òàêèì îá-
ðàçîì, êàæäîå ñëîâî èç L Sp ( )2 èìååò ñîîòâåòñòâóþùóþ åìó òðàññó â �( )S1 .
3 o . Â ÿçûêå ïðèñóòñòâóþò ñëîâà âèäà ( )� �e�1 è ( )� �e�2 . Ýòî èìååò
ìåñòî ëèøü â ñëó÷àå, êîãäà ÑÏ ñîäåðæèò ôðàãìåíò, ïîêàçàííûé íà ðèñ. 8,â. Ñîãëàñ-
íî àëãîðèòìó ïîñòðîåíèÿ ÑÏ òàêîé ôðàãìåíò ìîæåò âîçíèêíóòü òîëüêî â ñëó÷àå,
ïîêàçàííîì íà ðèñ. 6,â (êîíñòðóêöèÿ àëüòåðíàòèâíîãî âûïîëíåíèÿ). Ñîãëàñíî ñå-
ìàíòèêå MSC â ìíîæåñòâå òðàññ èñõîäíîãî äîêóìåíòà MSC áóäóò ïðèñóòñòâîâàòü
ïîñëåäîâàòåëüíîñòè âèäà ( )� �e�1 è ( )� �e�2 . Òàêèì îáðàçîì, êàæäîå ñëîâî
èç L Sp ( )2 èìååò ñîîòâåòñòâóþùóþ åìó òðàññó â �( )S1 .
4 o . Â ÿçûêå ïðèñóòñòâóþò ñëîâà âèäà ( )� �se�1 , ( )� �se se� �1 1 ,
( )� �se se se� � �1 1 1 , ... , ãäå se�1 — íåêîòîðàÿ ïîñëåäîâàòåëüíîñòü ñèìâîëîâ. Çàìå-
òèì, ÷òî ñîãëàñíî ïîñòðîåíèþ ñåòü Ïåòðè S 2 êîíå÷íà. Òàêèì îáðàçîì, áåñêîíå÷íàÿ
ïîñëåäîâàòåëüíîñòü â åå ÿçûêå ìîæåò áûòü ïîëó÷åíà òîëüêî ñ ïîìîùüþ öèêëà, ïîêà-
çàííîãî íà ðèñ. 8,ã, ãäå k îáîçíà÷àåò ôðàãìåíò ñåòè, ãåíåðèðóþùèé se�1 (öèêëû äðóãî-
ãî âèäà íåâîçìîæíû ïî ïîñòðîåíèþ ÑÏ). Ïîäîáíûé öèêë èìååò ìåñòî â ñëó÷àÿõ, ïîêà-
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2009, ¹ 4 45
Ðèñ. 8. Âîçìîæíûå ôðàãìåíòû ïîñòðîåííîé ÑÏ
à á â ã
çàííûõ íà ðèñ. 7,à (êîíñòðóêöèÿ loop) è ðèñ. 7,á (öèêëè÷åñêàÿ ññûëêà â HMSC). Ñî-
ãëàñíî ñåìàíòèêå MSC â ìíîæåñòâå òðàññ èñõîäíîãî äîêóìåíòà MSC áóäóò
ïðèñóòñòâîâàòü ïîñëåäîâàòåëüíîñòè âèäà ( )� �se�1 , ( )� �se se� �1 1 ,
( )� �se se se� � �1 1 1 , ... Òàêèì îáðàçîì, êàæäîå ñëîâî èç L Sp ( )2 èìååò ñîîòâåòñòâóþ-
ùóþ åìó òðàññó â �( )S1 .
 ñèëó ïðîèçâîëüíîñòè âûáîðà e�1 è e�2 êàæäîå ñëîâî èç L Sp ( )2 èìååò ñîîò-
âåòñòâóþùóþ åìó òðàññó â �( )S1 , ÷òî è òðåáîâàëîñü äîêàçàòü. Òàêèì îáðàçîì,
r S L Sp( ( )) ( )� 1 2� è r S L Sp( ( )) ( )� 1 2� , ò.å. r S( ( ))� 1 � L Sp ( )2 è ïîñòðîåííàÿ ïî
îïèñàííîìó àëãîðèòìó ÑÏ ñîáûòèéíî ýêâèâàëåíòíà èñõîäíîìó äîêóìåíòó MSC.
4. ÏÐÈÌÅÐ ÊÎÍÂÅÐÒÀÖÈÈ MSC-ÄÈÀÃÐÀÌÌÛ Â ÑÏ
È ÈÑÑËÅÄÎÂÀÍÈß ÑÒÐÓÊÒÓÐÍÛÕ ÑÂÎÉÑÒÂ
Ïðîèëëþñòðèðóåì ðàáîòó àëãîðèòìà íà ïðèìåðå îäíîâðåìåííîé êîíêóðåíòíîé
ðàáîòû äâóõ àãåíòîâ ñ îáùèì ðåñóðñîì. Ïîñêîëüêó ïîëíûå ìîäåëè ðåàëüíûõ
ñèñòåì è ñîîòâåòñòâóþùèå èì ñåòè Ïåòðè çàíèìàþò áîëüøîé îáúåì, ïðèìåð áó-
äåò ìàêñèìàëüíî óïðîùåííûì. (Áîëåå ïîäðîáíûå ïðèìåðû ðàçìåùåíû ïî àäðåñó
http://avch.org.ua/samples/.)
4.1. Èñõîäíàÿ MSC-äèàãðàì-
ìà. Èñõîäíûé äîêóìåíò MSC ïîêà-
çàí íà ðèñ. 9. Íà äèàãðàììå msc1
ïðèñóòñòâóþò äâà àãåíòà (ïðåäñòàâ-
ëåííûõ ñóùíîñòÿìè i è j), êàæäûé
èç êîòîðûõ ðàáîòàåò ñ îáùèì ðå-
ñóðñîì ñ ïîìîùüþ äåéñòâèé
getres1, leaveres1 è getres2, leaveres2
ñîîòâåòñòâåííî. Ïðåäïîëàãàåòñÿ,
÷òî â êàæäûé ìîìåíò âðåìåíè ñ ðå-
ñóðñîì ìîæåò ðàáîòàòü òîëüêî
îäèí àãåíò, ïîýòîìó ñîîòâåòñòâóþ-
ùèå äåéñòâèÿ ðàçíåñåíû ïî ðàçíûì
àëüòåðíàòèâàì âñòðîåííîãî âûðà-
æåíèÿ òèïà alt. Íà äèàãðàììå
hmsc1 ññûëêà íà msc1 ñîïðîâîæäàåòñÿ îïåðàòîðîì èòåðàöèè loop, ïîýòîìó äèà-
ãðàììà msc1 áóäåò âûïîëíÿòüñÿ íåîäíîêðàòíî.
4.2. Ñåòü Ïåòðè, ïîëó÷åííàÿ â ðåçóëüòàòå êîíâåðòàöèè. Ïîñòðîèì ñåòü
Ïåòðè äëÿ ïðèâåäåííîé äèàãðàììû ñ ïîìîùüþ ðaññìîòðåííîãî àëãîðèòìà. Äîêó-
ìåíò MSC ñîäåðæèò ÷åòûðå ñîáûòèÿ: getres1, leaveres1, getres2 è leaveres2. Ìíî-
æåñòâà Pre�() äëÿ ýòèõ ñîáûòèé èìåþò âèä
Pre getres alt in�( ) _1 �{ },
Pre leaveres getres�( )1 1�{ },
Pre getres alt in�( ) _2 �{ },
Pre leaveres getres�( )2 2�{ }.
Ñ ïîìîùüþ îïèñàííîãî àëãîðèòìà ïîëó÷àåì ñåòü, ïîêàçàííóþ íà ðèñ. 10,à;
ïðèìåíèâ ê íåé ïðàâèëà óïðîùåíèÿ ñåòè Ïåòðè (ñì. ðèñ. 1), ïîëó÷èì ñåòü, ïîêàçàí-
íóþ íà ðèñ. 10,á. Ðàçìåòêà ñåòè ïîêàçàíà ðÿäîì ñî çíàêàìè ïåðåõîäîâ.
46 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2009, ¹ 4
Ðèñ. 9. Äîêóìåíò MSC, îïèñûâàþùèé êîíêóðåíòíîå
âçàèìîäåéñòâèå ñ îáùèì ðåñóðñîì
4.3. Äåðåâî ïîêðûòèÿ. Ïîñòðîèì äåðåâî ïîêðûòèÿ äëÿ ïîëó÷åííîé (óïðîùåí-
íîé) ñåòè (ðèñ. 11). Àíàëèçèðóÿ äåðåâî ïîêðûòèÿ, ìîæíî ñäåëàòü ñëåäóþùèå âûâîäû:
1) ñåòü îãðàíè÷åíà;
2) ñåòü áåçîïàñíà;
3) â ñåòè íåò íåäîñòèæèìûõ ìåñò;
4) âñå ïåðåõîäû ñåòè ïîòåíöèàëüíî æèâû.
Ïðèìåíèòåëüíî ê àíàëèçó èñõîäíîãî äîêóìåíòà MSC ýòî îçíà÷àåò, ÷òî â äîêóìåíòå
íåò «ìåðòâûõ» ó÷àñòêîâ (êàæäîå ñîáûòèå ñåòè ìîæåò áûòü âûïîëíåíî â ðàìêàõ îïðåäå-
ëåííîãî ñöåíàðèÿ) è íåò ñèòóàöèè ìíîæåñòâåííîãî çàõâàòà ðåñóðñà (ïîñêîëüêó ñåòü áå-
çîïàñíà).
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2009, ¹ 4 47
Ðèñ. 11. Äåðåâî ïîêðûòèÿ äëÿ óïðîùåííîé ñåòè
Ðèñ. 10. Ñåòü Ïåòðè, ïîëó÷åííàÿ èç èñõîäíîãî äîêóìåíòà (à), è åå óïðîùåííûé âàðèàíò (á)
a á
4.4. Óðàâíåíèå ñîñòîÿíèÿ è åãî ðåøåíèå TSS-àëãîðèòìîì. Ïîñòðîèì ìàò-
ðèöó èíöèäåíòíîñòè äëÿ óïðîùåííîé ñåòè
A �
�
�
�
�
� �
�
�
�
��
�
�
1 0 0 0 0 0 0
1 1 0 0 0 1 0
0 0 1 1 1 0 0
0 0 0 1 1 1 0
0 0 0 0 1 1 1
�
�
!
�
��
"
�
�
�
.
Ðåøèâ óðàâíåíèå ñîñòîÿíèÿ ñèñòåìû Ax � 0 ñ ïîìîùüþ ìåòîäà TSS, ïîëó÷èì
óñå÷åííîå ìíîæåñòâî ðåøåíèé
0 1 1 0 1 1 0
0 1 0 1 1 1 0
#
$
%%
&
'
(( .
Îòñþäà ñëåäóåò, ÷òî âñå ïåðåõîäû, êðîìå ïåðâîãî è ïîñëåäíåãî (ñîîòâåòñòâóþ-
ùèõ ñòàðòó è îñòàíîâêå ñèñòåìû), ÿâëÿþòñÿ æèâûìè. Ïðèìåíèòåëüíî ê àíàëèçè-
ðóåìîé ñèñòåìå ýòî îáîçíà÷àåò, ÷òî âñå ÷åòûðå åå ñîáûòèÿ ìîãóò èñïîëíÿòüñÿ
íåîãðàíè÷åííîå ÷èñëî ðàç.
ÇÀÊËÞ×ÅÍÈÅ
 íàñòîÿùåé ñòàòüå îïèñàí àëãîðèòì ïåðåâîäà äîêóìåíòà MSC â ñîáûòèéíî ýê-
âèâàëåíòíóþ åìó ñåòü Ïåòðè. Äîêàçàíà ñîáûòèéíàÿ ýêâèâàëåíòíîñòü ïîëó÷åííîé
ÑÏ èñõîäíîìó äîêóìåíòó. Ïîêàçàí òåõíîëîãè÷åñêèé ïðîöåññ èñïîëüçîâàíèÿ ýòî-
ãî àëãîðèòìà äëÿ àíàëèçà ñâîéñòâ ñèñòåì, âûðàæåííûõ íà ÿçûêå MSC, à òàêæå
ïðèâåäåí ïðèìåð, èëëþñòðèðóþùèé ðàáîòó àëãîðèòìà.
ÑÏÈÑÎÊ ËÈÒÅÐÀÒÓÐÛ
1. I T U - T S R e c o m m e n d a t i o n Z.120: Message Sequence Chart (MSC) / Edited by ITU-TS. —
ITU-TS, Geneva, 2000. — 128 ð.
2. N a k a m u r a M . , K a k u d a Y . , K i k u n o T . Petri-net based detection method for non-deterministic
feature interaction and its experimental evaluation // Feature Interaction in Telecommunication Networks.
— 1997. — N 4. — Ð. 138–152.
3. K l u g e O . , P a d b e r g J . , E h r i g H . Model train control systems: From message sequence charts to
petri nets // Technische Universitat Berlin, 2001 — 18 p.
4. K r y v y y S . , M a t v y e y e v a L . , L o p a t i n a M . Automatic modeling and analysis of msc-specified
systems // Fundamenta Informaticae. — 2005. — 67, N 1–3. — Ð. 107–120.
5. K r y v y i S . , M a t v y e y e v a L . Algorithm of translation of msc-specified system into petri net // Ibid.
— 2007. — N 79. — Ð. 1–15.
6. K r y v y i S . , M a t v y e y e v a L . , C h u g a e n k o A . Extension of algorithm of translation of
msc-specified system into petri net // Proceedings of the CS&P’2007 Workshop, 2007. — Ð. 376–387.
7. × ó ã à å í ê î À . Î ðåàëèçàöèè àëãîðèòìà ïåðåâîäà íàáîðà msc-äèàãðàìì â ñåòü Ïåòðè //
Óïðàâëÿþùèå ñèñòåìû è ìàøèíû. — 2007. — ¹ 6. — Ñ. 17–23.
8. K r y v y y S . , C h u g a y e n k o O . Extended algorithm for translation of msc diagrams into petri nets //
Fundamenta Informaticae. — 2008. — 2, N 1. — Ð. 68–75.
9. Ê î ò î â Â . Å . Ñåòè Ïåòðè. — Ì.: Íàóêà, 1984. — 160 ñ.
10. M u r a t a T . Petri nets: Properties, analysis and applications // Proceedings of the IEEE. — 1989. — 77.
— Ð. 541–580.
11. Ê ð û â û é Ñ . Ë . Àëãîðèòìû ðåøåíèÿ ñèñòåì ëèíåéíûõ äèîôàíòîâûõ óðàâíåíèé â öåëî÷èñëåííûõ
îáëàñòÿõ // Êèáåðíåòèêà è ñèñòåìíûé àíàëèç. — 2006. — ¹ 2. — Ñ. 3–17.
12. × ó ã à å í ê î À . Î ðåàëèçàöèè tss-àëãîðèòìà // Óïðàâëÿþùèå ñèñòåìû è ìàøèíû. — 2007. — ¹ 4.
— Ñ. 14–18.
13. I T U - T S R e c o m m e n d a t i o n Z.120. Annex B: Algebraic Semantics of Message Sequence Charts /
Edited by ITU-TS. — ITU-TS, Geneva, 1998. — 73 p.
Ïîñòóïèëà 19.08.2008
48 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2009, ¹ 4
|