Исследование свойств документов MSC с помощью преобразования их в сети Петри
Розглянуто остаточний варіант алгоритму трансляції документів з мови MSC-2000 у мережі Петрі, що подійно еквівалентні до них. Вхідний документ може використовувати довільні елементи мови MSC-2000, але значення елементів у мовах не використовується, також послідовна композиція діаграм інтерпретується...
Saved in:
| Published in: | Кибернетика и системный анализ |
|---|---|
| Date: | 2009 |
| Main Authors: | , , |
| Format: | Article |
| Language: | Russian |
| Published: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2009
|
| Subjects: | |
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/44496 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Cite this: | Исследование свойств документов MSC с помощью преобразования их в сети Петри / С.Л. Крывый, А.В. Чугаенко, Л.Е. Матвеева // Кибернетика и системный анализ. — 2009. — № 6. — С. 165-171. — Бібліогр.: 13 назв. — рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1860247708069003264 |
|---|---|
| author | Крывый, С.Л. Чугаенко, А.В. Матвеева, Л.Е. |
| author_facet | Крывый, С.Л. Чугаенко, А.В. Матвеева, Л.Е. |
| citation_txt | Исследование свойств документов MSC с помощью преобразования их в сети Петри / С.Л. Крывый, А.В. Чугаенко, Л.Е. Матвеева // Кибернетика и системный анализ. — 2009. — № 6. — С. 165-171. — Бібліогр.: 13 назв. — рос. |
| collection | DSpace DC |
| container_title | Кибернетика и системный анализ |
| description | Розглянуто остаточний варіант алгоритму трансляції документів з мови MSC-2000 у мережі Петрі, що подійно еквівалентні до них. Вхідний документ може використовувати довільні елементи мови MSC-2000, але значення елементів у мовах не використовується, також послідовна композиція діаграм інтерпретується як строга. Наведений алгоритм реалізовано як повнофункціональний прототип, що може використовуватися для верифікації програмних систем.
The article presents the final version of the algorithm for translating MSC-2000 documents to Petri net modulo event equivalence. The input document may include any elements of the MSC-2000 language, assuming that condition element value is not used and sequential composition of MSC diagrams is regarded as strict. The algorithm is implemented as a full-functional prototype and can be used to verify software systems.
|
| first_indexed | 2025-12-07T18:39:13Z |
| format | Article |
| fulltext |
ÓÄÊ 51.681.3
Ñ.Ë. ÊÐÛÂÛÉ, À.Â. ×ÓÃÀÅÍÊÎ, Ë.Å. ÌÀÒÂÅÅÂÀ
ÈÑÑËÅÄÎÂÀÍÈÅ ÑÂÎÉÑÒÂ ÄÎÊÓÌÅÍÒÎÂ MSC Ñ ÏÎÌÎÙÜÞ
ÏÐÅÎÁÐÀÇÎÂÀÍÈß ÈÕ Â ÑÅÒÈ ÏÅÒÐÈ1
Êëþ÷åâûå ñëîâà: ñåòè Ïåòðè, MSC, âåðèôèêàöèÿ.
ÂÂÅÄÅÍÈÅ
 íàñòîÿùåå âðåìÿ ôîðìàëüíûå ìåòîäû øèðîêî èñïîëüçóþòñÿ äëÿ ôîðìàëüíîé
ñïåöèôèêàöèè, àíàëèçà è âåðèôèêàöèè ïðîãðàììíûõ è àïïàðàòíûõ ñèñòåì. Ñóòü
ôîðìàëüíûõ ìåòîäîâ ñîñòîèò â àâòîìàòèçàöèè âåðèôèêàöèè ñèñòåì. Â ðåçóëüòàòå
äîïîëíÿþòñÿ äðóãèå ìåòîäû êîíòðîëÿ êà÷åñòâà, òàêèå êàê òåñòèðîâàíèå, ïðîâåðêà
êîäà è ñòàòè÷åñêèé àíàëèç êîäà, è ïîÿâëÿåòñÿ âîçìîæíîñòü ïîâûøåíèÿ êà÷åñòâà
ïðîäóêöèè äî óðîâíÿ, îáû÷íî íåäîñòèæèìîãî îäíèì ëèøü òåñòèðîâàíèåì.
Èññëåäîâàíèÿ â ýòîé îáëàñòè ïðèâåëè ê òîìó, ÷òî â íàñòîÿùåå âðåìÿ âåðèôèêà-
öèÿ ïðîãðàììíûõ ñèñòåì âûäåëèëàñü â îòäåëüíóþ ïðîáëåìó.  ÷àñòíîñòè, àêòèâíî
ðàçâèâàåòñÿ ìåòîä ïðîâåðêè íà ìîäåëè (model checking), ñäåëàâøèé âîçìîæíîé âåðè-
ôèêàöèþ ðåàêòèâíûõ ñèñòåì. Ïðè ýòîì ñïåöèôèêàöèè çàïèñûâàþòñÿ â îïðåäåëåííîì
ôîðìàëüíîì ëîãè÷åñêîì ÿçûêå, â òî âðåìÿ êàê ñàìà ñèñòåìà âûñòóïàåò â êà÷åñòâå ìî-
äåëè, íà êîòîðîé ïðîâåðÿåòñÿ âûïîëíèìîñòü åå ñïåöèôèêàöèé.
1. ÏÎÄÕÎÄÛ Ê ÂÅÐÈÔÈÊÀÖÈÈ ÏÐÎÃÐÀÌÌÍÛÕ ÑÈÑÒÅÌ
Ïðîöåññ ðàçâèòèÿ ñîâðåìåííîãî ïðîãðàììíîãî îáåñïå÷åíèÿ ââèäó ñâîåé ñëîæ-
íîñòè (íàðÿäó ñ íåîáõîäèìîñòüþ áûñòðîãî ðåàãèðîâàíèÿ íà òðåáîâàíèÿ ðûíêà,
æåñòêèìè îãðàíè÷åíèÿìè âðåìåíè è ðåñóðñîâ, à òàêæå òåêó÷åñòüþ êàäðîâ
â îðãàíèçàöèÿõ) íóæäàåòñÿ â ðàçëè÷íûõ ìåòîäîâ ïðîâåðêè äëÿ óäîâëåòâîðåíèÿ
êîíêðåòíûõ çàïðîñîâ.  ýòîì ñëó÷àå ïðåäñòàâëÿåòñÿ öåëåñîîáðàçíûì íàïðàâèòü
óñèëèÿ íà îáåñïå÷åíèå êà÷åñòâà.
Ïðîöåññ ðàçâèòèÿ òåõíîëîãèé ðàçðàáîòêè ïðîãðàììíîãî îáåñïå÷åíèÿ ïðîøåë
äîëãèé ïóòü, íà÷èíàÿ ñ 1970 ã., êîãäà áûëà èçîáðåòåíà âîäîïàäíàÿ ìîäåëü [1]. Ñ ïî-
ÿâëåíèåì CMM/CMMI [2] ñèñòåìû îáåñïå÷åíèÿ êà÷åñòâà ðàçðàáîòêè ïðîãðàììíîãî
îáåñïå÷åíèÿ ïðîöåññà ïîëó÷èëè øèðîêîå ðàñïðîñòðàíåíèå, ïðè ýòîì ïðîäîëæàëàñü
ðàáîòà íàä ñîçäàíèåì íîâûõ ïðîãðàììíûõ ìîäåëåé. Â ïîñëåäíåå âðåìÿ ïîïóëÿðíû-
ìè ñòàíîâÿòñÿ ãèáêèå ìåòîäû (Agile Programming) [3, 4]. Ýòè ìåòîäû îáû÷íî èñ-
ïîëüçóþòñÿ ïðè èíêðåìåíòàëüíîé è áûñòðîé ðàçðàáîòêå ïðèëîæåíèé â ñèòóàöèÿõ,
êîãäà îïðåäåëÿþùåé ÿâëÿåòñÿ ñêîðîñòü âûïóñêà ïðîäóêòà.
Ñîâðåìåííûå ãèáêèå ïîäõîäû òðåáóþò ðàçðàáîòêè ñîîòâåòñòâóþùèõ íîâûõ
ìåòîäîâ è óëó÷øåííûõ ïðîöåññîâ, â ÷àñòíîñòè äëÿ èíòåãðàöèè ôîðìàëüíûõ ìåòî-
äîâ. Ñî÷åòàíèå ãèáêèõ ïîäõîäîâ è ñðåäñòâ àâòîìàòèçèðîâàííîãî êîíòðîëÿ äàåò âîç-
ìîæíîñòü áûñòðîé àäàïòàöèè êîíòðîëÿ êà÷åñòâà ê èçìåíåíèþ áèçíåñ-ñðåäû. Èòåðà-
öèîííàÿ ðàçðàáîòêà, áûñòðîå ïðîòîòèïèðîâàíèå, ìåòîä ÷àñòûõ ðåëèçîâ ìîãóò áûòü
ýôôåêòèâíî äîïîëíåíû ïðèìåíåíèåì àâòîìàòèçèðîâàííîé ñèñòåìû êîíòðîëÿ. Òà-
êàÿ ñèñòåìà êîíòðîëÿ ïîçâîëèò íàõîäèòü è îïðåäåëÿòü èçíà÷àëüíî íåñòàáèëüíûå
è/èëè íåïîëíûå òðåáîâàíèÿ è â òî æå âðåìÿ íå ïðèâîäèò ê óâåëè÷åíèþ ïðîäîëæè-
òåëüíîñòè èòåðàöèè.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2009, ¹ 6 165
1Ðàáîòà âûïîëíåíà ïðè ôèíàíñîâîé ïîääåðæêå ÌÎÍ Óêðàèíû â ðàìêàõ ñîâìåñòíîãî Óêðàèíñêî-
Áîëãàðñêîãî ïðîåêòà ¹145/23.02.2009 «Ðàçðàáîòêà ðàñïðåäåëåííûõ ëàáîðàòîðèé íà îñíîâå
ïðîãðåññèâíûõ ìåòîäîâ äîñòóïà äëÿ ïîääåðæêè ïðîåêòèðîâàíèÿ ñåíñîðíûõ ñèñòåì» è Áîëãàðñêîãî
íàöèîíàëüíîãî íàó÷íîãî ôîíäà â ðàìêàõ ñîâìåñòíîãî Áîëãàðñêî-Óêðàèíñêîãî ïðîåêòà
Ä002-331/19.12.2008 ñ òåì æå íàçâàíèåì.
© Ñ.Ë. Êðûâûé, À.Â. ×óãàåíêî, Ë.Å. Ìàòâååâà, 2009
Íàñòîÿùàÿ ðàáîòà çà-
âåðøàåò ðÿä ñòàòåé, ïðåä-
ñòàâëåííûõ ðàíåå [5–8].
 ñôåðó èññëåäîâàíèÿ âõî-
äèëà ðàçðàáîòêà ñèñòåìû
(ðèñ. 1) äëÿ àíàëèçà è âåðè-
ôèêàöèè ïðîãðàììíîãî îáåñ-
ïå÷åíèÿ è àïïàðàòíûõ ñèñ-
òåì, çàäàííûõ c ïîìîùüþ
ÿçûêà MSC-2000. Â ñòàòüå
îïèñàí àëãîðèòì àâòîìàòè-
÷åñêîé òðàíñëÿöèè òàêîé
ñèñòåìû â ñåòü Ïåòðè. Äîñ-
òîèíñòâîì òàêîãî ïîäõîäà
ÿâëÿåòñÿ òî, ÷òî îò ðàçðàáîò-
÷èêîâ íå òðåáóåòñÿ èçó÷åíèÿ
íîâîãî ÿçûêà ñïåöèôèêàöèé
è äîïîëíèòåëüíîãî ìàòåìà-
òè÷åñêîãî îáðàçîâàíèÿ.
Ñèñòåìà ïîçâîëÿåò ïðè-
ìåíÿòü ðàçíîîáðàçíûå ôîð-
ìàëüíûå ìåòîäèêè ìîäåëèðî-
âàíèÿ ê ñåòÿì Ïåòðè äëÿ óòî÷-
íåíèÿ è ïðîâåðêè òðåáîâàíèé
è àðõèòåêòóðû èñõîäíîé àï-
ïàðàòíîé èëè ïðîãðàììíîé
ñèñòåìû. Äëÿ ýòîãî èñõîäíàÿ
ñèñòåìà, çàäàííàÿ íà ÿçûêå MSC-2000, ïåðåâîäèòñÿ â îðäèíàðíóþ ñåòü Ïåòðè.
 äàííîé ñòàòüå âõîäíîé ÿçûê àëãîðèòìà ðàñøèðåí äî âñåãî ÿçûêà MSC-2000.
Ïðè ýòîì ïîñëåäîâàòåëüíàÿ êîìïîçèöèÿ äèàãðàìì èíòåðïðåòèðóåòñÿ êàê ñòðîãàÿ è çíà-
÷åíèÿ ýëåìåíòîâ òèïà óñëîâèå èãíîðèðóåòñÿ.
2. ÎÑÍÎÂÍÛÅ ÎÏÐÅÄÅËÅÍÈß
Îïðåäåëåíèå 1. Ïóñòü P S� �[ , ] — ÷àñòè÷íî óïîðÿäî÷åííîå ìíîæåñòâî, a è b
— åãî ýëåìåíòû. Áóäåì ãîâîðèòü, ÷òî a äîìèíèðóåò íàä b , åñëè a b� (ò.å. a b�
è a b� ) è �� � �x S a x b: . Áóäåì ãîâîðèòü òàêæå, ÷òî a è b íàõîäÿòñÿ â îòíîøå-
íèè äîìèíèðîâàíèÿ, åñëè a äîìèíèðóåò íàä b èëè b äîìèíèðóåò íàä a.
Îòíîøåíèå äîìèíèðîâàíèÿ ñâÿçàíî ñ ÷àñòè÷íûì ïîðÿäêîì, à èìåííî ÷àñòè÷-
íûé ïîðÿäîê îäíîçíà÷íî âîññòàíàâëèâàåòñÿ èç îòíîøåíèÿ äîìèíèðîâàíèÿ â ëþáîì
êîíå÷íîì ÷àñòè÷íî óïîðÿäî÷åííîì ìíîæåñòâå.
ßçûê MSC. MSC — ÿçûê ìîäåëèðîâàíèÿ äèíàìè÷åñêèõ ñèñòåì, êîòîðûé èñ-
ïîëüçóåò êàê ãðàôè÷åñêîå, òàê è òåêñòîâîå ïðåäñòàâëåíèÿ è ñòàíäàðòèçèðîâàí ITU
(International Telecommunication Union) â [9] (ñèíòàêñèñ) è â [10] (ñåìàíòèêà).
Îáëàñòü ïðèëîæåíèÿ MSC âêëþ÷àåò â ñåáÿ òåëåêîììóíèêàöèè, à òàêæå äðóãèå ðàñ-
ïðåäåëåííûå ðåàêòèâíûå ñèñòåìû ðåàëüíîãî âðåìåíè. MSC øèðîêî èñïîëüçóåòñÿ
íà ðàííèõ ýòàïàõ ðàçðàáîòêè äëÿ ñáîðà ñèñòåìíûõ òðåáîâàíèé. Íàëè÷èå ñòàíäàðòè-
çèðîâàííîé ñåìàíòèêè ÿâëÿåòñÿ îäíîé èç îòëè÷èòåëüíûõ ÷åðò ÿçûêà MSC ïî ñðàâ-
íåíèþ ñ äðóãèìè ÿçûêàìè ìîäåëèðîâàíèÿ.
Ñåòè Ïåòðè. Â ñòàòüå èñïîëüçóþòñÿ îïðåäåëåíèÿ ñåòåé Ïåòðè, ïðèâåäåííûå â
[11].  êà÷åñòâå ôîðìàëüíîé ìîäåëè äëÿ îïðåäåëåíèÿ ñåìàíòèêè è àíàëèçà äîêó-
ìåíòîâ MSC èñïîëüçóþòñÿ îðäèíàðíûå ñåòè Ïåòðè [6].
3. ÀËÃÎÐÈÒÌ ÏÐÅÎÁÐÀÇÎÂÀÍÈß ÄÎÊÓÌÅÍÒÎÂ MSC Â ÑÅÒÈ ÏÅÒÐÈ
3.1. Îáùèå äîïóùåíèÿ è îáîçíà÷åíèÿ. Ïðåäïîëàãàåòñÿ, ÷òî èñõîäíûé äîêó-
ìåíò MSC ñèíòàêñè÷åñêè êîððåêòåí è ñîîòâåòñòâóåò ñòàòè÷åñêèì òðåáîâàíèÿì,
èçëîæåííûì â [9].
166 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2009, ¹ 6
Ðèñ. 1. Ñõåìà òåõíîëîãè÷åñêîãî ïðîöåññà ïðîâåðêè ñèñòåìû
Òåëà âñòðîåííûõ âûðàæåíèé ðàññìàòðèâàþòñÿ êàê àíîíèìíûå äèàãðàììû
MSC (â ñîîòâåòñòâèè ñ [10]). Ïðè ýòîì ñîãëàñíî [9] ïðèíèìàåòñÿ, ÷òî âñå ñîáûòèÿ
â äîêóìåíòå MSC óíèêàëüíû (ïðè íåîáõîäèìîñòè îíè ïåðåèìåíîâûâàþòñÿ). Â îòëè-
÷èå îò [9] çäåñü èñïîëüçóåòñÿ ñòðîãàÿ ïîñëåäîâàòåëüíàÿ êîìïîçèöèÿ äèàãðàìì MSC.
Ïîëó÷åííàÿ â ðåçóëüòàòå ïðèìåíåíèÿ äàííîãî àëãîðèòìà ñåòü Ïåòðè îòðàæàåò
òîëüêî ñòðóêòóðó èñõîäíîãî äîêóìåíòà MSC, ò.å. ñòàòè÷åñêóþ ÷àñòü ïîâåäåíèÿ ðàñ-
ñìàòðèâàåìîé ñèñòåìû; èíôîðìàöèÿ, íàõîäÿùàÿñÿ âíóòðè ýëåìåíòîâ òèïà óñëîâèå,
íå èñïîëüçóåòñÿ.
Ïðè îïèñàíèè àëãîðèòìà èñïîëüçóþòñÿ ñëåäóþùèå îáîçíà÷åíèÿ:
• ñîáûòèÿ MSC (âêëþ÷àÿ ýëåìåíò òèïà óñëîâèå), êàê è ñîîòâåòñòâóþùèå èì
ôðàãìåíòû ÑÏ, îáîçíà÷àåì e i� ;
• ïîñëåäîâàòåëüíîñòè è íåóïîðÿäî÷åííûå ãðóïïû ñîáûòèé MSC, êàê è ñîîò-
âåòñòâóþùèå èì ôðàãìåíòû ÑÏ, îáîçíà÷àåì se i� ;
• ôðàãìåíòû ÑÏ, èñïîëüçóåìûå äëÿ ïðåäñòàâëåíèÿ óïðàâëÿþùèõ êîíñòðóê-
öèé MSC, íàçûâàåì êîíñòðóêöèÿìè; â ïîëó÷åííîé ÑÏ ìåòêè ïåðåõîäîâ ðàç-
ìåùàþòñÿ ðÿäîì ñî çíàêîì ïåðåõîäà, â òî âðåìÿ êàê äîïîëíèòåëüíàÿ ñëó-
æåáíàÿ èíôîðìàöèÿ (íàïðèìåð, äëÿ îáðàòíîé òðàññèðîâêè â MSC) ïîìåùà-
åòñÿ âíóòðè çíà÷êîâ ïåðåõîäà èëè ìåñòà;
• L ap ( ) — ïðåôèêñíûé ÿçûê ðàçìå÷åííîé ñåòè a, êîòîðûé íàçîâåì ÿçûêîì ÑÏ.
3.2. Îïèñàíèå àëãîðèòìà. Ïðåäñòàâëåííûé àëãîðèòì îñíîâûâàåòñÿ íà òîì,
÷òî ñîãëàñíî ñåìàíòèêå MSC ([10] ñ ðàñøèðåíèåì, îïèñàííûì â [6]) äîêóìåíò MSC
ìîæåò ðàññìàòðèâàòüñÿ êàê íàáîð ñîáûòèé, ñâÿçàííûõ ïîñëåäîâàòåëüíîé, ïàðàë-
ëåëüíîé è àëüòåðíàòèâíîé êîìïîçèöèÿìè. Òèï èñïîëüçóåìîé êîìïîçèöèè âûáèðà-
åòñÿ â çàâèñèìîñòè îò óïðàâëÿþùèõ êîíñòðóêöèé ÿçûêà MSC. Òàêèì îáðàçîì, àëãî-
ðèòì ñèìóëèðóåò ýòè óïðàâëÿþùèå ñòðóêòóðû ñ ïîìîùüþ ôðàãìåíòîâ ñåòè Ïåòðè,
ïîëó÷àÿ â ðåçóëüòàòå ñåòü Ïåòðè, ïðåôèêñíûé ÿçûê êîòîðîé ñîáûòèéíî ýêâèâàëåí-
òåí íàáîðó òðàññ èñõîäíîãî äîêóìåíòà MSC. Äîêàçàòåëüñòâî êîððåêòíîñòè àëãî-
ðèòìà ïðèâåäåíî â [8].
3.2.1. Øàãè àëãîðèòìà. Ðàññìîòðèì ïîñòðîåíèå ñåòè Ïåòðè ïî äîêóìåíòó
MSC.
Øàã 1. Êàæäàÿ äèàãðàììà MSC (âêëþ÷àÿ àíîíèìíûå äèàãðàììû, íàõîäÿùèåñÿ â
òåëàõ âñòðîåííûõ âûðàæåíèé) ïåðåâîäèòñÿ â êîíñòðóêöèþ, ïîêàçàííóþ íà ðèñ. 2,à,
ãäå se se n� �1 , ,� îáîçíà÷àþò ïîñëåäîâàòåëüíîñòè ñîáûòèé è êîíñòðóêöèé, ïðèíàä-
ëåæàùèõ ýòîé äèàãðàììå. Åñëè äîêóìåíò MSC ñîäåðæèò íåñêîëüêî ññûëîê íà îäíó
è òó æå äèàãðàììó, òî îíè ðàññìàòðèâàþòñÿ êàê íåñêîëüêî íåçàâèñèìûõ ýêçåìïëÿ-
ðîâ äèàãðàììû è êîïèðóþòñÿ â íóæíîì êîëè÷åñòâå.
Øàã 2. Äëÿ êàæäîãî ñîáûòèÿ MSC e i� ñòðîèòñÿ Pre e i� �( ) — ìíîæåñòâî ñîáû-
òèé è êîíñòðóêöèé, íåïîñðåäñòâåííî ïðåäøåñòâóþùèõ ýòîìó ñîáûòèþ. Çàòåì e i�
ïåðåâîäèòñÿ â êîíñòðóêöèþ, ïîêàçàííóþ íà ðèñ. 2,á, ãäå n Pre e i� | ( )|� � , ïîñëå ÷åãî
âõîäíûå ìåñòà p pn1 , ,� ñîåäèíÿþòñÿ ñ ñîîòâåòñòâóþùèìè ñîáûòèÿìè è êîí-
ñòðóêöèÿìè èç Pre e i� �( ) .
Øàã 3. Ïàðàëëåëüíàÿ êîìïîçèöèÿ äèàãðàìì MSC (ïðåäñòàâëåíà êîíñòðóêöèåé
par â ññûëî÷íîì ëèáî âñòðîåííîì âûðàæåíèè MSC èëè êîíñòðóêöèåé parallel
frame â HMSC) ïåðåâîäèòñÿ â êîíñòðóêöèþ, ïîêàçàííóþ íà ðèñ. 2,â, ãäå n ñîîòâå-
òñòâóåò êîëè÷åñòâó àðãóìåíòîâ ýòîé êîìïîçèöèè.
Øàã 4. Àëüòåðíàòèâíàÿ êîìïîçèöèÿ äèàãðàìì MSC (ïðåäñòàâëåíà êîíñòðóê-
öèÿìè alt, opt, exc â ññûëî÷íîì ëèáî âñòðîåííîì âûðàæåíèè MSC èëè ðàçäåëÿþ-
ùåéñÿ ëèíèåé â HMSC) ïåðåâîäèòñÿ â êîíñòðóêöèþ, ïîêàçàííóþ íà ðèñ. 2,ã, ãäå n
ñîîòâåòñòâóåò êîëè÷åñòâó àðãóìåíòîâ ýòîé êîìïîçèöèè.
Øàã 5. Ïîñëåäîâàòåëüíàÿ êîìïîçèöèÿ äèàãðàìì MSC (ïðåäñòàâëåíà êîíñòðóê-
öèåé seq â ññûëî÷íîì âûðàæåíèè MSC èëè ëèíèåé â HMSC) ïåðåâîäèòñÿ â êîí-
ñòðóêöèþ, ïîêàçàííóþ íà ðèñ. 2,ä.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2009, ¹ 6 167
Øàã 6. Èòåðàöèÿ äèàãðàììû MSC (ïðåäñòàâëåíà êîíñòðóêöèåé loop â ññûëî÷-
íîì èëè âñòðîåííîì âûðàæåíèè MSC) ðàññìàòðèâàåòñÿ êàê âàðèàíò àëüòåðíàòèâ-
íîé êîìïîçèöèè è ïåðåâîäèòñÿ â êîíñòðóêöèþ, ïîêàçàííóþ íà ðèñ. 2,å.
Øàã 7. Ïîñëåäíèå ýëåìåíòû è êîíñòðóêöèè (êðîìå ýëåìåíòà stop) êîìïîçèöèè
èëè äèàãðàììû MSC ñîåäèíÿþòñÿ ñ ñîîòâåòñòâóþùåé êîíñòðóêöèåé _out.
Øàã 8. Ýëåìåíò HMSC start ïåðåâîäèòñÿ â êîíñòðóêöèþ, ïîêàçàííóþ íà
ðèñ. 2,æ.
Øàã 9. Ýëåìåíò HMSC stop ïåðåâîäèòñÿ â êîíñòðóêöèþ, ïîêàçàííóþ íà
ðèñ. 2,ç.
Øàã 10. Îáëàñòü ïàðàëëåëüíîãî âûïîëíåíèÿ ðàññìàòðèâàåòñÿ êàê ïàðàëëåëü-
íàÿ êîìïîçèöèÿ (ñîãëàñíî [10]) è ïåðåâîäèòñÿ â êîíñòðóêöèþ, ïîêàçàííóþ íà
ðèñ. 2,è.
3.2.2. Ïîñòðîåíèå ìíîæåñòâà Pre e i� �( ) . Äëÿ êàæäîãî ñîáûòèÿ e i� ìíîæåñòâî
Pre e i� �( ) âêëþ÷àåò ñëåäóþùèå ýëåìåíòû è êîíñòðóêöèè.
1. Ñîáûòèÿ, èìåþùèå îáùóþ ñ e i� ñóùíîñòü è ðàñïîëîæåííûå íåïîñðåäñòâåí-
íî âûøå e i� íà ëèíèè ýòîé ñóùíîñòè.
2. Êîíñòðóêöèÿ msc_in äèàãðàììû MSC, åñëè e i� ðàñïîëîæåíî â íà÷àëå äèàã-
ðàììû è íå ÿâëÿåòñÿ ñîáûòèåì òèïà create in.
3. Ñîáûòèÿ message out, create out, call out èëè reply out , åñëè e i� — ñîîòâå-
òñòâóþùåå ñîáûòèå òèïà message in, create in, call in èëè reply in.
4. Ñîáûòèÿ, íåïîñðåäñòâåííî ïðåäøåñòâóþùèå e i� ñîãëàñíî ÿâíîìó óïîðÿäî-
÷åíèþ (âûðàæåíû êîíñòðóêöèÿìè before è after).
×òîáû óìåíüøèòü ðàçìåð ðåçóëüòèðóþùåé ñåòè Ïåòðè, èç ìíîæåñòâà
Pre e i� �( ) ìîæíî èñêëþ÷èòü ýëåìåíòû, êîòîðûå íå óäîâëåòâîðÿþò äîìèíèðîâàíèþ
îòíîñèòåëüíî ïîðÿäêà ýëåìåíòîâ. Äàííîå ñîêðàùåíèå Pre e i� �( ) íå âëèÿåò íà ÿçûê
ïîëó÷åííîé ñåòè Ïåòðè.
3.2.3. Ñâîéñòâà àëãîðèòìà. Îïðåäåëåíèå 2. Äîêóìåíò MSC áóäåì íàçûâàòü
àöèêëè÷åñêèì, åñëè â íåì îòñóòñòâóþò êîíñòðóêöèè loop è åãî HMSC ïðåäñòàâëÿ-
þò àöèêëè÷åñêèå ãðàôû.
168 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2009, ¹ 6
Ðèñ. 2. Ôðàãìåíòû ÑÏ, ñîîòâåòñòâóþùèå êîíñòðóêöèÿì MSC
à á â ã
ä å æ ç è
Òåîðåìà 1. Äëÿ àöèêëè÷åñêîãî äîêóìåíòà MSC ñåòü Ïåòðè, ïîñòðîåííàÿ ïðè-
âåäåííûì âûøå àëãîðèòìîì, ãåíåðèðóåò ïðåôèêñíûé ÿçûê, âêëþ÷àþùèé ìíîæåñ-
òâî ñòàòè÷åñêèõ òðàññ, êîòîðûå ñòðîÿòñÿ íà îñíîâå èñõîäíîãî äîêóìåíòà MSC.
Òåîðåìà 2. Äîáàâëåíèå êîíñòðóêöèé èòåðàöèè (êîíñòðóêöèé loop èëè öèêëè-
÷åñêèõ ðåáåð â HMSC) â äîêóìåíò MSC ñîãëàñíî âûøåïðèâåäåííîìó àëãîðèòìó íå
íàðóøàåò âêëþ÷åíèÿ ìíîæåñòâà ñòàòè÷åñêèõ òðàññ, ãåíåðèðóåìûõ èñõîäíûì äîêó-
ìåíòîì MSC, â ÿçûê ïîñòðîåííîé ïî íåìó ÑÏ.
Òåîðåìà 3. Äëÿ äîêóìåíòà MSC è ïîñòðîåííîé ïî íåìó ñ ïîìîùüþ âûøåîïè-
ñàííîãî àëãîðèòìà ñåòè Ïåòðè ïðåôèêñíûé ÿçûê, ãåíåðèðóåìûé ýòîé ñåòüþ, âêëþ-
÷àåòñÿ â ìíîæåñòâî ñòàòè÷åñêèõ òðàññ, ãåíåðèðóåìûõ èñõîäíûì äîêóìåíòîì MSC.
Äîêàçàòåëüñòâà ýòèõ òåîðåì ïðèâåäåíû â [13]
Èç òåîðåì 1–3 ñëåäóåò ñîáûòèéíàÿ ýêâèâàëåíòíîñòü ñòàòè÷åñêèõ òðàññ äîêó-
ìåíòà MSC è ïðåôèêñíîãî ÿçûêà ïîñòðîåííîé ïî íåìó ñåòè Ïåòðè.
4. ÏÐÈÌÅÐ
Ðàññìîòðèì ïðèìåíåíèå ïðåäñòàâëåííîãî àëãîðèòìà äëÿ èññëåäîâàíèÿ ñâîéñòâ
ñèñòåìû, îïèñàííîé íà ÿçûêå MSC. Ïóñòü äàí äîêóìåíò, ñîñòîÿùèé èç òðåõ äèàã-
ðàìì MSC è îäíîé HMSC (ðèñ. 3). Ýòîò äîêóìåíò îïèñûâàåò ïðîñòóþ ñèñòåìó ñ
âçàèìíûì èñêëþ÷åíèåì, â êîòîðîé äâà ïîòðåáèòåëÿ (cons1 è cons2) êîíêóðèðó-
þò çà îáùèé ðåñóðñ (res). Ïîëó÷èâ äîñòóï ê ðåñóðñó, êàæäûé ïîòðåáèòåëü çàõâà-
òûâàåò åãî, âûïîëíÿåò êðèòè÷åñêóþ ñåêöèþ (Cr1 èëè Cr2) è çàòåì âîçâðàùàåò.
Âíà÷àëå ïîñòðîèì ñåòü Ïåòðè ïî ïðèâåäåííîìó äîêóìåíòó MSC. Ïîñëå ïðèìå-
íåíèÿ âûøåîïèñàííîãî àëãîðèòìà ïîëó÷èì ñåòü, ïîêàçàííóþ íà ðèñ. 4. Âíóòðè ýëå-
ìåíòîâ ñåòè ïîìåùåíû íàçâàíèÿ ñîîòâåòñòâóþùèõ èì ýëåìåíòîâ è êîíñòðóêöèé
èñõîäíîãî äîêóìåíòà MSC. Äëÿ óïðîùåíèÿ àíàëèçà ðåäóöèðóåì ïîñòðîåííóþ ñåòü
Ïåòðè ñîãëàñíî ïðàâèëàì, ïðèâåäåííûì â [11]. Ïîëó÷åííàÿ ñåòü ïîêàçàíà íà ðèñ. 5.
Äàëåå ïðèìåíèì ìåòîä ìàòðèöû èíöèäåíòíîñòè äëÿ ïðîâåðêè æèâîñòè ïåðåõî-
äîâ ñåòè [11]. Äëÿ ýòîãî íåîáõîäèìî ðåøèòü äèîôàíòîâî óðàâíåíèå Ax � 0 , ãäå
A — ìàòðèöà èíöèäåíòíîñòè ñåòè Ïåòðè. Ðåøèâ ýòî óðàâíåíèå ìåòîäîì, îïèñàí-
íûì â [12], ïîëó÷èì ñëåäóþùèé óðåçàííûé íàáîð ðåøåíèé (îíè æå Ò-èíâàðèàíòû
ñåòè Ïåòðè):
0 1 1 1 1 1 1 1 1 0 0 0 0 0
0 0 0 0 0 1 1 1 1 0 1 1 1 1
�
��
�
�� .
Êàê âèäíî èç íàáîðà ðåøåíèé, âñå ïåðåõîäû ñåòè, çà èñêëþ÷åíèåì íà÷àëüíîãî
(t_0) è êîíå÷íîãî (t_9), ïîêðûòû åäèíèöàìè è, ñëåäîâàòåëüíî, æèâû. Ýòî îçíà÷àåò,
÷òî â èñõîäíîé ñèñòåìå íåò äåäëîêîâ è ëîâóøåê.
Äàëåå ïðîâåðèì îãðàíè÷åííîñòü ïîëó÷åííîé ñåòè Ïåòðè ñ ïîìîùüþ åå äåðåâà
ïîêðûòèÿ. Ïîëíîå äåðåâî ïîêðûòèÿ ñëèøêîì ãðîìîçäêî äëÿ âêëþ÷åíèÿ â ñòàòüþ
(ñì. http://avch.org.ua/downloads/mutex_PN_tree.dot.gz), íî åãî àíàëèç ïîêàçûâàåò,
÷òî â íåì îòñóòñòâóþò �-ëèñòû (ò.å. â èññëåäóåìîé ñåòè íåò íåîãðàíè÷åííûõ ìåñò).
Ýòî çíà÷èò, ÷òî äàííàÿ ñåòü îãðàíè÷åíà è â èññëåäóåìîé ñèñòåìå íå ìîæåò áûòü íå-
îãðàíè÷åííîãî íàêîïëåíèÿ çàïðîñîâ ðåñóðñà.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2009, ¹ 6 169
Ðèñ. 3. Äîêóìåíò MSC äëÿ âçàèìíîãî èñêëþ÷åíèÿ
170 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2009, ¹ 6
Ðèñ. 4. Ñåòü Ïåòðè äëÿ ïðèìåðà ñ âçàèìíûì èñêëþ÷åíèåì
ÇÀÊËÞ×ÅÍÈÅ
Íàñòîÿùàÿ ðàáîòà çàâåðøàåò öèêë ñòàòåé [1–4]. Â îïèñàííîé âåðñèè àëãîðèòìà
âõîäíîé íàáîð ýëåìåíòîâ ðàñøèðåí äî ïîëíîãî ÿçûêà MSC-2000, à òàêæå ïðèâå-
äåí ïðèìåð, èëëþñòðèðóþùèé ðàáîòó àëãîðèòìà. Ïðåäñòàâëåííûé àëãîðèòì ðåà-
ëèçîâàí â âèäå ïîëíîôóíêöèîíàëüíîãî ïðîòîòèïà è ìîæåò èñïîëüçîâàòüñÿ äëÿ
âåðèôèêàöèè ïðîãðàììíûõ ñèñòåì.
ÑÏÈÑÎÊ ËÈÒÅÐÀÒÓÐÛ
1. R o y c e W . Managing the development of large software systems: Concepts and techniques / In Proceed-
ings of IEEE WESCON, 1970. — P. 1–9.
2. C M M I product team. CMMI for system engineering/software engineering, Version 1.02 / Carnegie
Mellon, Software Engineering Institute, 2000. — 606 p.
3. B e c k K . Extreme programming explained: embrace change / Addison Wesley Longman, Inc., 2000. —
224 p.
4. C o c k b u r n A . Agile software development. — Boston: Addison-Wesley, 2001. — 256 p.
5. 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. — P. 107–120.
6. 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. — 79, N 3–4. — P. 1–15.
7. 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. — P. 376–387.
8. 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 . Converting of MSC documents to Petri Nets /
Proceedings of the CS\&P’2008 Workshop, 2008. — P. 83–93.
9. I T U - T S Recommendation Z.120: Message Sequence Chart (MSC) / Edited by ITU-TS. — ITU-TS,
Geneva, 2000. — 128 p.
10. I T U - T S Recommendation Z.120 Annex B: Algebraic semantics of Message Sequence Charts / Edited by
ITU-TS. — ITU-TS, Geneva, 1998. — 73 p.
11. M u r a t a T . Petri nets: Properties, analysis and applications / Proceedings of the IEEE, 1989. — 77. — P. 541–580.
12. K r i v o i S . Criteria of satisfiability for homogeneous systems of linear diophantine constraints // Lecture
Notes in Computer Science. Parallel Processing and Applied Mathematics. — 2002. — 2328. — P. 264–271.
13. Ê ð û â û é Ñ . Ë . , × ó ã à å í ê î À . Â . Ôîðìàëüíûå ìåòîäû àíàëèçà äèñêðåòíûõ ñèñòåì ñ èñïîëü-
çîâàíèåì ÿçûêà ñïåöèôèêàöèé // Êèáåðíåòèêà è ñèñòåìíûé àíàëèç. — 2009. — ¹ 4. — Ñ. 31–48.
Ïîñòóïèëà 07.07.2009
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2009, ¹ 6 171
Ðèñ. 5. Óïðîùåííàÿ ñåòü Ïåòðè äëÿ ïðèìåðà ñ âçàèìíûì èñêëþ÷åíèåì
|
| id | nasplib_isofts_kiev_ua-123456789-44496 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 0023-1274 |
| language | Russian |
| last_indexed | 2025-12-07T18:39:13Z |
| publishDate | 2009 |
| publisher | Інститут кібернетики ім. В.М. Глушкова НАН України |
| record_format | dspace |
| spelling | Крывый, С.Л. Чугаенко, А.В. Матвеева, Л.Е. 2013-06-02T09:46:43Z 2013-06-02T09:46:43Z 2009 Исследование свойств документов MSC с помощью преобразования их в сети Петри / С.Л. Крывый, А.В. Чугаенко, Л.Е. Матвеева // Кибернетика и системный анализ. — 2009. — № 6. — С. 165-171. — Бібліогр.: 13 назв. — рос. 0023-1274 https://nasplib.isofts.kiev.ua/handle/123456789/44496 51.681.3 Розглянуто остаточний варіант алгоритму трансляції документів з мови MSC-2000 у мережі Петрі, що подійно еквівалентні до них. Вхідний документ може використовувати довільні елементи мови MSC-2000, але значення елементів у мовах не використовується, також послідовна композиція діаграм інтерпретується як строга. Наведений алгоритм реалізовано як повнофункціональний прототип, що може використовуватися для верифікації програмних систем. The article presents the final version of the algorithm for translating MSC-2000 documents to Petri net modulo event equivalence. The input document may include any elements of the MSC-2000 language, assuming that condition element value is not used and sequential composition of MSC diagrams is regarded as strict. The algorithm is implemented as a full-functional prototype and can be used to verify software systems. Работа выполнена при финансовой поддержке МОН Украины в рамках совместного Украинско-Болгарского проекта №145/23,02,2009 «Разработка распределенных лабораторий на основе прогрессивных методов доступа для поддержки проектирования сенсорных систем» и Болгарского национального научного фонда в рамках совместного Болгарско-Украинского проекта Д002-331/19,12,2008 с тем же названием. ru Інститут кібернетики ім. В.М. Глушкова НАН України Кибернетика и системный анализ Новые средства кибернетики, информатики, вычислительной техники и системного анализа Исследование свойств документов MSC с помощью преобразования их в сети Петри Дослідження властивостей документів MSC за допомогою їх перетворення у мережі Петрі Exploring the properties of MSC documents by converting them to Petri nets Article published earlier |
| spellingShingle | Исследование свойств документов MSC с помощью преобразования их в сети Петри Крывый, С.Л. Чугаенко, А.В. Матвеева, Л.Е. Новые средства кибернетики, информатики, вычислительной техники и системного анализа |
| title | Исследование свойств документов MSC с помощью преобразования их в сети Петри |
| title_alt | Дослідження властивостей документів MSC за допомогою їх перетворення у мережі Петрі Exploring the properties of MSC documents by converting them to Petri nets |
| title_full | Исследование свойств документов MSC с помощью преобразования их в сети Петри |
| title_fullStr | Исследование свойств документов MSC с помощью преобразования их в сети Петри |
| title_full_unstemmed | Исследование свойств документов MSC с помощью преобразования их в сети Петри |
| title_short | Исследование свойств документов MSC с помощью преобразования их в сети Петри |
| title_sort | исследование свойств документов msc с помощью преобразования их в сети петри |
| topic | Новые средства кибернетики, информатики, вычислительной техники и системного анализа |
| topic_facet | Новые средства кибернетики, информатики, вычислительной техники и системного анализа |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/44496 |
| work_keys_str_mv | AT kryvyisl issledovaniesvoistvdokumentovmscspomoŝʹûpreobrazovaniâihvsetipetri AT čugaenkoav issledovaniesvoistvdokumentovmscspomoŝʹûpreobrazovaniâihvsetipetri AT matveevale issledovaniesvoistvdokumentovmscspomoŝʹûpreobrazovaniâihvsetipetri AT kryvyisl doslídžennâvlastivosteidokumentívmsczadopomogoûíhperetvorennâumerežípetrí AT čugaenkoav doslídžennâvlastivosteidokumentívmsczadopomogoûíhperetvorennâumerežípetrí AT matveevale doslídžennâvlastivosteidokumentívmsczadopomogoûíhperetvorennâumerežípetrí AT kryvyisl exploringthepropertiesofmscdocumentsbyconvertingthemtopetrinets AT čugaenkoav exploringthepropertiesofmscdocumentsbyconvertingthemtopetrinets AT matveevale exploringthepropertiesofmscdocumentsbyconvertingthemtopetrinets |