Генерация символьных трасс в системе инсерционного моделирования
Описан новый генератор символьных трасс, разработанный для последней версии системы инсерционного моделирования. Основными характеристиками генератора являются использование графического представления описания многоуровневых моделей, разделение локальных описаний и отношения следования, возможность...
Gespeichert in:
| Veröffentlicht in: | Кибернетика и системный анализ |
|---|---|
| Datum: | 2015 |
| Hauptverfasser: | , , , |
| Format: | Artikel |
| Sprache: | Russian |
| Veröffentlicht: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2015
|
| Schlagworte: | |
| Online Zugang: | https://nasplib.isofts.kiev.ua/handle/123456789/124753 |
| 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: | Генерация символьных трасс в системе инсерционного моделирования / А.А. Летичевский, А.Ал. Летичевский, В.С. Песчаненко, А.А. Губа // Кибернетика и системный анализ. — 2015. — Т. 51, № 1. — С. 7-19. — Бібліогр.: 25 назв. — рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
nasplib_isofts_kiev_ua-123456789-124753 |
|---|---|
| record_format |
dspace |
| spelling |
Летичевский, А.А. Летичевский, А.Ал. Песчаненко, В.С. Губа, А.А. 2017-10-04T19:48:18Z 2017-10-04T19:48:18Z 2015 Генерация символьных трасс в системе инсерционного моделирования / А.А. Летичевский, А.Ал. Летичевский, В.С. Песчаненко, А.А. Губа // Кибернетика и системный анализ. — 2015. — Т. 51, № 1. — С. 7-19. — Бібліогр.: 25 назв. — рос. 0023-1274 https://nasplib.isofts.kiev.ua/handle/123456789/124753 519.686.2 Описан новый генератор символьных трасс, разработанный для последней версии системы инсерционного моделирования. Основными характеристиками генератора являются использование графического представления описания многоуровневых моделей, разделение локальных описаний и отношения следования, возможность настройки на различные стратегии поиска, применение нового предикатного трансформера, допускающего кванторы общности с ослабленными ограничениями относительно предыдущих версий. Описано новий генератор символьних трас, розроблений для останньої версії системи інсерційного моделювання. Основними характеристиками цього генератора є використання графічного представлення опису багаторівневих моделей, поділ локальних описів і відносини слідування, можливість настроювання на різні стратегії пошуку. The paper describes a new generator of symbolic traces, which is designed for the latest version of insertion modeling system. The main characteristics of the generator is the use of graphic representations of the description of multilevel models, division of local descriptions and consequence relation, the possibility of configuration to different search strategies, and application of a new predicate transformer, which admits generality quantifiers with relaxed constraints with respect to the previous versions. ru Інститут кібернетики ім. В.М. Глушкова НАН України Кибернетика и системный анализ Кибернетика Генерация символьных трасс в системе инсерционного моделирования Генерація символьних трас у системі інерційного моделювання Generation of symbolic traces in insertion modeling system 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 |
2015 |
| language |
Russian |
| container_title |
Кибернетика и системный анализ |
| publisher |
Інститут кібернетики ім. В.М. Глушкова НАН України |
| format |
Article |
| title_alt |
Генерація символьних трас у системі інерційного моделювання Generation of symbolic traces in insertion modeling system |
| description |
Описан новый генератор символьных трасс, разработанный для последней версии системы инсерционного моделирования. Основными характеристиками генератора являются использование графического представления описания многоуровневых моделей, разделение локальных описаний и отношения следования, возможность настройки на различные стратегии поиска, применение нового предикатного трансформера, допускающего кванторы общности с ослабленными ограничениями относительно предыдущих версий.
Описано новий генератор символьних трас, розроблений для останньої версії системи інсерційного моделювання. Основними характеристиками цього генератора є використання графічного представлення опису багаторівневих моделей, поділ локальних описів і відносини слідування, можливість настроювання на різні стратегії пошуку.
The paper describes a new generator of symbolic traces, which is designed for the latest version of insertion modeling system. The main characteristics of the generator is the use of graphic representations of the description of multilevel models, division of local descriptions and consequence relation, the possibility of configuration to different search strategies, and application of a new predicate transformer, which admits generality quantifiers with relaxed constraints with respect to the previous versions.
|
| issn |
0023-1274 |
| url |
https://nasplib.isofts.kiev.ua/handle/123456789/124753 |
| citation_txt |
Генерация символьных трасс в системе инсерционного моделирования / А.А. Летичевский, А.Ал. Летичевский, В.С. Песчаненко, А.А. Губа // Кибернетика и системный анализ. — 2015. — Т. 51, № 1. — С. 7-19. — Бібліогр.: 25 назв. — рос. |
| work_keys_str_mv |
AT letičevskiiaa generaciâsimvolʹnyhtrassvsistemeinsercionnogomodelirovaniâ AT letičevskiiaal generaciâsimvolʹnyhtrassvsistemeinsercionnogomodelirovaniâ AT pesčanenkovs generaciâsimvolʹnyhtrassvsistemeinsercionnogomodelirovaniâ AT gubaaa generaciâsimvolʹnyhtrassvsistemeinsercionnogomodelirovaniâ AT letičevskiiaa generacíâsimvolʹnihtrasusistemíínercíinogomodelûvannâ AT letičevskiiaal generacíâsimvolʹnihtrasusistemíínercíinogomodelûvannâ AT pesčanenkovs generacíâsimvolʹnihtrasusistemíínercíinogomodelûvannâ AT gubaaa generacíâsimvolʹnihtrasusistemíínercíinogomodelûvannâ AT letičevskiiaa generationofsymbolictracesininsertionmodelingsystem AT letičevskiiaal generationofsymbolictracesininsertionmodelingsystem AT pesčanenkovs generationofsymbolictracesininsertionmodelingsystem AT gubaaa generationofsymbolictracesininsertionmodelingsystem |
| first_indexed |
2025-11-25T23:52:50Z |
| last_indexed |
2025-11-25T23:52:50Z |
| _version_ |
1850588921362120704 |
| fulltext |
À.À. ËÅÒÈ×ÅÂÑÊÈÉ, À.Àë. ËÅÒÈ×ÅÂÑÊÈÉ, Â.Ñ. ÏÅÑ×ÀÍÅÍÊÎ, À.À. ÃÓÁÀ
ÓÄÊ 519.686.2 ÃÅÍÅÐÀÖÈß ÑÈÌÂÎËÜÍÛÕ ÒÐÀÑÑ Â ÑÈÑÒÅÌÅ
ÈÍÑÅÐÖÈÎÍÍÎÃÎ ÌÎÄÅËÈÐÎÂÀÍÈß
Àííîòàöèÿ. Îïèñàí íîâûé ãåíåðàòîð ñèìâîëüíûõ òðàññ, ðàçðàáîòàííûé äëÿ ïîñëåäíåé
âåðñèè ñèñòåìû èíñåðöèîííîãî ìîäåëèðîâàíèÿ. Îñíîâíûìè õàðàêòåðèñòèêàìè ãåíåðàòîðà
ÿâëÿþòñÿ èñïîëüçîâàíèå ãðàôè÷åñêîãî ïðåäñòàâëåíèÿ îïèñàíèÿ ìíîãîóðîâíåâûõ ìîäåëåé,
ðàçäåëåíèå ëîêàëüíûõ îïèñàíèé è îòíîøåíèÿ ñëåäîâàíèÿ, âîçìîæíîñòü íàñòðîéêè íà ðàç-
ëè÷íûå ñòðàòåãèè ïîèñêà, ïðèìåíåíèå íîâîãî ïðåäèêàòíîãî òðàíñôîðìåðà, äîïóñêàþùåãî
êâàíòîðû îáùíîñòè ñ îñëàáëåííûìè îãðàíè÷åíèÿìè îòíîñèòåëüíî ïðåäûäóùèõ âåðñèé.
Êëþ÷åâûå ñëîâà: âåðèôèêàöèÿ, èíñåðöèîííîå ìîäåëèðîâàíèå, ÿçûê UCM.
ÂÂÅÄÅÍÈÅ
Èíñåðöèîííîå ìîäåëèðîâàíèå ïðåäñòàâëÿåò ñîáîé íàïðàâëåíèå, êîòîðîå ðàçâèâàåò-
ñÿ â òå÷åíèå ïîñëåäíèõ äâóõ äåñÿòèëåòèé â êà÷åñòâå ïîäõîäà ê îáùåé òåîðèè âçà-
èìîäåéñòâèÿ àãåíòîâ è ñðåä â ñëîæíûõ ðàñïðåäåëåííûõ ìíîãîàãåíòíûõ ñèñòåìàõ.
Èñòîðèÿ èíñåðöèîííîãî ìîäåëèðîâàíèÿ íà÷èíàåòñÿ ñ ðàáîò À. Ëåòè÷åâñêîãî
è Ä. Ãèëüáåðòà, âûïîëíåííûõ âî âòîðîé ïîëîâèíå 90-õ ãîäîâ ïðîøëîãî ñòîëåòèÿ,
â êîòîðûõ èññëåäîâàíû àáñòðàêòíûå ñåìàíòè÷åñêèå ìîäåëè íåäåòåðìèíèðîâàííûõ
ïàðàëëåëüíûõ ÿçûêîâ ïðîãðàììèðîâàíèÿ [1, 2]. Â äàëüíåéøåì ýòîò ïîäõîä áûë
îáîáùåí äî îáùåé ìîäåëè âçàèìîäåéñòâèÿ àãåíòîâ è ñðåä [3], îñíîâàííîé íà ïî-
íÿòèè ôóíêöèè ïîãðóæåíèÿ è àëãåáðû ïîâåäåíèé, ÿâëÿþùåéñÿ ðàçíîâèäíîñòüþ
àëãåáðû ïðîöåññîâ. Ìîäåëè èíñåðöèîííîãî ìîäåëèðîâàíèÿ îáîáùàþò áîëüøèí-
ñòâî òðàäèöèîííûõ ìîäåëåé âçàèìîäåéñòâóþùèõ ïðîöåññîâ, âêëþ÷àÿ CCS (èñ÷èñ-
ëåíèå âçàèìîäåéñòâóþùèõ ïðîöåññîâ) è �-èñ÷èñëåíèå Ð. Ìèëíåðà [4–6], CSP (âçà-
èìîäåéñòâóþùèå ïîñëåäîâàòåëüíûå ïðîöåññû) Ò. Õîàðà [7], ACP (àëãåáðà âçàèìî-
äåéñòâóþùèõ ïðîöåññîâ) Áåðãñòðû [8], èñ÷èñëåíèå ìîáèëüíûõ àìáèåíòîâ
Ë. Êàðäåëëè [9] è ìíîãèå äðóãèå îòâåòâëåíèÿ ýòèõ îñíîâíûõ òåîðèé.
Êàæäóþ òåîðèþ âçàèìîäåéñòâóþùèõ ïðîöåññîâ ìîæíî ïîëó÷èòü â ðåçóëü-
òàòå âûáîðà ïîäõîäÿùåé ôóíêöèè ïîãðóæåíèÿ — ïàðàìåòðà èíñåðöèîííîé ìîäå-
ëè. Îòìåòèì, ÷òî â îäíîé ìîäåëè ìîæíî èñïîëüçîâàòü íåñêîëüêî ôóíêöèé ïîãðó-
æåíèÿ (ìíîãîóðîâíåâûå ñðåäû). Ýòî ïîçâîëÿåò îáúåäèíÿòü ðàçëè÷íûå òåîðèè
âçàèìîäåéñòâèÿ. Èíñåðöèîííîå ìîäåëèðîâàíèå ïðèìåíÿåòñÿ òàêæå äëÿ óíèôèöè-
ðîâàííîãî ïðåäñòàâëåíèÿ òàêèõ àáñòðàêòíûõ ìîäåëåé ïàðàëëåëüíûõ âû÷èñëå-
íèé, êàê ñåòè Ïåòðè [10], ìîäåëè àêòåðîâ Õüþèòà [11], àâòîìàòíûå ñåòåâûå
ìîäåëè è ðàçëè÷íûå àáñòðàêöèè ïàðàäèãìû îáúåêòíî-îðèåíòèðîâàííîãî
ïàðàëëåëüíîãî ïðîãðàììèðîâàíèÿ.
Ñîâðåìåííîå ïðåäñòàâëåíèå òåîðåòè÷åñêèõ îñíîâ èíñåðöèîííîãî ìîäåëèðî-
âàíèÿ îïèñàíî â [12], ãäå àãåíòû ðàññìîòðåíû êàê íåïðåðûâíûå ïðåîáðàçîâàíèÿ
ñðåäû, à èõ ïîâåäåíèÿ — êàê ýëåìåíòû ïîëíîé íåïðåðûâíîé àëãåáðû ïîâåäåíèé,
ðàñøèðåííîé íåïðåðûâíûìè îïåðàöèÿìè, ñðåäè êîòîðûõ ãëàâíîå ìåñòî çàíèìà-
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2015, òîì 51, ¹ 1 7
© À.À. Ëåòè÷åâñêèé, À.Àë. Ëåòè÷åâñêèé, Â.Ñ. Ïåñ÷àíåíêî, À.À. Ãóáà, 2015
åò ôóíêöèÿ ïîãðóæåíèÿ. Òåðìèí «èíñåðöèîííîå ìîäåëèðîâàíèå» ââåäåí â [13]
âìåñòî «ìîäåëèðîâàíèå âçàèìîäåéñòâèÿ àãåíòîâ è ñðåä».
 2000-õ ãîäàõ íà÷àëèñü ðàáîòû ïî ïðèìåíåíèþ èíñåðöèîííîãî ìîäåëèðî-
âàíèÿ ïðè ðàçðàáîòêå ñèñòåì âåðèôèêàöèè òðåáîâàíèé è ñïåöèôèêàöèé ðàñïðå-
äåëåííûõ âçàèìîäåéñòâóþùèõ ñèñòåì [14–18]. Ñèñòåìà VRS (Verification of
Requirement Specifications), ðàçðàáîòàííàÿ ïî çàêàçó ôèðìû Ìîòîðîëà ñ ó÷àñòèåì
ñîòðóäíèêîâ Èíñòèòóòà êèáåðíåòèêè èì Â.Ì. Ãëóøêîâà, óñïåøíî èñïîëüçîâà-
ëàñü äëÿ ïðîâåðêè òðåáîâàíèé è ñïåöèôèêàöèé â îáëàñòè ñèñòåì ðåàëüíîãî
âðåìåíè, à òàêæå òåëåêîììóíèêàöèîííûõ è âñòðîåííûõ ñèñòåì.
Ïðîòîòèïû äëÿ îñíîâíûõ êîìïîíåíòîâ ñèñòåìû VRS ñîçäàíû íà áàçå ïåð-
âûõ âåðñèé ñèñòåìû èíñåðöèîííîãî ìîäåëèðîâàíèÿ, êîòîðàÿ âíà÷àëå ðàçðàáàòû-
âàëàñü êàê èíòåðïðåòàòîð äëÿ ÿçûêà äåéñòâèé [2]. Íîâàÿ âåðñèÿ ñèñòåìû èíñåð-
öèîííîãî ìîäåëèðîâàíèÿ IMS [19] ñòðîèòñÿ êàê ñðåäà äëÿ ðàçðàáîòêè
èíñåðöèîííûõ ìàøèí.
ÎÏÈÑÀÍÈÅ ÌÎÄÅËÅÉ Â ÑÈÑÒÅÌÅ IMS
Îñíîâîé ïîñòðîåíèÿ èíñåðöèîííûõ ìîäåëåé ÿâëÿþòñÿ ëîêàëüíûå îïèñàíèÿ
� �� �x x P x x( ( ) ( ) ( ))� � [13, 20]. Îíè ïðåäñòàâëÿþò ëîêàëüíûå ñâîéñòâà ñèñ-
òåìû: åñëè äëÿ íåêîòîðîãî ñîñòîÿíèÿ s u u� �[ , , ]1 2 � ñèñòåìû ñ ïîãðóæåííûìè
â íåå àãåíòàìè u u1 2, , ... è íåêîòîðîãî íàáîðà çíà÷åíèé ïàðàìåòðîâ x ïðåäóñëî-
âèå �( )x íà ñîñòîÿíèè s èñòèííî, òî íà÷èíàåòñÿ ïðîöåññ P x( ) è ïîñëå åãî
óñïåøíîãî çàâåðøåíèÿ íà íîâîì ñîñòîÿíèè áóäåò èñòèííûì ïîñòóñëîâèå �( )x .
Âñå ñîñòîÿíèÿ ðàññìàòðèâàþòñÿ ñ òî÷íîñòüþ äî áèñèìóëÿöèîííîé ýêâèâàëåí-
òíîñòè è ìîãóò îòîæäåñòâëÿòüñÿ ñ ïîâåäåíèÿìè ñèñòåìû â ýòèõ ñîñòîÿíèÿõ.
Ëîêàëüíûå îïèñàíèÿ èìåþò íå òîëüêî ëîãè÷åñêóþ, íî è èìïåðàòèâíóþ ñåìàíòè-
êó. Êàæäîå èç íèõ îïðåäåëÿåò íåêîòîðûé íåäåòåðìèíèðîâàííûé îïåðàòîð íà
ìíîæåñòâå ñîñòîÿíèé ñèñòåìû, êîòîðûé ìîæíî âûïîëíÿòü, ïðèìåíÿÿ åãî ê òåêó-
ùåìó ñîñòîÿíèþ. Ñ ïîìîùüþ ýòîãî îïåðàòîðà îïðåäåëÿåòñÿ îòíîøåíèå ïåðåõî-
äîâ s s
a
� �� �. Äåéñòâèå a , îïðåäåëÿþùåå ïåðåõîä, ìîæåò áûòü ëîêàëüíûì îïèñà-
íèåì (êðóïíîøàãîâàÿ ñåìàíòèêà) èëè ïðîöåññîì P x( ) ñ ïîäñòàâëåííûìè çíà÷åíè-
ÿìè ïàðàìåòðîâ.  ýòîì ñëó÷àå ìîæíî ïåðåéòè îò îäíîãî ïåðåõîäà ê îäíîé èëè
íåñêîëüêèì ïîñëåäîâàòåëüíîñòÿì ïåðåõîäîâ, ðàññìàòðèâàÿ ìåëêîøàãîâóþ ñåìàí-
òèêó [21]. Â äàëüíåéøåì äëÿ ëîêàëüíûõ îïèñàíèé ñèñòåìû áóäåò ðàññìîòðåíà
êðóïíîøàãîâàÿ ñåìàíòèêà. Åñëè s — ñîñòîÿíèå ñèñòåìû, à Q — ìíîæåñòâî ëî-
êàëüíûõ îïèñàíèé, òî ñèñòåìà óðàâíåíèé
s B s B Qs
s s
B
� �
� ��
� . ,�
'
,
ïðåäñòàâëÿåò êðóïíîøàãîâóþ ñåìàíòèêó ñèñòåìû ëîêàëüíûõ îïèñàíèé.
Äëÿ ïîëíîãî çàäàíèÿ ìîäåëè îäíèõ ëîêàëüíûõ îïèñàíèé íåäîñòàòî÷íî. Îòìå-
òèì, ÷òî â ëîêàëüíûõ îïèñàíèÿõ íå ñóùåñòâóåò îãðàíè÷åíèé íà ïîñëåäîâàòåëüíîñ-
òè èõ ïðèìåíåíèÿ, ÷òî ïðèâîäèò ê ðàññìîòðåíèþ íåæåëàòåëüíûõ èñòîðèé è òðàññ.
Ñëåäóþùèé óðîâåíü îïèñàíèÿ ìîäåëè ñîñòîèò â îïðåäåëåíèè îòíîøåíèÿ ñëåäîâà-
íèÿ íà ìíîæåñòâå ëîêàëüíûõ îïèñàíèé. Ýòî îòíîøåíèå ìîæíî ââåñòè ïóòåì îïðå-
äåëåíèÿ äîïîëíèòåëüíûõ óïðàâëÿþùèõ àòðèáóòîâ è óñëîâèé íà íèõ, îãðàíè÷èâà-
þùèõ óñëîâèÿ ïðèìåíåíèÿ ëîêàëüíûõ îïèñàíèé. Íåäîñòàòêîì òàêîãî îïèñàíèÿ ÿâ-
ëÿåòñÿ íåîáõîäèìîñòü ðàçäåëåíèÿ îñíîâíûõ è âñïîìîãàòåëüíûõ àòðèáóòîâ
óïðàâëåíèÿ. Êðîìå òîãî, óñëîæíÿþòñÿ ñîáñòâåííî ñàìè ëîêàëüíûå îïèñàíèÿ.
 ñèñòåìå VRS èñïîëüçóþòñÿ ñïåöèàëüíûå ñòðóêòóðû óïðàâëåíèÿ ïîèñêîì (guided
search), îäíàêî è îíè ñïåöèôè÷íû è íå ïîçâîëÿþò ïîëíîñòüþ ðåøèòü ïðîáëåìû.
 ïîñëåäíåå âðåìÿ â ñèñòåìå VRS äëÿ çàäàíèÿ îòíîøåíèÿ ñëåäîâàíèÿ èñïîëüçóåò-
8 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2015, òîì 51, ¹ 1
ñÿ ÿçûê UCM, ðàçðàáîòàííûé îðãàíèçàöèåé ITU, êàê îäèí èç ÿçûêîâ äëÿ ôîðìàëè-
çàöèè òðåáîâàíèé ê ïðîãðàììíûì ñèñòåìàì [22]. Ôîðìàëüíàÿ ñåìàíòèêà ÿçûêà
UCM ïîñòðîåíà â ðàáîòå [23]. Ñåìàíòèêà ïëîñêèõ êàðò è ñòàáîâ ïðåäñòàâëåíà
ñ ïîìîùüþ èíñåðöèîííûõ ìîäåëåé â ðàáîòàõ [24, 25].
 ñèñòåìå IMS âåðõíèì óðîâíåì îïèñàíèÿ ìîäåëè ÿâëÿåòñÿ óïðàâëÿþùàÿ
ñèñòåìà, êîòîðàÿ îïðåäåëÿåò ïîðÿäîê ïðèìåíåíèÿ ëîêàëüíûõ îïèñàíèé áàçîâîé
ñèñòåìû. Óïðàâëÿþùóþ ñèñòåìó ìîæíî çàäàòü ñèñòåìîé óðàâíåíèé â ðàñøèðåí-
íîé àëãåáðå ïîâåäåíèé, â êîòîðîé ïîìèìî îñíîâíûõ îïåðàöèé è ôóíêöèé èñïîëü-
çóþòñÿ ôóíêöèè ïîãðóæåíèÿ äëÿ ðàçëè÷íûõ ñðåä [20]. Îñîáåííîñòü óïðàâëÿþùåé
ñèñòåìû çàêëþ÷àåòñÿ â òîì, ÷òî âî ìíîæåñòâî åå äåéñòâèé âõîäÿò ëîêàëüíûå
îïèñàíèÿ äëÿ áàçîâîé ñèñòåìû. Ñîñòîÿíèå óïðàâëÿþùåé ñèñòåìû ïðåäñòàâëÿ-
åòñÿ âûðàæåíèåì U S[ ], ãäå U — ñîñòîÿíèå óïðàâëÿþùåé ñèñòåìû, à S — ñîñòî-
ÿíèå áàçîâîé ñèñòåìû, îïðåäåëåííîé ìíîæåñòâîì ëîêàëüíûõ îïèñàíèé Q. Îòíî-
øåíèå ïåðåõîäîâ äëÿ ñèñòåìû ñ óïðàâëåíèåì çàäàäèì ïðàâèëàìè
U U
U S U S
a Q
a
a
� �� �
� �� �
�
[ ] [ ]
,
U U S S
U S U S
a Q
a a
a
� �� � � �� �
� �� � �
,
[ ] [ ]
.
Äîïóñòèì, ÷òî ïåðåõîäû ñ äåéñòâèÿìè, îòëè÷íûìè îò ëîêàëüíûõ îïèñàíèé
áàçîâîé ñèñòåìû, óïðÿòàíû, ò.å. ïåðâîå ïðàâèëî çàìåíåíî ïðàâèëîì
U U
U S U S
a Q
a
� �� �
��� �
�
[ ] [ ]
.
Òîãäà âíåøíèé íàáëþäàòåëü íå çàìåòèò ðàçíèöû ìåæäó ôóíêöèîíèðîâàíèåì
áàçîâîé ñèñòåìû ñ óïðàâëåíèåì è áåç íåãî. Îí óâèäèò òîëüêî òðàññû òîé æå
ñàìîé áàçîâîé ñèñòåìû. Ïðè ýòîì ñ èñïîëüçîâàíèåì óïðàâëÿþùåé ñèñòåìû èõ
ìîæåò áûòü ìåíüøå, à òàêæå âîçìîæíû òóïèêîâûå ñîñòîÿíèÿ, êîòîðûõ íå ñó-
ùåñòâóåò äëÿ áàçîâîé ñèñòåìû. Óïðàâëÿþùàÿ ñèñòåìà êàê ñðåäà èìååò äîñòóï
ê ñîñòîÿíèþ áàçîâîé ñèñòåìû è àíàëèçèðóåò åå ñîñòîÿíèÿ òàê æå, êàê èíñåð-
öèîííàÿ ìàøèíà ðåàëüíîãî âðåìåíè. Òàêèå ìàøèíû ìîæíî èñïîëüçîâàòü êàê
óïðàâëÿþùèå ñèñòåìû. Îäíàêî äëÿ ãåíåðàöèè òðàññ íóæåí åùå îäèí óðîâåíü
óïðàâëåíèÿ — àíàëèòè÷åñêàÿ èíñåðöèîííàÿ ìàøèíà, îïèñàííàÿ äàëåå.
ÓÏÐÀÂËÅÍÈÅ ÌÎÄÅËßÌÈ Â ÑÈÑÒÅÌÅ IMS
Äëÿ ðàçðàáîòêè óïðàâëÿþùèõ êîìïîíåíòîâ èíñåðöèîííûõ ìîäåëåé â ñèñòåìå
IMS èñïîëüçóåòñÿ ÿçûê LiveUCM-IMS (â äàëüíåéøåì LiveUCM). Îí èìååò
äâà ïðåäñòàâëåíèÿ: àëãåáðàè÷åñêîå è ãðàôè÷åñêîå.  îñíîâå ñåìàíòèêè
LiveUCM ëåæàò îñíîâíûå ñåìàíòè÷åñêèå êîíñòðóêöèè ÿçûêà UCM, âûðàæåí-
íûå â òåðìèíàõ èíñåðöèîííîãî ìîäåëèðîâàíèÿ. ßçûê UCM íà àáñòðàêòíîì
óðîâíå ìîæíî ðàññìàòðèâàòü êàê óäà÷íóþ èíòåãðàöèþ äâóõ êîíöåïöèé: ïà-
ðàëëåëèçì â ñåòÿõ Ïåòðè è èäåÿ ìîáèëüíûõ àìáèåíòîâ [9]. ßçûê LiveUCM äî-
ïîëíÿåò ýòè äâå êîíöåïöèè èäååé ìíîãîóðîâíåâîé ñðåäû.
Îïèñàíèå óïðàâëÿþùåé ñèñòåìû â LiveUCM, êàê è â UCM, ñîñòîèò èç ìíî-
æåñòâà âëîæåííûõ êàðò. Íà êàæäîé êàðòå èçîáðàæåíà ñåòü íàïðàâëåííûõ ïóòåé.
Ïðèìåð òàêîé ñèñòåìû, ñîñòîÿùåé èç òðåõ êàðò: îäíîé êàðòû âåðõíåãî óðîâíÿ è
äâóõ âëîæåííûõ â íåå êàðò, ïðåäñòàâëåí íà ðèñ. 1. Êàæäûé ïóòü èìååò íà÷àëüíóþ
âåðøèíó (ðèñ. 2, à), ïðè÷åì èõ ìîæåò áûòü íåñêîëüêî. Êîíå÷íûå ìàêñèìàëüíûå
ïóòè çàêàí÷èâàþòñÿ êîíå÷íûìè âåðøèíàìè, ïðåäñòàâëåííûìè æèðíûìè êîðîòêè-
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2015, òîì 51, ¹ 1 9
ìè ëèíèÿìè, îðòîãîíàëüíûìè ïóòÿì,
êîòîðûå îíè çàâåðøàþò (ðèñ. 2, b).
Èç íà÷àëüíîé âåðøèíû âûõîäèò,
à â êîíå÷íóþ âõîäèò òîëüêî îäèí ïóòü.
Ïóòè ìîãóò ðàçâåòâëÿòüñÿ è ñëè-
âàòüñÿ (fork and join). Ñóùåñòâóåò äâà
âèäà âåòâëåíèÿ è ñëèÿíèÿ: ïàðàëëåëü-
íûå è àëüòåðíàòèâíûå. Ïàðàëëåëüíûå
âåòâëåíèÿ (AndFork, ðèñ. 2, ñ) è ñëèÿ-
íèÿ (AndJoin, ðèñ. 2, d) îáîçíà÷åíû
æèðíûìè ëèíèÿìè, îðòîãîíàëüíûìè
ïóòÿì. Ó ïàðàëëåëüíîãî âåòâëåíèÿ ñó-
ùåñòâóåò îäèí âõîäíîé ïóòü è íå-
ñêîëüêî âûõîäíûõ. Ïàðàëëåëüíîå ñëè-
ÿíèå ìîæåò èìåòü íåñêîëüêî âõîäíûõ
ïóòåé, íî òîëüêî îäèí âûõîäíîé.
Ó àëüòåðíàòèâíûõ âåòâëåíèÿ (OrFork,
ðèñ. 2, e) è ñëèÿíèÿ (OrJoin, ðèñ. 2, f )
òàêàÿ æå ñòðóêòóðà, êàê è ó ïàðàëëåëü-
íûõ (âåòâëåíèå èìååò îäèí âõîäíîé
ïóòü è íåñêîëüêî âûõîäíûõ, ñëèÿíèå — íåñêîëüêî âõîäíûõ è îäèí âûõîäíîé ïóòü).
Àëüòåðíàòèâíûå âåòâëåíèÿ è ñëèÿíèÿ ïðåäñòàâëåíû òî÷êàìè íà ïóòÿõ.
Êðîìå âåòâëåíèé è ñëèÿíèé íà ïóòÿõ èìåþòñÿ äâà âèäà ñèìâîëîâ: îáÿçàòåëüñòâî,
îáîçíà÷åííîå êðåñòèêîì (Responsibility, ðèñ. 2, g), è ñòàá, îáîçíà÷åííûé ðîìáîì (Stub,
ðèñ. 2, h). Ñèìâîëû îáÿçàòåëüñòâ èìåþò ïî îäíîìó âõîäíîìó è âûõîäíîìó ïóòè, ñèì-
âîë ñòàáà ìîæåò èìåòü ïî íåñêîëüêó âõîäíûõ è âûõîäíûõ ïóòåé. Ñ êàæäûì îáÿ-
çàòåëüñòâîì àññîöèèðîâàíî íåêîòîðîå ëîêàëüíîå îïèñàíèå ñèñòåìû ëîêàëüíûõ
îïèñàíèé, êîòîðûå, â îñíîâíîì, îòíîñÿòñÿ ê áàçîâîé ñèñòåìå, õîòÿ â íåêîòîðûõ
ñëó÷àÿõ — è ê óïðàâëåíèþ.
Ïóòè ìîãóò ïåðåõîäèòü èç îäíîé êàðòû â äðóãóþ, ðàñïîëîæåííóþ íà òîì æå
èëè ñìåæíîì óðîâíå (âåðõíåì èëè íèæíåì) (ðèñ. 3). Òàêèì îáðàçîì, ïóòè ñîåäè-
íÿþò âåðøèíû, íàõîäÿùèåñÿ â ðàçëè÷íûõ êàðòàõ.
Ñ êàæäûì ñòàáîì àññîöèèðîâàíà íåêîòîðàÿ êàðòà, íà êîòîðóþ ññûëàåòñÿ
äàííûé ñòàá, âõîäíûå ïóòè ïîñëåäíåãî ñâÿçàíû ñ íà÷àëüíûìè, à âûõîäíûå
ïóòè — ñ êîíå÷íûìè âåðøèíàìè àññîöèèðîâàííîé êàðòû.
10 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2015, òîì 51, ¹ 1
Ðèñ. 1
vans # councilor
horticulturist
Feynman
Xmases
convicting
s1
chars
cankering
s2
s3
s4
shilled
OUT1
OUT1
OUT1
IN1
IN1
OUT1
pages
sapience
IN1
thanksgivinghorticulturist
lollipopfacelift mutiny
bifocals
IN1
bottom
squab
toniest
arce
IN1
UCM example
unrestrained # serge
numbling
veggleOUT1
maneuver
Ðèñ. 2
a b
dc
g h
fe
IN1 OUT1
StartPoint EndPoint
AndFork AndJoin
OrFork
OrJoin
Responsibility Stub
Èíòóèòèâíóþ ñåìàíòèêó
ÿçûêà LiveUCM ìîæíî ïðåäñòà-
âèòü ñëåäóþùèì îáðàçîì. Â íà-
÷àëüíûé ìîìåíò âðåìåíè àêòèâ-
íûìè ÿâëÿþòñÿ âñå íà÷àëüíûå
âåðøèíû êàæäîé êàðòû, êðîìå àñ-
ñîöèèðîâàííîé ñî ñòàáàìè. Äàëåå
àêòèâíûå òî÷êè äâèæóòñÿ ïî ñâî-
èì ïóòÿì. Ñîñòîÿíèå ñèñòåìû èç-
ìåíÿåòñÿ òîëüêî, êîãäà àêòèâíûå
òî÷êè íà ïóòÿõ ïðîõîäÿò ÷åðåç
òî÷êè ïåðåõîäîâ. Ê íèì îòíîñÿòñÿ: îáÿçàòåëüñòâà, âåòâëåíèÿ, ñëèÿíèÿ, òî÷êè a —
âûõîäû èç êàðòû íèæíåãî óðîâíÿ íà âåðõíèé óðîâåíü, òî÷êè b — âõîäû â êàðòû íè-
æíåãî óðîâíÿ (ñì. ðèñ. 3), ñòàáû, íà÷àëüíûå è êîíå÷íûå âåðøèíû.
Âñå òî÷êè ïåðåõîäîâ è êàðòû èìåþò èìåíà, óíèêàëüíûå âíóòðè îäíîé êàðòû.
Äëÿ òîãî ÷òîáû ðàçëè÷àòü èìåíà â ðàçëè÷íûõ êàðòàõ, ê íèì äîñòàòî÷íî äîáàâèòü
èìåíà êàðò, ëåæàùèõ íà ïóòè ê èìåíóåìûì ýëåìåíòàì îò êàðòû âåðõíåãî óðîâíÿ.
Èçìåíåíèå ñîñòîÿíèé ñèñòåìû ïðîèñõîäèò ïî ïðàâèëó èíòåðëèâèíãà: â êàæ-
äûé ìîìåíò âðåìåíè ïåðåõîä ìîæåò ïðîèçîéòè â ðåçóëüòàòå ñðàáàòûâàíèÿ òîëü-
êî îäíîé òî÷êè ïåðåõîäà.
Ïðè ïðîõîæäåíèè àêòèâíîé òî÷êè ÷åðåç îáÿçàòåëüñòâî ñèñòåìà äåëàåò ïîïûòêó
âûïîëíèòü ëîêàëüíîå îïèñàíèå, àññîöèèðîâàííîå ñ äàííûì îáÿçàòåëüñòâîì. Åñëè
ýòî óäàåòñÿ, òî ëîêàëüíîå îïèñàíèå âûïîëíÿåòñÿ è èçìåíÿåòñÿ ñîñòîÿíèå áàçîâîé
ñèñòåìû. Åäèíñòâåííûé ïóòü, âûõîäÿùèé èç òî÷êè îáÿçàòåëüñòâà, àêòèâèçèðóåòñÿ,
ò.å. íà íåì ïîÿâëÿåòñÿ àêòèâíàÿ òî÷êà, ïðîøåäøàÿ ÷åðåç äàííîå îáÿçàòåëüñòâî.
 ïðîòèâíîì ñëó÷àå àêòèâíàÿ òî÷êà îñòàíàâëèâàåòñÿ ïåðåä îáÿçàòåëüñòâîì è ïåðå-
õîäèò â ñîñòîÿíèå îæèäàíèÿ, ïåðåõîäû ñèñòåìû âûïîëíÿþòñÿ â ðåçóëüòàòå ïðî-
õîæäåíèÿ äðóãèõ àêòèâíûõ òî÷åê ÷åðåç òî÷êè ïåðåõîäîâ. Êîãäà âñå àêòèâíûå
òî÷êè êàæäîé êàðòû íàõîäÿòñÿ â ñîñòîÿíèè îæèäàíèÿ, ñèñòåìà ïîïàäàåò â òóïè-
êîâîå ñîñòîÿíèå (dead lock).
Ïðè ïðîõîæäåíèè ïàðàëëåëüíîãî âåòâëåíèÿ àêòèâèçèðóþòñÿ âñå âûõîäíûå
ïóòè. Ïàðàëëåëüíîå ñëèÿíèå ñèíõðîíèçèðóåò äâèæåíèå àêòèâíûõ òî÷åê. Íà êàæ-
äîì ïóòè ñî âðåìåíåì íàêàïëèâàåòñÿ íåêîòîðîå êîëè÷åñòâî êîíòðîëüíûõ òî÷åê,
êîòîðûå íàõîäÿòñÿ â ñîñòîÿíèè îæèäàíèÿ. Êîãäà íà êàæäîì âõîäíîì ïóòè ïàðàë-
ëåëüíîãî âåòâëåíèÿ èìååòñÿ ïî êðàéíåé ìåðå îäíà àêòèâíàÿ òî÷êà, êîòîðàÿ íàõî-
äèòñÿ â ñîñòîÿíèè îæèäàíèÿ, àêòèâèçèðóåòñÿ âûõîäíîé ïóòü è íà âñåõ âõîäíûõ
ïóòÿõ ñëèÿíèÿ êîëè÷åñòâî àêòèâíûõ òî÷åê óìåíüøàåòñÿ íà åäèíèöó.
Ïðîõîæäåíèå àëüòåðíàòèâíîãî âåòâëåíèÿ âûïîëíÿåòñÿ ïî ñëåäóþùåìó àëãî-
ðèòìó. Îïðåäåëÿþòñÿ âñå òî÷êè ïåðåõîäîâ, îòëè÷íûå îò àëüòåðíàòèâíûõ âåòâëå-
íèé, êîòîðûå ìîæíî äîñòè÷ü, ïðîõîäÿ òîëüêî ÷åðåç àëüòåðíàòèâíûå âåòâëåíèÿ
è ñëèÿíèÿ. Âûáèðàåòcÿ íåäåòåðìèíèðîâàííûì îáðàçîì îäíà èç ïîëó÷åííûõ òî÷åê
ïåðåõîäîâ. Ïðè ýòîì çàïðåùàåòñÿ âûáèðàòü îáÿçàòåëüñòâî, ëîêàëüíîå îïèñàíèå êî-
òîðîãî íåïðèìåíèìî ê òåêóùåìó ñîñòîÿíèþ áàçîâîé ñèñòåìû. Åñëè òàêóþ òî÷êó
âûáðàòü íåëüçÿ, òî àêòèâíàÿ òî÷êà ïåðåõîäèò â ñîñòîÿíèå îæèäàíèÿ. Ïóòü, ïî êî-
òîðîìó àêòèâíàÿ òî÷êà ïðîõîäèò ê âûáðàííîé òî÷êå ïåðåõîäà, òàêæå âûáèðàåòñÿ
íåäåòåðìèíèðîâàííûì îáðàçîì. Íåîäíîçíà÷íîñòü âûáîðà ýòîãî ïóòè îïðåäåëÿåòñÿ
âîçìîæíûìè òî÷êàìè àëüòåðíàòèâíîãî ñëèÿíèÿ. Ïðè äâèæåíèè àêòèâíîé òî÷êè îò
àëüòåðíàòèâíîãî âåòâëåíèÿ äî âûáðàííîé òî÷êè ïåðåõîäà âñå äðóãèå àêòèâíûå
òî÷êè ïðèîñòàíàâëèâàþòñÿ. Êîãäà àêòèâíàÿ òî÷êà äîñòèãàåò âûáðàííîé òî÷êè ïå-
ðåõîäà, ïîñëåäíèé âûïîëíÿåòñÿ, ò.å. ïðîèñõîäèò ñîîòâåòñòâóþùåå èçìåíåíèå ñî-
ñòîÿíèÿ ñèñòåìû. Àëüòåðíàòèâíîå ñëèÿíèå ìîæåò áûòü ïðîéäåíî âñåãäà.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2015, òîì 51, ¹ 1 11
a
a
b
b
Ðèñ. 3
Âûõîä èç êàðòû íèæíåãî óðîâíÿ íà âåðõíèé è âõîä â êàðòó íèæíåãî óðîâíÿ
âîçìîæíû âñåãäà.
Êîãäà àêòèâíàÿ òî÷êà äîñòèãàåò ñòàáà, ïîñëåäíèé çàìåíÿåòñÿ êîïèåé àññîöè-
èðîâàííîé ñ íèì êàðòû. Ïðè ýòîì íà÷àëüíûå âåðøèíû àññîöèèðîâàííîé êàðòû
ñòàíîâÿòñÿ òî÷êàìè âõîäà, à âñå êîíå÷íûå âåðøèíû — òî÷êàìè âûõîäà. Âñå
âõîäíûå ïóòè ñâÿçûâàþòñÿ ñ ñîîòâåòñòâóþùèìè òî÷êàìè âõîäà àññîöèèðîâàí-
íîé êàðòû, à âñå âûõîäíûå — ñ ñîîòâåòñòâóþùèìè òî÷êàìè âûõîäà. Ïîñëå ïðî-
öåññ ïðîäîëæàåòñÿ â ñîîòâåòñòâèè ñ îïèñàííûìè âûøå ïðàâèëàìè.
 íà÷àëüíûé ìîìåíò âðåìåíè àêòèâíûìè ÿâëÿþòñÿ îòðåçêè ïóòåé, âûõîäÿ-
ùèõ èç íà÷àëüíûõ âåðøèí âñåõ êàðò, êîòîðûå íå àññîöèèðîâàíû ñî ñòàáàìè.
Àêòèâíûå òî÷êè íå ðàçëè÷àþòñÿ è èõ ìåñòîïîëîæåíèå íà îòðåçêå ïóòè ìåæäó
äâóìÿ òî÷êàìè ïåðåõîäîâ íåñóùåñòâåííî. Ïîýòîìó ñîñòîÿíèå ñèñòåìû óïðàâëåíèÿ
îäíîçíà÷íî îïðåäåëÿåòñÿ êîëè÷åñòâîì àêòèâíûõ òî÷åê íà êàæäîì îòðåçêå, ñîåäè-
íÿþùåì äâå áëèæàéøèå òî÷êè ïåðåõîäîâ. À ñîñòîÿíèå âñåé ñèñòåìû îïðåäåëÿåòñÿ
ñîñòîÿíèÿìè ñèñòåì óïðàâëåíèÿ è áàçîâîé.
ÔÎÐÌÀËÜÍÀß ÑÅÌÀÍÒÈÊÀ LiveUCM
Ñòðóêòóðà ñðåäû. Êàæäàÿ êàðòà ïðåäñòàâëÿåò ñîáîé àòðèáóòíóþ ñðåäó äëÿ
ïîãðóæåííûõ â íåå àãåíòîâ. Ñèãíàòóðà êàðòû âêëþ÷àåò êîíå÷íîå ìíîæåñòâî T
ñèìâîëüíûõ êîíñòàíò äëÿ îáîçíà÷åíèÿ èìåí òî÷åê ïåðåõîäà è îòíîøåíèå ñëå-
äîâàíèÿ Succ T
2 , êîòîðîå îïèñûâàåò ñòðóêòóðó ïóòåé êàðòû: ( , )a b Succ
òîãäà è òîëüêî òîãäà, êîãäà ñóùåñòâóåò ïóòü èç òî÷êè ïåðåõîäà a â òî÷êó ïå-
ðåõîäà b, íà êîòîðîì íå èìååòñÿ äðóãèõ òî÷åê ïåðåõîäà. Ñòàáû îòëè÷àþòñÿ îò
äðóãèõ òî÷åê ïåðåõîäà òåì, ÷òî èõ âõîäíûå è âûõîäíûå ïóòè óïîðÿäî÷åíû.
Ïîýòîìó êàæäîìó ñòàáó b ñîïîñòàâèì åùå íåñêîëüêî òî÷åê ïåðåõîäà: òî÷êè
âõîäà â ñòàá ( : )1 b , ( : ),2 b � è òî÷êè âûõîäà èç ñòàáà ( : ), ( : ),b b1 2 � Îòíîøå-
íèå ñëåäîâàíèÿ åñòü ñòàòè÷åñêàÿ ñòðóêòóðà äàííûõ, êîòîðàÿ ìåíÿåòñÿ òîëüêî
ïðè âõîäå â ñòàá. Ìíîæåñòâî òî÷åê ïåðåõîäà êàðòû âêëþ÷àåò è âñå òî÷êè ïå-
ðåõîäà êàæäîé âëîæåííîé â íåå êàðòû.
Äëÿ îáîçíà÷åíèÿ òèïîâ òî÷åê ïåðåõîäîâ èñïîëüçóåòñÿ äðóãàÿ ñåðèÿ ñèìâîëü-
íûõ êîíñòàíò: Resp (îáÿçàòåëüñòâî), OrFork (àëüòåðíàòèâíîå âåòâëåíèå), AndFork
(ïàðàëëåëüíîå âåòâëåíèå), OrJoin (àëüòåðíàòèâíîå ñëèÿíèå), AndJoin (ïàðàëëåëü-
íîå ñëèÿíèå), MapOut (âûõîä èç êàðòû íèæíåãî óðîâíÿ íà âåðõíèé èëè âûõîä èç
ñòàáà), MapIn (âõîä â êàðòó íèæíåãî óðîâíÿ èëè âõîä â ñòàá), Stub (ñòàá), StubIn
(òî÷êà âõîäà â ñòàá), StubOut (òî÷êà âûõîäà èç ñòàáà), Init (íà÷àëüíàÿ âåðøèíà),
Termnl (êîíå÷íàÿ âåðøèíà). Îíè ÿâëÿþòñÿ çíà÷åíèÿìè ïåðå÷èñëèìîãî òèïà
PoinType. Àòðèáóò PT T PointType: � ïîçâîëÿåò îïðåäåëèòü òèï òî÷êè ïåðåõîäà.
Âìåñòî ôîðìóëû PT b t( ) � èñïîëüçóåòñÿ áîëåå êîðîòêîå âûðàæåíèå t b( ).
Åñëè ( , )a b Succ
, òî òî÷êó a áóäåì íàçûâàòü òî÷êîé âõîäà äëÿ b, à òî÷êó b —
òî÷êîé âûõîäà äëÿ a. Îòíîøåíèå ñëåäîâàíèÿ äîëæíî óäîâëåòâîðÿòü ñëåäóþùèì
òðåáîâàíèÿì:
— êàæäîå îáÿçàòåëüñòâî (òî÷êè òèïà MapOut è MapIn) èìååò òî÷íî ïî îä-
íîé òî÷êå âõîäà è âûõîäà;
— êàæäîå âåòâëåíèå èìååò òî÷íî îäíó òî÷êó âõîäà è ïî êðàéíåé ìåðå äâå
òî÷êè âûõîäà;
— êàæäîå ñëèÿíèå èìååò ïî êðàéíåé ìåðå äâå òî÷êè âõîäà è òî÷íî îäíó òî÷-
êó âûõîäà;
— íà÷àëüíàÿ âåðøèíà íå èìååò òî÷åê âõîäà è èìååò òî÷íî îäíó òî÷êó
âûõîäà;
— êîíå÷íàÿ âåðøèíà íå èìååò òî÷åê âûõîäà è èìååò òî÷íî îäíó òî÷êó
âõîäà;
12 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2015, òîì 51, ¹ 1
— òî÷êîé âûõîäà äëÿ òî÷êè âõîäà â ñòàá åñòü ñòàá, à òî÷êà âûõîäà èç ñòàáà
èìååò ñòàá â êà÷åñòâå âõîäà;
— ïóñòü StubIn b( ) — ìíîæåñòâî òî÷åê âõîäà â ñòàá b, StubOut b( ) — ìíîæåñ-
òâî òî÷åê âûõîäà èç ñòàáà b. Òîãäà
StubIn b i b i m StubOut b b i i( ) ( : ) | , , , , ( ) ( : ) | ,� � � �{ } {1 2 1� 2, ,� n},
ãäå m è n — ñîîòâåòñòâåííî ÷èñëî íà÷àëüíûõ è êîíå÷íûõ âåðøèí êàðòû, àñ-
ñîöèèðîâàííîé ñî ñòàáîì b.
Ñîñòîÿíèå êàðòû êàê ñðåäû îïèñûâàåòñÿ ôóíêöèîíàëüíûì àòðèáóòîì
active Succ N: � , ãäå N — ìíîæåñòâî öåëûõ íåîòðèöàòåëüíûõ ÷èñåë, è ñîñòîÿ-
íèÿìè âñåõ âëîæåííûõ â íåå êàðò. Ðàâåíñòâî active a b n( , ) � îçíà÷àåò, ÷òî íà îò-
ðåçêå ìåæäó a è b íàõîäèòñÿ â òî÷íîñòè n àêòèâíûõ òî÷åê.
Àãåíòû.  êà÷åñòâå àãåíòîâ, ïîãðóæåííûõ â ñðåäó êàðòû, ðàññìàòðèâàþòñÿ
àêòèâíûå òî÷êè, äâèæóùèåñÿ ïî åå ïóòÿì, à òàêæå êàðòû ñëåäóþùåãî óðîâíÿ,
âëîæåííûå (ïîãðóæåííûå) â äàííóþ êàðòó. Â òåêóùèé ìîìåíò âðåìåíè àêòèâíàÿ
òî÷êà íàõîäèòñÿ íà íåêîòîðîì îòðåçêå ïóòè ìåæäó äâóìÿ òî÷êàìè ïåðåõîäîâ:
òî÷êîé âõîäà è âûõîäà. Ïîâåäåíèå àãåíòà, íàõîäÿùåãîñÿ íà îòðåçêå ( , )a b , îòî-
æäåñòâëÿåòñÿ ñ åãî ñîñòîÿíèåì è îáîçíà÷àåòñÿ behavior a b( , ), à äåéñòâèå, êîòîðîå
âûïîëíÿåòñÿ ïðè ïðîõîæäåíèè òî÷êè b èç îòðåçêà ( , )a b , îáîçíà÷àåòñÿ
action a b( , ). Åñëè òèï âåðøèíû b åñòü îáÿçàòåëüñòâî, òî action a b( , ) åñòü ëîêàëü-
íîå îïèñàíèå, ñîîòâåòñòâóþùåå äàííîìó îáÿçàòåëüñòâó, âî âñåõ îñòàëüíûõ ñëó-
÷àÿõ ýòî ìîæåò áûòü ëþáûì âûðàæåíèåì, êîòîðîå ñîäåðæèò ïîëíóþ èíôîðìà-
öèþ î ãðàíèöàõ èíòåðâàëà a è b. Ïîâåäåíèÿ àãåíòîâ ñâÿçàíû ñîîòíîøåíèÿìè àë-
ãåáðû ïîâåäåíèé, êîòîðûå îäíîçíà÷íî èõ îïðåäåëÿþò êàê íàèìåíüøåå ðåøåíèå
ñîîòâåòñòâóþùåé ñèñòåìû óðàâíåíèé. Âîò ýòè ñîîòíîøåíèÿ:
Resp b b c Succ behavior a b action a b behav( ) ( , ) ( , ) ( , ).�
� � ior b c( , ),
OrFork behavior a b action a b behavior b c
b c
� �( , ) ( , ). ( , )
( , )
�
Succ
,
AndFork behavior a b action a b behav
b c Succ
� �
( , ) ( , ).
( , )
� ior b c( , )
(cèìâîë
x X
u x
� ( ) îáîçíà÷àåò ïàðàëëåëüíóþ êîìïîçèöèþ ïîâåäåíèé u x( ) ïî
âñåì ýëåìåíòàì x X
);
OrJoin b b c Succ behavior a b action a b beh( ) ( , ) ( , ) ( , ).�
� � avior b c( , ),
AndJoin b b c Succ behavior a b action a b be( ) ( , ) ( , ) ( , ).�
� � havior b c( , )
(âñå àêòèâíûå òî÷êè íà âõîäå ïàðàëëåëüíîãî ñëèÿíèÿ ñòðåìÿòñÿ ïåðåéòè â
òî÷êó c, îäíàêî, êàê áóäåò âèäíî äàëüøå, ñðåäà ðàçðåøàåò òîëüêî îäíîé òî÷êå
(íå âàæíî êàêîé) ïåðåéòè ÷åðåç ïàðàëëåëüíîå ñëèÿíèå, îñòàëüíûå (ïî îäíîé
äëÿ êàæäîãî âõîäíîãî ïóòè) ïðåêðàùàþò ñâîå äâèæåíèå);
MapOut b b c Succ behavior a b action a b beh( ) ( , ) ( , ) ( , ).�
� � avior b c( , ),
MapIn b b c Succ behavior a b action a b beha( ) ( , ) ( , ) ( , ).�
� � vior b c( , )
(ïîâåäåíèå àãåíòà ïðè ïåðåõîäå èç îäíîé êàðòû â äðóãóþ íè÷åì íå îòëè÷àåò-
ñÿ îò ïåðåõîäîâ àãåíòà ÷åðåç îáÿçàòåëüñòâà èëè ñëèÿíèÿ);
Termnl b behavior a b action a b( ) ( , ) ( , ) .� � � .
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2015, òîì 51, ¹ 1 13
Çàìåòèì, ÷òî ïðèâåäåííûå ñîîòíîøåíèÿ îïðåäåëÿþò ïðàâèëà ïåðåõîäîâ
àãåíòîâ. Íàïðèìåð, ïåðâîå ñîîòíîøåíèå ìîæíî çàïèñàòü â âèäå
Resp b b c Succ behavior a b b
action a b
( ) ( , ) ( , )
( , )
�
� � ����� ehavior b c( , ) .
Óðàâíåíèé äëÿ ïðîõîæäåíèÿ ñòàáà íå ñóùåñòâóåò. Ïîñëåäíåå îáúÿñíÿåòñÿ
òåì, ÷òî ïîäñòàíîâêó äåëàåò ñðåäà. Â ðåçóëüòàòå ýòîé ïîäñòàíîâêè ìåíÿåòñÿ
ñòðóêòóðà êàðòû è òèï âòîðîé âåðøèíû èíòåðâàëà, íà êîòîðîì íàõîäèòñÿ àêòèâ-
íàÿ òî÷êà, òàêæå ìîæåò èçìåíèòüñÿ. Ïîýòîìó, äîéäÿ äî ñòàáà, àêòèâíàÿ òî÷êà
îæèäàåò èçìåíåíèÿ ñòðóêòóðû êàðòû íà îäíîì èç åãî âõîäîâ.
Ôóíêöèÿ ïîãðóæåíèÿ. Ïåðåéäåì òåïåðü ê ðàññìîòðåíèþ îáùèõ ïðàâèë âû-
÷èñëåíèÿ ôóíêöèè ïîãðóæåíèÿ äëÿ êàðò, ðàññìàòðèâàåìûõ êàê ñðåäû. Òåêóùåå ñî-
ñòîÿíèå êàðòû ïðåäñòàâëÿåòñÿ âûðàæåíèåì M u u[ , , ]1 2 � , ãäå M — íåðàçëîæèìîå
ñîñòîÿíèå êàðòû, ò.å. íàáîð çíà÷åíèé åå àòðèáóòîâ, u u1 2, ,� — ñîñòîÿíèÿ àêòèâ-
íûõ òî÷åê è âëîæåííûõ êàðò, ïîãðóæåííûõ â êàðòó Ì . Ôóíêöèÿ ïîãðóæåíèÿ êàð-
òû êîììóòàòèâíà. Ïîýòîìó, åñëè íåîáõîäèìî ïðèìåíèòü ïðàâèëî ïåðåõîäà äëÿ îä-
íîãî àãåíòà, åãî íóæíî ïåðåìåñòèòü íà ïîñëåäíåå ìåñòî è ïðèìåíèòü îäíî èç ïðà-
âèë ïåðåõîäà ê ñðåäå, ïðåäñòàâëåííîé â âèäå ( [ , , ])[ ] [ ]M u u u M u1 2 � � � .
Ôóíêöèÿ ïîãðóæåíèÿ äëÿ êàðòû ÿâëÿåòñÿ ïàðàëëåëüíûì ïîãðóæåíèåì. Ýòî
çíà÷èò, ÷òî M u M u[ , ] [ | | ]� �� . Äðóãîå ñâîéñòâî ôóíêöèè ïîãðóæåíèÿ — àääè-
òèâíîñòü: M u M u M[ ] [ ] [ ] � � � .
Èñïîëüçóÿ ýòè ñâîéñòâà, à òàêæå èçâåñòíûå ñâîéñòâà ïàðàëëåëüíîé êîìïîçè-
öèè, ïîëó÷àåì, ÷òî ñîñòîÿíèå êàðòû ìîæíî ïðèâåñòè ê âèäó M a ui i
i I
[ . ]
� �, ãäå
� åñòü M [ ]� èëè 0. Ñîñòîÿíèå M [ ]� ñîîòâåòñòâóåò ñëó÷àþ, êîãäà äëÿ âñåõ ïàð
( , )a b Succ
, active a b( , ) � 0 , ò.å. êàðòà M íå èìååò âëîæåííûõ êàðò è àêòèâ-
íûõ òî÷åê.
Ïðåäïîëîæèì, ÷òî ìíîæåñòâî T èìåí àêòèâíûõ òî÷åê è êàðò ìåíÿåòñÿ ñîîò-
âåòñòâóþùèì îáðàçîì ïðè êàæäîì ïîãðóæåíèè íîâîé êàðòû. Èíûìè ñëîâàìè,
åñëè M M N
a
� �� �[ ], ãäå N — íîâàÿ êàðòà, òî ïåðåä âûïîëíåíèåì ïåðåõîäà
M M
a
� �� � ê ìíîæåñòâó T èìåí òî÷åê ïåðåõîäà êàðòû M äîáàâëÿþòñÿ èìåíà òî-
÷åê ïåðåõîäà êàðòû N . Àíàëîãè÷íî ìåíÿåòñÿ è îòíîøåíèå ñëåäîâàíèÿ êàðòû M :
ê íåìó äîáàâëÿåòñÿ îòíîøåíèå ñëåäîâàíèÿ êàðòû N .
Ôóíêöèÿ ïîãðóæåíèÿ äëÿ äåéñòâèÿ x , ñîîòâåòñòâóþùåãî ïðîõîæäåíèþ àêòèâ-
íîé òî÷êè ÷åðåç îáÿçàòåëüñòâî, âåòâëåíèå, ñëèÿíèå èëè êîíå÷íóþ âåðøèíó M ,
îïðåäåëÿåòñÿ ïðàâèëîì
M M u u
M u M u
x x
x
� �� � � �� �
� �� � �
,
[ ] [ ]
.
Ïåðåõîä M M
x
� �� � êàðòû M çàäàåòñÿ ñ ïîìîùüþ ëîêàëüíûõ îïèñàíèé, çàâè-
ñÿùèõ îò òèïà âåðøèíû, êîòîðóþ ïðîõîäèò àêòèâíàÿ òî÷êà. Âîò ýòè îïèñàíèÿ:
�( , )(a b
active a b Resp b AndFork b OrJoin b Termnl( , ) ( ( ) ( ) ( )� � � � �0 ( ))b
�� �action a b( , )
active a b active a b( , ) : ( , )� � �1
�
� � c b c Succ active b c active b c(( , ) ( , ) : ( , ) )1
);
� ( , , )(a b c
active a b OrFork b( , ) ( )� � �0
( ( , ) ( , ) . ( ( , ). ))behavior a b action a b active b c u� �
14 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2015, òîì 51, ¹ 1
�� �action a b( , )
active a b active a b active b c active b c( , ) : ( , ) ( , ) : ( ,� � � �1 ) 1
);
� ( , , )(a b c
active a b AndFork b b c Succ( , ) ( ) (( , ) )� � �
�0
� � �
� � �a a b Succ active a b(( , ) ( , ) )0
�� �action a b( , )
active a b active a b( , ) : ( , )� � �1
� � �
� � � � �a a b Succ active a b active a b(( , ) ( , ) : ( , ) )1
) ;
Äëÿ ïåðåõîäîâ èç îäíîé êàðòû â äðóãóþ ïðèìåíÿþòñÿ èíûå ïðàâèëà:
M M N N u u
M N u M N u
x acti
x x x
x
� �� � � �� � � �� �
� �� � � �
�
, ,
[ [ ]] [ , ]
( on a b MapOut b( , ) ( ))� ,
M M N N u u
M N u M N u
x act
x x x
x
� �� � � �� � � �� �
� �� � � �
�
, ,
[ [ ]] [ [ ]]
( ion a b MapIn b b N( , ) ( ) )� �
.
Ëîêàëüíîå îïèñàíèå äëÿ ïåðåõîäîâ êàðòû èìååò âèä
�( , , )(a b c
active a b MapIn b b c Succ PointType c Stu( , ) ( ) ( , ) ( )� � �
� �0 b
�� �action a b( , )
active a b active a b active b c active b( , ) : ( , ) ( , ) : ( ,`� � � �1 c) 1
);
� ( , , )(a b c
active a b MapOut b b c Succ( , ) ( ) ( , )� � �
0
�� �action a b( , )
active a b active a b active b c active b c( , ) : ( , ) ( , ) : ( ,� � � �1 ) 1
) ;
Ïîÿâëåíèå àêòèâíîé òî÷êè ïåðåä âõîäîì â ñòàá ìîæåò ñòàòü ïðè÷èíîé âû-
ïîëíåíèÿ ïåðåõîäà ñðåäû, ïðè êîòîðîì ñòàá çàìåíÿåòñÿ àññîöèèðîâàííîé ñ íèì
êàðòîé. Ïðàâèëî ïåðåõîäà èìååò âèä
( ( , ) . ) ( , ) ( ) ( [ ] [ ,u action a b u b c Succ Stub c M u M u N� � �
� � � � ( )])c .
Êàðòà N c( ) ïîëó÷àåòñÿ èç êàðòû, àññîöèèðîâàííîé ñî ñòàáîì ñ, ïîäñòàíîâêîé
âåðøèí èç ìíîæåñòâà StubIn c( ) âìåñòî åå íà÷àëüíûõ âåðøèí è âåðøèí èç
ìíîæåñòâà StubOut c( ) âìåñòî åå êîíå÷íûõ âåðøèí ñ ó÷åòîì ïîðÿäêà íà ìíî-
æåñòâàõ íà÷àëüíûõ è êîíå÷íûõ âåðøèí.
Åñëè â ñèñòåìå óïðàâëåíèÿ íå äîïóñêàþòñÿ ðåêóðñèâíûõ âûçîâîâ ñòàáîâ, òî âñå
ïîäñòàíîâêè ìîæíî ñäåëàòü ñòàòè÷åñêè è ðàáîòàòü â ñèñòåìå áåç ñòàáîâ.  ýòîì ñëó-
÷àå íà óðîâíå ðåàëèçàöèè ìîæíî èñïîëüçîâàòü äîïîëíèòåëüíûå âîçìîæíîñòè îïòè-
ìèçàöèè, ñâÿçàííûå ñî ñïåöèôèêîé ïðåäìåòíîé îáëàñòè. Â íàñòîÿùåé ñòàòüå íå ðàñ-
ñìîòðåíî îêîí÷àòåëüíîé ôîðìàëèçàöèè ïîäñòàíîâîê êàðò, ÷òîáû íå îïèñûâàòü äå-
òàëåé ðåàëèçàöèè, íàïðèìåð, òåõíîëîãèé îáåñïå÷åíèÿ óíèêàëüíîñòè èìåí
è ñïîñîáîâ äîñòóïà ê íèì. Ýòà ôîðìàëèçàöèÿ òðåáóåò áîëåå íèçêîãî óðîâíÿ àëãî-
ðèòìèçàöèè, à ñïåöèôèêàöèè íå äîëæíû òðåáîâàòü îãðàíè÷åííûõ ðåøåíèé.
Áàçîâàÿ ñèñòåìà. Ãåíåðàòîð òðàññ ðàññ÷èòàí â ïåðâóþ î÷åðåäü íà ñèìâîëü-
íîå ìîäåëèðîâàíèå. Ýòî çíà÷èò, ÷òî ñîñòîÿíèå áàçîâîé ñèñòåìû ïðåäñòàâëÿåòñÿ
ôîðìóëîé ëîãèêè ïåðâîãî ïîðÿäêà èëè òåìïîðàëüíîé ëîãèêè è ïðîäâèæåíèå ïî
ïóòÿì ñèñòåìû óïðàâëåíèÿ òðåáóåò ïðèìåíåíèÿ äåäóêòèâíûõ ñðåäñòâ äëÿ ðàñ-
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2015, òîì 51, ¹ 1 15
ïîçíàâàíèÿ ïðèìåíèìîñòè ëîêàëüíûõ îïèñàíèé. Áàçîâàÿ ñèñòåìà ìîæåò èìåòü
ñâîþ ìíîãîóðîâíåâóþ èåðàðõè÷åñêóþ ñòðóêòóðó, íå çàâèñÿùóþ îò èåðàðõèè
êàðò.  íåêîòîðûõ ñëó÷àÿõ ýòè äâå èåðàðõèè ïîëåçíî ñòðîèòü ñîâìåñòíî. Ýòî çíà-
÷èò, ÷òî ñðåäè àòðèáóòîâ êàðò ïîçâîëåíî ðàñïîëàãàòü íåêîòîðûå àòðèáóòû áàçî-
âîé ñèñòåìû ñ ôîðìóëàìè, îïèñûâàþùèìè ñâîéñòâà èõ çíà÷åíèé, à ïåðåõîä èç
îäíîé êàðòû â äðóãóþ ìîæåò ñîïðîâîæäàòüñÿ èçìåíåíèåì ñèãíàòóðû è ñîñòîÿ-
íèÿ áàçîâîé ñèñòåìû. Àòðèáóòû áàçîâîé ñèñòåìû ìîãóò áûòü äîñòóïíû ñèñòåìå
óïðàâëåíèÿ è, íàîáîðîò, àòðèáóòû ñèñòåìû óïðàâëåíèÿ ìîãóò èñïîëüçîâàòüñÿ áà-
çîâîé ñèñòåìîé. Òàêîå âçàèìîäåéñòâèå îáåñïå÷èâàåò áîëåå ïîëíîå åäèíñòâî
óïðàâëåíèÿ è îáðàáîòêè äàííûõ è åãî ìîæíî ïðèìåíÿòü êàê íà óðîâíå ìîäåëèðî-
âàíèÿ, òàê è íà óðîâíå ðåàëèçàöèè. Èñïîëüçîâàíèå ýòèõ âîçìîæíîñòåé óäîáíî ðå-
àëèçîâàòü íà ñëåäóþùåì óðîâíå óïðàâëåíèÿ â âèäå ñðåäû, êîòîðàÿ ñîäåðæèò
óïðàâëåíèå è áàçîâóþ ñèñòåìó â êà÷åñòâå ñâîèõ àãåíòîâ. Äëÿ ìîäåëèðîâàíèÿ
ýòîò óðîâåíü îáåñïå÷èâàåòñÿ ãåíåðàòîðîì òðàññ.
ÃÅÍÅÐÀÒÎÐ ÒÐÀÑÑ
Ñèìâîëüíûé ãåíåðàòîð òðàññ ñèñòåìû IMS — àíàëèòè÷åñêàÿ èíñåðöèîííàÿ ìà-
øèíà ñèñòåì ëîêàëüíûõ îïèñàíèé ñ óïðàâëåíèåì, ïðåäñòàâëåííûõ â âèäå
LiveUCM-IMS. Ýòà èíñåðöèîííàÿ ìàøèíà èñïîëüçóåòñÿ äëÿ ðåøåíèÿ ðàçëè÷íûõ
çàäà÷, òðåáóþùèõ ãåíåðàöèè òðàññ. Ïîýòîìó îíà ïðåäñòàâëåíà êàê íàñòðàèâàåìàÿ
ìàøèíà ñ âîçìîæíîñòüþ àäàïòàöèè ê ðàçëè÷íûì êëàññàì çàäà÷. Äàëåå ïðèâåäåíî
íåôîðìàëüíîå îïèñàíèå ãåíåðàòîðà òðàññ. Ôîðìàëüíîå îïèñàíèå ìîæíî ñäåëàòü
íà îñíîâàíèè ôîðìàëüíîé ñåìàíòèêè ÿçûêà LiveUCM-IMS, èçëîæåííîé ðàíåå.
Îáû÷íî ãåíåðàòîð òðàññ ðàññìàòðèâàåòñÿ êàê ñðåäà äëÿ àíàëèçèðóåìîé ìî-
äåëè è ïîëíîå ñîñòîÿíèå ãåíåðàòîðà òðàññ îïèñûâàåòñÿ ñ ïîìîùüþ âûðàæåíèÿ
G U S[ [ ]], ãäå G, U è S — ñîîòâåòñòâåííî ñîñòîÿíèÿ ãåíåðàòîðà, óïðàâëÿþùåé è
áàçîâîé ñèñòåìû. Ãåíåðàòîð òðàññ îáõîäèò äåðåâî ïîâåäåíèÿ ñèñòåìû U S[ ], ïî-
ðîæäàÿ åå ñèìâîëüíûå ñîñòîÿíèÿ â ñîîòâåòñòâèè ñ íåêîòîðîé ñòðàòåãèåé ãåíåðà-
öèè, êîòîðàÿ çàäàåòñÿ ñ ïîìîùüþ íåêîòîðûõ ïàðàìåòðîâ, îïðåäåëÿþùèõ íà-
ñòðîéêó ãåíåðàòîðà íà ðåøàåìóþ çàäà÷ó.
Îñíîâíûå êëàññû çàäà÷, ðåøàåìûõ ñ ïîìîùüþ ãåíåðàòîðà òðàññ, — ýòî ñèì-
âîëüíàÿ âåðèôèêàöèÿ ìîäåëè è ïîñòðîåíèå òåñòîâûõ íàáîðîâ äëÿ ïðîâåðêè ìîäå-
ëè íà êîíêðåòíûõ ñîñòîÿíèÿõ.  ïåðâîì ñëó÷àå â ïðîöåññå ãåíåðàöèè ïðîâåðÿåò-
ñÿ âûïîëíèìîñòü çàäàííûõ óñëîâèé, âî âòîðîì — ñòðîèòñÿ ñèñòåìà òðàññ,
óäîâëåòâîðÿþùàÿ íåêîòîðîìó êðèòåðèþ ïîêðûòèÿ.
 ïðîöåññå ãåíåðàöèè òðàññ íàêàïëèâàåòñÿ ìíîæåñòâî ïðîéäåííûõ ñîñòîÿ-
íèé. Ïðè âòîðè÷íîì ïîïàäàíèè â óæå ïðîéäåííîå ñîñòîÿíèå ãåíåðàöèÿ äëÿ ýòîãî
ñîñòîÿíèÿ ïðåêðàùàåòñÿ.  ñëó÷àå ñèìâîëüíîãî ìîäåëèðîâàíèÿ ñîñòîÿíèå åñòü
ôîðìóëà, êîòîðàÿ ïðîêðûâàåò ìíîæåñòâî êîíêðåòíûõ ñîñòîÿíèé, è äëÿ ïðåêðà-
ùåíèÿ ãåíåðàöèè ìîæíî èñïîëüçîâàòü áîëåå ñëàáûå óñëîâèÿ, íàïðèìåð, èç íîâî-
ãî ñîñòîÿíèÿ ëîãè÷åñêè ñëåäóåò óæå ïðîéäåííîå.
Ïåðâûì ïàðàìåòðîì ãåíåðàòîðà òðàññ ÿâëÿåòñÿ ìíîæåñòâî êîíòðîëüíûõ òî-
÷åê íà êàðòàõ ñèñòåìû óïðàâëåíèÿ, â êà÷åñòâå êîòîðûõ âûáèðàþòñÿ íåêîòîðûå
òî÷êè ïåðåõîäîâ. Íà÷àëüíûå è êîíå÷íûå âåðøèíû, âõîäû â ñòàáû è ïàðàëëåëü-
íûå âåòâëåíèÿ âûáèðàþòñÿ îáÿçàòåëüíî, à ñòàáû íèêîãäà íå ÿâëÿþòñÿ êîíòðîëü-
íûìè òî÷êàìè. Âûáîð êîíòðîëüíûõ òî÷åê ìîæåò îïðåäåëÿòüñÿ íåêîòîðûì êðèòå-
ðèåì èëè êîíêðåòíûì óêàçàíèåì òî÷åê ïåðåõîäà, íàïðèìåð âñå îáÿçàòåëüñòâà
(äëÿ çàäà÷ âåðèôèêàöèè), âñå òî÷êè ïåðåõîäîâ èëè âñå îáÿçàòåëüñòâà è âåòâëåíèÿ
(äëÿ çàäà÷è òåñòèðîâàíèÿ).
Äâå êîíòðîëüíûå òî÷êè íàçûâàþòñÿ ñìåæíûìè, åñëè íà ñîåäèíÿþùèõ èõ
ïóòÿõ íå ñóùåñòâóåò äðóãèõ êîíòðîëüíûõ òî÷åê. Ïðåäïîëîæèì, ÷òî êîíòðîëüíûå
16 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2015, òîì 51, ¹ 1
òî÷êè ðàçðåçàþò âñå öèêëû îòíîøåíèÿ ñëåäîâàíèÿ. Òàê, åñëè ( , , , )a a am1 2 � —
ïîñëåäîâàòåëüíîñòü òî÷åê ïåðåõîäîâ òàêàÿ, ÷òî ( , ) , , , ,a a Succ i mi i
� �1 1 2 1�
è a am1 � , òî ñóùåñòâóåò i òàêîå, ÷òî1� �i m è ai åñòü êîíòðîëüíàÿ òî÷êà. Èç ýòî-
ãî ïðåäïîëîæåíèÿ ñëåäóåò, ÷òî êîëè÷åñòâî ïóòåé, ñîåäèíÿþùèõ äâå
êîíòðîëüíûå òî÷êè, êîíå÷íî.
Ðàññìîòðèì òðàññó ñèñòåìû óïðàâëåíèÿ, íà÷àëîì êîòîðîé åñòü ïàðàëëåëüíàÿ
êîìïîçèöèÿ âñåõ íà÷àëüíûõ òî÷åê, è ïàðó ñìåæíûõ êîíòðîëüíûõ òî÷åê, íàõîäÿ-
ùèõñÿ íà ýòîé òðàññå. Òîãäà ìíîæåñòâî òðàññ, ñîåäèíÿþùèõ ýòè äâå êîíòðîëü-
íûå òî÷êè è íå ïðîõîäÿùèõ ÷åðåç äðóãèå êîíòðîëüíûå òî÷êè, êîíå÷íî. Äåéñòâè-
òåëüíî, ïðè÷èíîé áåñêîíå÷íîãî êîëè÷åñòâà òðàññ, ñîåäèíÿþùèõ äâà ñîñòîÿíèÿ,
ìîãóò áûòü òîëüêî ïàðàëëåëüíûå âåòâëåíèÿ è ïåðåõîäû âíóòðü ñòàáà. Íî îíè
âêëþ÷åíû â ìíîæåñòâî êîíòðîëüíûõ òî÷åê è íå íàõîäÿòñÿ âíóòðè òðàññ, ñîåäè-
íÿþùèõ äâå ñìåæíûå êîíòðîëüíûå òî÷êè.
Èñõîäÿ èç ýòèõ ñîîáðàæåíèé, äëÿ ëþáîé ïàðû äîñòèæèìûõ èç íà÷àëüíîãî
ñîñòîÿíèÿ ñìåæíûõ êîíòðîëüíûõ òî÷åê ìîæíî ïîñòðîèòü ïðîöåññ, ïðåäñòàâëÿþ-
ùèé ñîáîé íåäåòåðìèíèðîâàííóþ ñóììó ïîñëåäîâàòåëüíîé êîìïîçèöèè îáÿçà-
òåëüñòâ ïî âñåì ïóòÿì, ñîåäèíÿþùèì çàäàííûå êîíòðîëüíûå òî÷êè è íå ïðîõî-
äÿùèì ÷åðåç äðóãèå êîíòðîëüíûå òî÷êè. Íàçîâåì ýòîò ïðîöåññ óêðóïíåííûì ëî-
êàëüíûì îïèñàíèåì.
Òðàññà, êîòîðàÿ ïîëó÷àåòñÿ èç îáû÷íîé òðàññû ïðîåêöèåé íà êîíòðîëüíûå
òî÷êè, íàçûâàåòñÿ óêðóïíåííîé. Ïîñëå âûáîðà êîíòðîëüíûõ òî÷åê ãåíåðàòîð
òðàññ ñòðîèò óêðóïíåííûå òðàññû è ïðèìåíÿåò óêðóïíåííûå ëîêàëüíûå îïèñà-
íèÿ ê ñèìâîëüíûì ñîñòîÿíèÿì áàçîâîé ñèñòåìû. Ïåðåõîä îò îäíîé êîíòðîëüíîé
òî÷êè ê äðóãîé ìîæíî ðàññìàòðèâàòü êàê ðåçóëüòàò âûïîëíåíèÿ óêðóïíåííîãî
äåéñòâèÿ, êîòîðîå áóäåì îáîçíà÷àòü êàê Act a a( , )� , ãäå à è �a — ñìåæíûå êîí-
òðîëüíûå òî÷êè. Åñëè ðàññìàòðèâàòü òîëüêî óêðóïíåííûå äåéñòâèÿ, ïîëó÷èì
óêðóïíåííóþ óïðàâëÿþùóþ ñèñòåìó, à ïåðåíîñ óêðóïíåííûõ äåéñòâèé íà áàçî-
âóþ ñèñòåìó ïðèâåäåò ê óêðóïíåííîé áàçîâîé ñèñòåìå.
Îñíîâíîé àòðèáóò ãåíåðàòîðà òðàññ — äåðåâî, ñîñòàâëåííîå èç óêðóïíåí-
íûõ òðàññ. Ëèñòüÿìè ýòîãî äåðåâà ÿâëÿþòñÿ ñîñòîÿíèÿ óïðàâëÿþùåé ñèñòåìû
ñ ñîîòâåòñòâóþùèìè ñîñòîÿíèÿìè áàçîâîé ñèñòåìû, ïîëó÷åííûå â ðåçóëüòàòå
ïðîõîæäåíèÿ óêðóïíåííûõ òðàññ. Êàæäîå ñîñòîÿíèå îòìå÷åíî òðàññîé, êîòîðàÿ
ïðèâåëà ê íåìó. Òàêèì îáðàçîì, ñîñòîÿíèå ãåíåðàòîðà â òåêóùèé ìîìåíò
âðåìåíè ìîæíî çàïèñàòü â âèäå
G p U S p U S p U Sn n n[ : [ ], : [ ], , : [ ]]1 1 1 2 2 2 � .
Âûðàæåíèÿ p U Si i i: [ ] ðàññìàòðèâàþòñÿ êàê ñîñòîÿíèÿ àãåíòîâ, ïîãðóæåííûõ
â ñðåäó ãåíåðàòîðà òðàññ. Ýòè àãåíòû íå âçàèìîäåéñòâóþò, èõ ñîñòîÿíèÿ îòíîñÿò-
ñÿ ê ðàçëè÷íûì ìîìåíòàì âðåìåíè è îíè èìåþò àëüòåðíàòèâíûå âîçìîæíîñòè
äâèæåíèÿ áàçîâîé ñèñòåìû ñ óïðàâëåíèåì. Îòìåòêè ñîñòîÿíèé p p pn1 2, , ,� ìî-
ãóò ÿâëÿòüñÿ ññûëêàìè íà ïîñëåäíèå âåðøèíû òðàññû â äåðåâå òðàññ, ïî êîòî-
ðûì òðàññû âîññòàíàâëèâàþòñÿ îäíîçíà÷íî. Ñîñòîÿíèå U i îáû÷íî ïðåäñòàâëÿ-
åò ñîáîé ïàðàëëåëüíóþ êîìïîçèöèþ àêòèâíûõ òî÷åê, ïîñëå ðàçâåðòûâàíèÿ
êîòîðîé îíî ïðåâðàùàåòñÿ â îõðàíÿåìóþ íåäåòåðìèíèðîâàííóþ ñóììó ïàðàë-
ëåëüíûõ êîìïîçèöèé. Èõ âçàèìîäåéñòâèå îñóùåñòâëÿåòñÿ ïóòåì ñèíõðîíèçà-
öèè òî÷åê ïàðàëëåëüíîãî ñëèÿíèÿ è îæèäàíèÿ ïðèìåíèìîñòè ëîêàëüíûõ îïè-
ñàíèé ïðè ïðîõîæäåíèè îáÿçàòåëüñòâ.
Îñíîâíîå ïðàâèëî, îïèñûâàþùèå ôóíêöèîíèðîâàíèå ãåíåðàòîðà òðàññ, èìå-
åò âèä
G G U S U S U Act a
Act a a Act a a( , ) ( , )
, [ ] [ ], (� �� �� �� � � �� �� � � � , ).
[ * : [ ]] [ * * : [
( , )
� � ��
� �� �� � � � ��
a U U
G p a U S G p a a U
Act a a
S p a U S
Allowed
] * : [ ]] ��
.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2015, òîì 51, ¹ 1 17
Çäåñü * îáîçíà÷àåò êîíêàòåíàöèþ òðàññ â äåðåâå òðàññ, ïåðåõîä íà ñîñòîÿíèÿõ
ãåíåðàòîðà ìåíÿåò ñîîòâåòñòâóþùèì îáðàçîì äåðåâî òðàññ. Ãëàâíûå ñâîéñòâà
ãåíåðàòîðà òðàññ ñïðÿòàíû â ôóíêöèè Allowed. Îíà âûáèðàåò òðàññó, êîòîðóþ
ïîëåçíî ïðîäîëæàòü, è ñëàãàåìîå íåäåòåðìèíèðîâàííîé ñóììû, íàõîäÿùååñÿ
â êîíöå ýòîé òðàññû, êîòîðîå òàêæå áóäåò ïðîäîëæåíî. Ýòè äâà âûáîðà ìîæíî
äåëàòü îäíîâðåìåííî. Àëãîðèòì âûáîðà ïðåäñòàâëÿåò ñîáîé âòîðîé ãëàâíûé
ïàðàìåòð íàñòðîéêè ãåíåðàòîðà íà êëàññ ðåøàåìûõ çàäà÷.
Îäíèì èç êëàññîâ çàäà÷, äëÿ êîòîðûõ ðàçðàáîòàíà íàñòðîéêà ãåíåðàòîðà òðàññ,
åñòü ïîñòðîåíèå ñèñòåìû òåñòîâ, óäîâëåòâîðÿþùåé ñëåäóþùåìó êðèòåðèþ ïîêðû-
òèÿ: ëþáîé ïåðåõîä ìåæäó êîíòðîëüíûìè òî÷êàìè äîëæåí èìåòü òðàññó, ïîêðû-
âàþùóþ ýòîò ïåðåõîä, è âñå òðàññû äîëæíû çàêàí÷èâàòüñÿ â çàäàííûõ òåðìèíàëü-
íûõ òî÷êàõ. Òîãäà êðèòåðèé âûáîðà ñîñòîèò â òîì, ÷òîáû ïîêðûòü êàê ìîæíî
áîëüøåå ÷èñëî ïåðåõîäîâ è ïðîäâèíóòüñÿ êàê ìîæíî áëèæå ê òåðìèíàëüíûì òî÷-
êàì.  ñëó÷àå, êîãäà ýòè äâà êðèòåðèÿ âñòóïàþò â ïðîòèâîðå÷èå, ïåðâîìó îòäàåòñÿ
ïðåäïî÷òåíèå, åñëè ïîêðûòî ìàëî ïåðåõîäîâ, âòîðîìó — åñëè ÷èñëî ïîêðûòûõ ïå-
ðåõîäîâ äîñòàòî÷íî âåëèêî. Òî÷íîå çíà÷åíèå ýòèõ êðèòåðèåâ âûðàæàåòñÿ ìàêñè-
ìèçàöèåé âçâåøåííîé ñóììû ñîîòâåòñòâóþùèõ ÷èñëîâûõ ïàðàìåòðîâ. Âåñà ïîä-
áèðàþòñÿ ýêñïåðèìåíòàëüíî èëè ñ ïîäêëþ÷åíèåì àëãîðèòìîâ ñàìîîáó÷åíèÿ ïðè
äîñòàòî÷íî áîëüøîì íàáîðå ïðèìåðîâ.
Äåðåâî òðàññ èìååò çíà÷èòåëüíûå ïðåèìóùåñòâà ïî ñðàâíåíèþ ñ ïðîñòûì
ìíîæåñòâîì. Ïðåæäå âñåãî äëÿ íåêîòîðûõ çàäà÷, â ÷àñòíîñòè äëÿ çàäà÷è òåñòèðî-
âàíèÿ, ïðåäñòàâëåíèå ðåçóëüòàòà â âèäå äåðåâà ìîæåò èñïîëüçîâàòüñÿ â äàëüíåé-
øåì äëÿ ïðîâåäåíèÿ íåïîñðåäñòâåííî òåñòèðîâàíèÿ. Îäíàêî îòìåòèì, ÷òî ýòî
óäîáíàÿ ñòðóêòóðà äàííûõ äëÿ õðàíåíèÿ ðàçëè÷íîãî ðîäà âñïîìîãàòåëüíûõ äàí-
íûõ äëÿ ïðîöåññà ãåíåðàöèè. Òàê, â òî÷êàõ òðàññ ìîãóò õðàíèòüñÿ ïîñëåäîâàòåëü-
íîñòè ñîñòîÿíèé áàçîâîé ñèñòåìû äëÿ îïðåäåëåíèÿ ïðîéäåííûõ ñîñòîÿíèé,
à òàêæå àïïðîêñèìàöèè èíâàðèàíòîâ è äðóãèå ïîëåçíûå äàííûå.
ÇÀÊËÞ×ÅÍÈÅ
 ñòàòüå îïèñàí íîâûé ãåíåðàòîð ñèìâîëüíûõ òðàññ â ñèñòåìå èíñåðöèîííîãî
ìîäåëèðîâàíèÿ. Ãëàâíûì îòëè÷èåì îò ïðåäûäóùèõ âåðñèé ÿâëÿåòñÿ äîáàâëå-
íèå óïðàâëÿþùåé ñèñòåìû è âîçìîæíîñòü íàñòðîéêè íà ïðåäìåòíóþ îáëàñòü.
ßçûê óïðàâëÿþùåé ñèñòåìû ìîäåëè — ýòî áàçîâîå ïîäìíîæåñòâî ÿçûêà UCM
ñ áàçîâûìè ïðîòîêîëàìè, èñïîëüçóåìûìè äëÿ ðåàëèçàöèè îáÿçàòåëüñòâ.
Ñåìàíòèêà ÿçûêà óïðàâëåíèÿ îïèñàíà â ôîðìàëèçìå èíñåðöèîííîãî ìîäåëè-
ðîâàíèÿ, êîòîðûé äîïóñêàåò âñåâîçìîæíûå ðàñøèðåíèÿ, èìïëåìåíòèðóþùèåñÿ
íà óðîâíå äåéñòâèé ñðåäû.  ÷àñòíîñòè, òàêèì îáðàçîì ìîæíî ðåàëèçîâàòü íåèñ-
ïîëüçîâàííûå ôóíêöèîíàëüíîñòè ïîëíîãî UCM.
Äðóãèå ïîëåçíûå ðàñøèðåíèÿ, êîòîðûå áóäóò ðåàëèçîâàíû â äàëüíåéøåì, —
ââåäåíèå ìåòðè÷åñêèõ õàðàêòåðèñòèê îòðåçêîâ ïóòåé ìåæäó òàêèìè ñìåæíûìè
òî÷êàìè ïåðåõîäîâ, êàê äëèíà èëè âðåìÿ ïðîõîæäåíèÿ îòðåçêà. Ïðåäïîëàãàåòñÿ
òàêæå ââåñòè âåðîÿòíîñòíûå ðàñïðåäåëåíèÿ íà àëüòåðíàòèâíûõ âåòâëåíèÿõ. Äëÿ
ïîâûøåíèÿ ýôôåêòèâíîñòè ãåíåðàöèè òðàññ áóäåò ðåàëèçîâàíî âû÷èñëåíèå èíâà-
ðèàíòîâ, èñïîëüçîâàíèå çàâèñèìîñòåé ïî äàííûì è äðóãèå ñðåäñòâà.
ÑÏÈÑÎÊ ËÈÒÅÐÀÒÓÐÛ
1. G i l b e r t D . R . , L e t i c h e v s k y A . A . A universal interpreter for nondeterministic concurrent
programming languages // Fifth Compulog Network Area Meeting on Language Design and
Semantic Analysis Methods (26 Oct., 1996). — Aachen, 1996. — P. 14.
2. L e t i c h e v s k y A . , G i l b e r t D . A general theory of action languages // Cybernetics and
System Analysis. — 1998. — N 1. — P. 16–37.
18 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2015, òîì 51, ¹ 1
3. L e t i c h e v s k y A . , G i l b e r t D . A model for interaction of agents and environments // Lecture
Notes in Computer Science. — 1999. — 1827. — P. 311–328.
4. M i l n e r R . A calculus of communicating systems. — H.: Springer-Verlag, 1980. — 192 p.
5. M i l n e r R . Communication and concurrency. — NJ.: Prentice Hall, 1989. — 260 p.
6. M i l n e r R . The polyadic �-calculus: a tutorial // Tech. Rep. ECS-LFCS-91-180. — 1991. —
N 180. — P. 91–180.
7. H o a r e C . A . R . Communicating sequential processes. — NJ.: Prentice Hall, 1985. — 256 p.
8. B e r g s t r a , J . A . , K l o p J . W . Process algebra for synchronous communications // Information
and Control. — 1984. — 60, N 1/3. — P. 109–137.
9. C a r d e l l i L . , G o r d o n A . D . Mobile ambients // Foundations of Software Science and Com-
putational Structures. Lecture Notes in Computer Science. — 1998. — 1378. — P. 140–155.
10. P e t r i C . A . Kommunikation mit Automaten. — Bonn: Institut fur Instrumentelle Mathematik,
Schriften des IIM Nr. 2, 1962. — 123 p.
11. H e w i t t C . , B i s h o p P . , S t e i g e r R . A universal modular actor formalism for artificial
intelligence // 3rd Intern. Joint Conf. on Artificial Intelligence (Aug., 1973). — Standford, 1973. —
P. 235–245.
12. L e t i c h e v s k y A . Algebra of behavior transformations and its applications // Structural Theory of
Automata, Semigroups, and Universal Algebra, NATO Science Series II. Mathematics, Physics and
Chemistry. — 2005. — 207. — P. 241–272.
13. Ê à ï è ò î í î â à Þ . Â . , Ë å ò è ÷ å â ñ ê è é À . À . Èíñåðöèîííîå ìîäåëèðîâàíèå // Ïðàö³
ì³æíàð. êîíô. «50 ðîê³â ²íñòèòóòó ê³áåðíåòèêè ³ì. Â.Ì. Ãëóøêîâà ÍÀÍ Óêðà¿íè». — Êè¿â:
Âèä-âî ²Ê ÍÀÍÓ, 2008. — Ñ. 293–301.
14. L e v e r a g i n g UML to deliver correct telecom applications in UML for real / S. Baranov, C. Jer-
vis, V. Kotlyarov, A. Letichevsky, T. Weigert // Design of Embedded Real-Time Systems. — 2003.
— P. 323–342.
15. K a p i t o n o v a J . , L e t i c h e v s k y A . , V o l k o v V . , W e i g e r t T . Validation of embedded
systems. — M.: CRC Press, 2005. — P. 58.
16. B a s i c protocols, message sequence charts, and the verification of requirements specifications /
A. Letichevsky, J. Kapitonova, A. Letichevsky Jr., V. Volkov, S. Baranov, V. Kotlyarov, T. Weigert
// Workshop on Integrated reliability with Telecommunications and UML Languages (Rennes,
4 Nov., 2005). — Rennes: Elsevier, 2005.— P. 42.
17. B a s i c protocols, message sequence charts, and the verification of requirements specifications /
A. Letichevsky, J. Kapitonova, A. Letichevsky Jr., V. Volkov, S. Baranov, V. Kotlyarov, T. Weigert
// Computer Networks. — 2005. — 47. — P. 662–675.
18. S y s t e m specification with basic protocols / A.A. Letichevsky, J.V. Kapitonova, V.A. Volkov,
A.A. Letichevsky Jr., S.N. Baranov, V.P. Kotlyarov, T. Weigert // Cybernetics and System Analysis.
— 2005. — N 4. — P. 3–21.
19. L e t i c h e v s k y A . , L e t y c h e v s k y i O . , P e s c h a n e n k o V . Insertion modeling system //
Lecture Notes in Computer Science. — 2011. — 7162. — P. 262–274.
20. Ë å ò è ÷ å â ñ ê è é À . À . Èíñåðöèîííîå ìîäåëèðîâàíèå // Óïðàâëÿþùèå ñèñòåìû è ìàøèíû.
— 2012. — ¹ 6. — Ñ. 3–14.
21. I n s e r t i o n modeling in distributed system design / A. Letichevsky, J. Kapitonova, V. Kotlyarov,
A. Letichevsky Jr, N. Nikitchenko, V. Volkov, T. Weigert // Problems in Programming. — 2008. —
N 4. — P. 13–39.
22. R e c o m m e n d a t i o n Z.151 User Requirements Notation (URN) // J. International Telecom-
munication Union, 2008. — 208 p.
23. H a s s i n e J . , R i l l i n g J . , D s s o u l i R . An ASM operational semantics for use case maps //
Proceedings of the 13th IEEE International Conference on Requirements Engineering (Paris,
29 Aug. – 2 Sept., 2005). — IEEE Computer Society, 2005. — P. 467.
24. Ã ó á à À . Á . , Ø ó ø ï à í î â Ê . È . Èíñåðöèîííàÿ ñåìàíòèêà ïëîñêèõ ìíîãîïîòîêîâûõ ìîäå-
ëåé ÿçûêà UCM // Óïðàâëÿþùèå ñèñòåìû è ìàøèíû. — 2012. — ¹ 6. — Ñ. 15–21.
25. Ã î ä ë å â ñ ê è é À . Á . Èíñåðöèîííàÿ ñåìàíòèêà ïàðàëëåëüíûõ ïðîöåäóðíûõ êîíñòðóêòîâ
ÿçûêà UCM // Òàì æå. — 2012. — ¹ 6. — Ñ. 22–34.
Ïîñòóïèëà 26.09.2014
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2015, òîì 51, ¹ 1 19
|