Алгоритм формальной верификации шаблонов бизнес-процессов
Формальне визначення шаблонів бізнес-процесів представлено на підставі аналізу бібліотек ІTІL і MOF. Визначено передумову ініціалізації і постумову для шаблонів бізнес-процесів. Доведено можливість розв’язання проблеми формальної верифікації для шаблонів бізнес-процесів щодо визначеної передумови ін...
Збережено в:
| Дата: | 2011 |
|---|---|
| Автор: | |
| Формат: | Стаття |
| Мова: | Russian |
| Опубліковано: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2011
|
| Назва видання: | Кибернетика и системный анализ |
| Теми: | |
| Онлайн доступ: | http://dspace.nbuv.gov.ua/handle/123456789/84185 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Цитувати: | Алгоритм формальной верификации шаблонов бизнес-процессов / А.С. Варосян // Кибернетика и системный анализ. — 2011. — Т. 47, № 2. — С. 62-76. — Бібліогр.: 11 назв. — рос. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
irk-123456789-84185 |
|---|---|
| record_format |
dspace |
| spelling |
irk-123456789-841852015-07-04T03:02:00Z Алгоритм формальной верификации шаблонов бизнес-процессов Варосян, А.С. Кибернетика Формальне визначення шаблонів бізнес-процесів представлено на підставі аналізу бібліотек ІTІL і MOF. Визначено передумову ініціалізації і постумову для шаблонів бізнес-процесів. Доведено можливість розв’язання проблеми формальної верифікації для шаблонів бізнес-процесів щодо визначеної передумови ініціалізації і постумови виконання. Планується подальша робота в двох напрямках: застосування запропонованого алгоритму формальної верифікації на інших бібліотеках шаблонів бізнес-процесів та дослідження інших бібліотек бізнес-процесів для їх ідентифікації. The formal definition of business process templates is presented based on the analysis of ITIL and MOF libraries. The definition of initialization precondition and execution postcondition is introduced. The solvability of formal verification problem for business process templates with respect to the defined initialization precondition and execution postcondition is shown. It is planned to continue this research in two fields: (i) to apply the formal verification algorithm with other business process template libraries and (ii) to examine other business process libraries to identify new classes of business processes. 2011 Article Алгоритм формальной верификации шаблонов бизнес-процессов / А.С. Варосян // Кибернетика и системный анализ. — 2011. — Т. 47, № 2. — С. 62-76. — Бібліогр.: 11 назв. — рос. 0023-1274 http://dspace.nbuv.gov.ua/handle/123456789/84185 519.681 ru Кибернетика и системный анализ Інститут кібернетики ім. В.М. Глушкова НАН України |
| institution |
Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| collection |
DSpace DC |
| language |
Russian |
| topic |
Кибернетика Кибернетика |
| spellingShingle |
Кибернетика Кибернетика Варосян, А.С. Алгоритм формальной верификации шаблонов бизнес-процессов Кибернетика и системный анализ |
| description |
Формальне визначення шаблонів бізнес-процесів представлено на підставі аналізу бібліотек ІTІL і MOF. Визначено передумову ініціалізації і постумову для шаблонів бізнес-процесів. Доведено можливість розв’язання проблеми формальної верифікації для шаблонів бізнес-процесів щодо визначеної передумови ініціалізації і постумови виконання. Планується подальша робота в двох напрямках: застосування запропонованого алгоритму формальної верифікації на інших бібліотеках шаблонів бізнес-процесів та дослідження інших бібліотек бізнес-процесів для їх ідентифікації. |
| format |
Article |
| author |
Варосян, А.С. |
| author_facet |
Варосян, А.С. |
| author_sort |
Варосян, А.С. |
| title |
Алгоритм формальной верификации шаблонов бизнес-процессов |
| title_short |
Алгоритм формальной верификации шаблонов бизнес-процессов |
| title_full |
Алгоритм формальной верификации шаблонов бизнес-процессов |
| title_fullStr |
Алгоритм формальной верификации шаблонов бизнес-процессов |
| title_full_unstemmed |
Алгоритм формальной верификации шаблонов бизнес-процессов |
| title_sort |
алгоритм формальной верификации шаблонов бизнес-процессов |
| publisher |
Інститут кібернетики ім. В.М. Глушкова НАН України |
| publishDate |
2011 |
| topic_facet |
Кибернетика |
| url |
http://dspace.nbuv.gov.ua/handle/123456789/84185 |
| citation_txt |
Алгоритм формальной верификации шаблонов бизнес-процессов / А.С. Варосян // Кибернетика и системный анализ. — 2011. — Т. 47, № 2. — С. 62-76. — Бібліогр.: 11 назв. — рос. |
| series |
Кибернетика и системный анализ |
| work_keys_str_mv |
AT varosânas algoritmformalʹnojverifikaciišablonovbiznesprocessov |
| first_indexed |
2025-07-06T11:07:56Z |
| last_indexed |
2025-07-06T11:07:56Z |
| _version_ |
1836895517389357056 |
| fulltext |
ÓÄÊ 519.681
À.Ñ. ÂÀÐÎÑßÍ
ÀËÃÎÐÈÒÌ ÔÎÐÌÀËÜÍÎÉ ÂÅÐÈÔÈÊÀÖÈÈ
ØÀÁËÎÍÎÂ ÁÈÇÍÅÑ-ÏÐÎÖÅÑÑÎÂ
Êëþ÷åâûå ñëîâà: áèçíåñ-ïðîöåññ, øàáëîí, ôîðìàëüíàÿ âåðèôèêàöèÿ.
 íàñòîÿùåé ñòàòüå ðàññìàòðèâàåòñÿ çàäà÷à ôîðìàëüíîé ïðîâåðêè êîððåêòíîñ-
òè øàáëîíîâ áèçíåñ-ïðîöåññîâ. Ïîñêîëüêó çàäà÷à ôîðìàëüíîé âåðèôèêàöèè
áèçíåñ-ïðîöåññîâ â îáùåì ñëó÷àå íåðàçðåøèìà, âîçíèêàåò íåîáõîäèìîñòü ïî-
ñòðîåíèÿ ôîðìàëüíî âåðèôèöèðóåìûõ ïîäêëàññîâ áèçíåñ-ïðîöåññîâ, ïðåäñòàâ-
ëÿþùèõ ïðàêòè÷åñêèé èíòåðåñ. Èçâåñòíî, ÷òî 70 % ñòîèìîñòè óïðàâëåíèÿ áèç-
íåñ-ïðîöåññàìè òðàòèòñÿ íà îáñëóæèâàíèå ñóùåñòâóþùèõ ïðîöåññîâ è òîëüêî
30 % — íà ðàçðàáîòêó íîâûõ [1]. Èçâåñòíî òàêæå, ÷òî íà ïåðåïðîåêòèðîâàíèå
ñóùåñòâóþùèõ ïðîöåññîâ òðàòèòñÿ ñâûøå 300 ìëí äîë. â ãîä [1, 2]. Ýòî ïðè-
âîäèò ê íåîáõîäèìîñòè ñîçäàíèÿ áèáëèîòåê øàáëîíîâ áèçíåñ-ïðîöåññîâ èëè
áèáëèîòåê ïàðàìåòðèçîâàííûõ îïèñàíèé ïðîöåññîâ, èç êîòîðûõ ìîæíî ïîëó-
÷àòü êîíêðåòíûå ïðîöåññû ïóòåì çàäàíèÿ çíà÷åíèé ïàðàìåòðîâ [3].  ðàáîòå
îïðåäåëÿåòñÿ ôîðìàëüíî âåðèôèöèðóåìûé ïîäêëàññ øàáëîíîâ áèçíåñ-ïðîöåñ-
ñîâ, êîòîðûé, êàê ïîêàçàíî äàëåå, ñîäåðæèò âñå øàáëîíû íåêîòîðûõ øèðîêî
èñïîëüçóåìûõ áèáëèîòåê øàáëîíîâ [3, 4].
Ðàññìàòðèâàåìûé ïîäêëàññ øàáëîíîâ îïðåäåëÿåòñÿ çàäàíèåì áàçîâûõ ýëå-
ìåíòîâ è îïåðàöèé íàä íèìè, ñ ïîìîùüþ êîòîðûõ ìîæíî ïîñòðîèòü ïðîèçâîëü-
íûé øàáëîí ïîäêëàññà. Ïîêàçàíî, ÷òî çàäà÷à ôîðìàëüíîé âåðèôèêàöèè øàáëî-
íîâ ñâîäèòñÿ ê çàäà÷å ôîðìàëüíîé âåðèôèêàöèè áàçîâûõ ýëåìåíòîâ. Ïîñòðîåíû
àëãîðèòìû ïîëèíîìèàëüíîé ñëîæíîñòè äëÿ âåðèôèêàöèè ýëåìåíòîâ øàáëîíîâ,
íà îñíîâå êîòîðûõ ïîñòðîåí îáùèé àëãîðèòì âåðèôèêàöèè, òàêæå èìåþùèé ïî-
ëèíîìèàëüíóþ ñëîæíîñòü.
 êà÷åñòâå áàçîâîé ìîäåëè âûáðàíà ìîäåëü, îïèñàííàÿ â IBM MQSeries
Workflow [7]. Ýòà ìîäåëü ðàñøèðåíà ñ ïîìîùüþ êîíñòðóêöèé, íåîáõîäèìûõ äëÿ
ðàññìîòðåíèÿ çàäà÷è ôîðìàëüíîé âåðèôèêàöèè, êîòîðàÿ ïðåäïîëàãàåò çàäàíèå
ïðåä- è ïîñòóñëîâèé ïðîöåññà, ò.å. óñëîâèé íà÷àëà è çàâåðøåíèÿ ïðîöåññà. Ïðî-
öåññ íàçûâàåòñÿ (÷àñòè÷íî) êîððåêòíûì, åñëè âñÿêèé ðàç ïðè óäîâëåòâîðåíèè
ïðåäóñëîâèÿ ïðîöåññà è åãî óñïåøíîãî çàâåðøåíèÿ óäîâëåòâîðÿåòñÿ ïîñòóñëîâèå
ïðîöåññà. Ïðîöåññ íàçûâàåòñÿ (ïîëíîñòüþ) êîððåêòíûì, åñëè âñÿêèé ðàç ïðè
óäîâëåòâîðåíèè ïðåäóñëîâèþ ïðîöåññ çàâåðøàåòñÿ è óäîâëåòâîðÿåòñÿ ïîñòóñëî-
âèå ïðîöåññà.
 íàñòîÿùåé ñòàòüå ðàññìàòðèâàåòñÿ ïðîáëåìà ÷àñòè÷íîé êîððåêòíîñòè (äà-
ëåå — êîððåêòíîñòè) äëÿ øàáëîíîâ áèçíåñ-ïðîöåññîâ.
1. ÔÎÐÌÀËÜÍÀß ÌÎÄÅËÜ ÁÈÇÍÅÑ-ÏÐÎÖÅÑÑÎÂ
Íèæå îïðåäåëÿåòñÿ ôîðìàëüíàÿ ìîäåëü áèçíåñ-ïðîöåññîâ íà áàçå IBM
MQSeries Workflow [7].
1.1. Ìîäåëü ïðîöåññà. Îñíîâíûìè ýëåìåíòàìè ïðîöåññà ÿâëÿþòñÿ îïåðàòî-
ðû äåéñòâèé (activities) (äàëåå — îïåðàòîðû). Îïåðàòîðû èìåþò êîíòåéíåðû âõî-
äà è âûõîäà, êàæäûé ñîñòîèò èç êîíå÷íîãî íàáîðà ÿ÷ååê. Âûïîëíåíèå îïåðàòîðà
ïðåîáðàçóåò ñîñòîÿíèå êîíòåéíåðà âõîäà â ñîñòîÿíèå êîíòåéíåðà âûõîäà. Íà
ìíîæåñòâå ÿ÷ååê êîíòåéíåðîâ îïðåäåëåíà ñåòü, ïî êîòîðîé îñóùåñòâëÿåòñÿ ïåðå-
62 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 2
© À.Ñ. Âàðîñÿí, 2011
äà÷à äàííûõ. Òîïîëîãèÿ ñåòè çàäàåòñÿ èçíà÷àëüíî è íå ìåíÿåòñÿ â õîäå ôóíêöèîíè-
ðîâàíèÿ ïðîöåññà. Îïåðàòîðû ñâÿçûâàþòñÿ ìåæäó ñîáîé êîííåêòîðàìè, êàæäûé
íàäåëÿåòñÿ óñëîâèåì ïåðåõîäà. Êðîìå òîãî, ñõîäÿùèåñÿ â îáùåé òî÷êå êîííåêòî-
ðû íàäåëÿþòñÿ óñëîâèåì ñîåäèíåíèÿ, îïðåäåëÿþùèì âîçìîæíîñòü ïðîõîæäåíèÿ
ïîòîêà óïðàâëåíèÿ ÷åðåç ýòó òî÷êó.
Ñóùåñòâóþùèå ôîðìàëüíûå ìîäåëè ïðîöåññîâ àöèêëè÷åñêèå [7], ò.å. óïðàâ-
ëÿþùèé ãðàô ïðîöåññà íå ñîäåðæèò öèêëîâ. Â òî æå âðåìÿ íå ïðàêòèêå èñïîëüçó-
þòñÿ áèçíåñ-ïðîöåññû, ó êîòîðûõ óïðàâëÿþùèé ãðàô ñîäåðæèò öèêëû. Â ðàáîòå
ïîñòðîåíî ðàñøèðåíèå ôîðìàëüíîé ìîäåëè [7] äëÿ ïðåäñòàâëåíèÿ òàêæå öèêëè÷åñ-
êèõ ïðîöåññîâ. Äëÿ öèêëè÷åñêîãî ïðîöåññà îïðåäåëÿþòñÿ âíóòðåííèå è âíåøíèå
êîííåêòîðû. Âíóòðåííèå êîííåêòîðû óêàçûâàþò íà âõîäíóþ âåðøèíó öèêëà è
ïðèíàäëåæàò åìó. Âñå îñòàëüíûå êîííåêòîðû âíåøíèå. Äëÿ âíóòðåííèõ êîííåêòî-
ðîâ, ñâÿçûâàþùèõ îïåðàòoðû öèêëà ñ åãî âõîäíîé âåðøèíîé, îïðåäåëåíî âíóòðåí-
íåå óñëîâèå ñîåäèíåíèÿ. Âõîäíàÿ âåðøèíà öèêëà ìîæåò áûòü àêòèâèçèðîâàíà êàê
èçâíå, òàê è ïðè èñòèííîì çíà÷åíèè óñëîâèÿ âíóòðåííåãî ñîåäèíåíèÿ.
Íèæå îïðåäåëÿþòñÿ àöèêëè÷åñêèå è öèêëè÷åñêèå áèçíåñ-ïðîöåññû íà îñíî-
âå W-ïðîöåññà [5]. Èñïîëüçóþòñÿ ñëåäóþùèå îáîçíà÷åíèÿ:
— äëÿ êîðòåæà x x x n�� � �1, , è ïîñëåäîâàòåëüíîñòè èíäåêñîâ
1 1� � �i i nk, , � i ik x1, , ( )� îáîçíà÷àåò êîðòåæ � � �x xi ik1, , .
— äëÿ ìíîæåñòâà X X�( ) îáîçíà÷àåò ìíîæåñòâî âñåõ ïîäìíîæåñòâ X .
Îïðåäåëåíèå. W-ïðîöåññ îïðåäåëÿåòñÿ êàê êîðòåæ P T V N C�� , , , , E, ,�
i o, , ,
�, â êîòîðîì ïðèíÿòû ñëåäóþùèå îáîçíà÷åíèÿ.
1. T — êîíå÷íîå ìíîæåñòâî òèïîâ.
Îáîçíà÷åíèå DOM( )t áóäåì èñïîëüçîâàòü äëÿ ìíîæåñòâà çíà÷åíèé òèïà
t T� . Áåç îãðàíè÷åíèÿ îáùíîñòè äëÿ ïeðåìåííîé � òèïà t îòîæäåñòâèì DOM( )� ñ
DOM( )t . Îáîçíà÷èì V ìíîæåñòâî âñåõ ïåðåìåííûõ.
2. N — êîíå÷íîå ìíîæåñòâî îïåðàòîðîâ, íàäåëåííûõ ïðèîðèòåòàìè.
3. C — êîíå÷íîå ìíîæåñòâî óñëîâèé ïåðåõîäà.
4. E N N C�
— ìíîæåñòâî êîííåêòîðîâ. Åñëè e A A c E�� � ��, , , òî áóäåì
ãîâîðèòü, ÷òî êîííåêòîð e ñ óñëîâèåì ïåðåõîäà c ñîåäèíÿåò îïåðàòîð A ñ îïåðà-
òîðîì A�. Ïðåäïîëàãàåì, ÷òî êîííåêòîð îäíîçíà÷íî îïðåäåëÿåòñÿ ñîåäèíÿåìûìè
îïåðàòîðàìè: � �� � � � � �e e E e e e e, : ( ) ( ) ( ) ( ), ,� � � �1 2 1 2 3 3 .
5. �: N F� — îòîáðàæåíèå, ñîïîñòàâëÿþùåå îïåðàòîðó A N� óñëîâèå ñîå-
äèíåíèÿ �( )A . Ñ÷èòàåì, ÷òî �( )A �1, åñëè A íå èìååò âõîäíûõ êîííåêòîðîâ.
6. i N C V: � � — îòîáðàæåíèå, ñîïîñòàâëÿþùåå îïåðàòîðó èëè óñëîâèþ ïå-
ðåõîäà êîíòåéíåð âõîäà. Ïîñëåäíèé ïðåäñòàâëÿåò ñîáîé êîðòåæ ðàçëè÷íûõ ïåðå-
ìåííûõ, êàæäàÿ èç êîòîðûõ ïðèíàäëåæèò íåêîòîðîìó òèïó èç ìíîæåñòâà T.
7. o N V: � — îòîáðàæåíèå, ñîïîñòàâëÿþùåå îïåðàòîðó êîíòåéíåð âûõîäà.
Ïîñëåäíèé ïðåäñòàâëÿåò ñîáîé êîðòåæ ðàçëè÷íûõ ïåðåìåííûõ, êàæäàÿ èç êîòî-
ðûõ ïðèíàäëåæèò íåêîòîðîìó òèïó èç ìíîæåñòâà T.
8. : N C E� � — îòîáðàæåíèå, ñîïîñòàâëÿþùåå îïåðàòîðó èëè óñëîâèþ
ïåðåõîäà ñåìàíòèêó âûïîëíåíèÿ. Ïðè ýòîì ñåìàíòèêà âûïîëíåíèÿ îïåðàòîðà
A N� îïðåäåëÿåòñÿ êàê îòîáðàæåíèå ( ): ( ) ( )
( ) ( )A
i A o A
�
� �� �� �DOM DOM ,
à ñåìàíòèêà âûïîëíåíèÿ óñëîâèÿ p C� — êàê îòîáðàæåíèå
( ): ( ) { ,( )p i p
��� �DOM }0 1 .
9.
: ( ) ( ( ) ( )),N N C o A i BA N B N C
� � � �
� � � — îòîáðàæåíèå, ñîïîñòàâ-
ëÿþùåå êàæäîé ïàðå âèäà <îïåðàòîð, îïåðàòîð> èëè <îïåðàòîð, óñëîâèå ïåðåõîäà>
áèíàðíîå îòíîøåíèå íà ìíîæåñòâå ïåðåìåííûõ êîíòåéíåðà âûõîäà ïåðâîãî êîìïî-
íåíòà è êîíòåéíåðà âõîäà âòîðîãî. Òðåáóåòñÿ âûïîëíåíèå ñëåäóþùèõ îãðàíè÷åíèé:
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 2 63
• [ , ] ( , ) ( ) ( ),A N B N C A B o A i B� � � � �
• [ , , , ( , ),A N B N C A B� � � � ���� �1
• � ��� � �� � � �2 1 2, ( , )] ,
A B
• � ��� � � �� � � �, ( , ) ( ) ( ).
X Y DOM DOM
Îòìåòèì, ÷òî îïðåäåëåíèå W-ïðîöåññà îòëè÷àåòñÿ îò ìîäåëè IBM [7] òåì,
÷òî Å íå ÿâëÿåòñÿ àöèêëè÷åñêèì.
Îïðåäåëåíèå àöèêëè÷åñêîãî ïðîöåññà â [7] îòëè÷àåòñÿ îò ïðèâåäåííîãî äî-
ïîëíèòåëüíûì îãðàíè÷åíèåì: â ï. 4 Å — àöèêëè÷åñêèé ãðàô.
Ãðàôû ïðîöåññà G N E( , ) è G N( , )
íàçûâàþò ãðàôîì óïðàâëåíèÿ è ãðàôîì
ïåðåäà÷è äàííûõ ñîîòâåòñòâåííî. A e E e A� � � �{ }| ( )�1 — ìíîæåñòâî îïåðàòî-
ðîâ, ñëåäóþùèõ çà îïåðàòîðîì A N� â ãðàôå óïðàâëåíèÿ, è
A e E e A� � � �{ | ( )�2 } — ìíîæåñòâî îïåðàòîðîâ, ïðåäøåñòâóþùèõ îïåðàòîðó A
â ãðàôå óïðàâëåíèÿ.
Îáîçíà÷èì N P( ) ìíîæåñò-
âî îïåðàòîðîâ, ñîäåðæàùèõñÿ
â P, In( )P è Out( )P — ìíîæåñòâî
ñòàðòîâûõ è êîíå÷íûõ îïåðàòî-
ðîâ ïðîöåññà P ñîîòâåòñòâåííî.
Ãðàôè÷åñêîå ïðåäñòàâëå-
íèå áèçíåñ-ïðîöåññîâ ïðèâåäå-
íî íà ðèñ. 1.
Ïóñòü � — ìíîæåñòâî âñåõ
öèêëîâ, ñîäåðæàùèõñÿ â ïðî-
öåññå P, è N C — ìíîæåñòâî
âñåõ âõîäíûõ âåðøèí öèêëîâ.
Äîïóñòèì, ÷òî � �A N ìíîæå-
ñòâî A
� îïðåäåëÿåò ìíîæåñòâî
âñåõ îïåðàòîðîâ, ñâÿçàííûõ ñ A ñ ïîìîùüþ êîííåêòîðîâ äàííûõ —
A D N A D
� � � ��{ }| ( , ) . Îáîçíà÷èì K � ìíîæåñòâî âñåõ îïåðàòîðîâ, ñîäåðæà-
ùèõñÿ â öèêëå � �� .
Îïðåäåëåíèå (îïåðàòîðû ïåðåñå÷åíèÿ öèêëîâ). Äîïóñòèì, � i ��,
1� � �i k N C| | , ÿâëÿþòñÿ öèêëàìè ïðîöåññà P. Îïåðàòîðû ïåðåñå÷åíèÿ öèêëîâ
— ýòî ìíîæåñòâî îïåðàòîðîâ, îáùèõ äëÿ âñåõ öèêëîâ: � � �1 2� ��� �k
� � ���K K K k� � �1 2 .
Äàëåå îïðåäåëÿåòñÿ ëîêàëèçîâàííûé öèêë, âïåðâûå ââåäåí Àëëåí ïðè ðàñ-
ñìîòðåíèè çàäà÷è îïòèìèçàöèè ïðîãðàìì [8].
Îïðåäåëåíèå (ëîêàëèçîâàííûé öèêë). Öèêë � �� ñ åäèíñòâåííîé âõîäíîé
âåðøèíîé a1 íàçûâàåòñÿ ëîêàëèçîâàííûì öèêëîì, åñëè åäèíñòâåííîé òî÷êîé ïå-
ðåñå÷åíèÿ ñ äðóãèìè öèêëàìè � ÿâëÿåòñÿ âõîäíàÿ âåðøèíà öèêëà: � �� �, � �� ,
� �� � { }a1 .
Îïðåäåëåíèå (âåòâÿùèéñÿ îïåðàòîð). Îïåðàòîð öèêëà íàçûâàåòñÿ âåòâÿ-
ùèìñÿ îïåðàòîðîì, åñëè èìååò õîòÿ áû îäèí âûõîäíîé êîííåêòîð óïðàâëåíèÿ,
ñîåäèíåííûé ñ îïåðàòîðîì, íå ïðèíàäëåæàùèì öèêëó: b N� ÿâëÿåòñÿ âåòâÿùèì-
ñÿ îïåðàòîðîì �� � � �� � � � �� � �� ��, , \ ( , ( ) , ( ) )e E b N K b K e b e b1 2
.
Îïðåäåëåíèå (ñîãëàñîâàííûå îïåðàòîðû). Îïåðàòîðû A è À� íàçîâåì ñî-
ãëàñîâàííûìè îïåðàòîðàìè, åñëè îíè ñâÿçàíû êîííåêòîðàìè ïåðåäà÷è äàííûõ
òîëüêî òîãäà, êîãäà ñâÿçàíû òàêæå êîííåêòîðîì óïðàâëåíèÿ: � ��A À N, ,
( , )À À� � � � �� �À A .
64 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 2
o
Êîíòåéíåð âõîäà
Îïåðàòîð
Êîíòåéíåð
Êîííåêòîð
ïåðåäà÷è
äàííûõ
Êîííåêòîð
ïåðåõîäà
Ðèñ. 1
A1
o o ot1 2 ...
A3
A2
âûõîäà
Îáîçíà÷èì C AC� ( ) ìíîæåñòâî âñåõ óñëîâèé ïåðåõîäîâ, ïðèíàäëåæàùèõ
êîííåêòîðàì, ñîäåðæàùèìñÿ â öèêëàõ ñ âõîäíîé âåðøèíîé A N C� è óêàçûâàþ-
ùèì íà îïåðàòîð A. Îáîçíà÷èì C A* ( )� ìíîæåñòâî âñåõ óñëîâèé ïåðåõîäîâ,
ïðèíàäëåæàùèõ êîííåêòîðàì, íå ñîäåðæàùèìñÿ â öèêëàõ ñ âõîäíîé âåðøèíîé
A N C� è óêàçûâàþùèì íà îïåðàòîð A.
Íèæå îïðåäåëÿþòñÿ ñâîäèìûå àöèêëè÷åñêèå è öèêëè÷åñêèå ïðîöåññû. Îñíî-
âîé äëÿ èõ îïðåäåëåíèÿ ÿâëÿþòñÿ ïîíÿòèÿ ñòðóêòóðíîãî ïðîãðàììèðîâàíèÿ [9].
1.2. Ñâîäèìîñòü. Îïðåäåëåíèå (ñâîäèìûé àöèêëè÷åñêèé ïðîöåññ). Êàæ-
äûé W-ïðîöåññ, èìåþùèé àöèêëè÷åñêèé ãðàô óïðàâëåíèÿ, íàçîâåì ñâîäèìûì
àöèêëè÷åñêèì ïðîöåññîì, èëè A-ïðîöåññîì, åñëè:
1) � � � � �� �A N A A;| | | | ;1 1
2) � � � �� �� � � � ��� � � � �� � � � �A N A A A A A A A; | | (| | & ; | | );1 1 1
3) � �A N è À N�� — ñîãëàñîâàííûå îïåðàòîðû.
Îïðåäåëåíèå (ñâîäèìûé öèêëè÷åñêèé ïðîöåññ). Êàæäûé W-ïðîöåññ íàçî-
âåì ñâîäèìûì öèêëè÷åñêèì ïðîöåññîì, èëè C-ïðîöåññîì. Ïðè ýòîì äîëæíû âû-
ïîëíÿòüñÿ ñëåäóþùèå óñëîâèÿ.
1. Âñå öèêëû ãðàôà óïðàâëåíèÿ ÿâëÿþòñÿ ëîêàëèçîâàííûìè öèêëàìè.
2. �: N FC � îòîáðàæåíèå ñîïîñòàâëÿåò îïåðàòîðó A N C� âíåøíåå óñëî-
âèå ñîåäèíåíèÿ �( )A . Ïîñëåäíåå îïðåäåëÿåòñÿ êàê âûðàæåíèå áóëåâîé àëãåáðû,
çàâèñÿùåå îò ìíîæåñòâà ïåðåìåííûõ C A* ( )� .
3. �C CN F: � îòîáðàæåíèå ñîïîñòàâëÿåò îïåðàòîðó A N C� âíóòðåííåå
óñëîâèå ñîåäèíåíèÿ �C A( ) . Ïîñëåäíåå îïðåäåëÿåòñÿ êàê âûðàæåíèå áóëåâîé àë-
ãåáðû, çàâèñÿùåå îò ìíîæåñòâà ïåðåìåííûõ C AC� ( ) . Ïðåäïîëîæèì, ÷òî
� � �A N AC C, ( )� 0 .
4. � �A N C ìîæåò áûòü àêòèâèçèðîâàí � � �( ( )( ( ), , ( )) )� A i p i pnA1
1�
� � ��( ( )( ( ), , ( )) ), ( ) , ,*�C mA nAA i q i q C A p p1 11� �{ } , C A q qC
mA
� �( ) , ,{ }1 � .
5. � �A N è À N�� ÿâëÿþòñÿ ñîãëàñîâàííûìè îïåðàòîðàìè.
6. � � � � �� �A N A A;| | | |1 1.
7. A N A A A A A A A� � � � �� � � � ��� � � � �� � � � �; | | (| | & ; | | )1 1 1 .
Äàëåå ðàññìàòðèâàþòñÿ òîëüêî ñâîäèìûå áèçíåñ-ïðîöåññû.
1.3. Ôîðìàëüíàÿ âåðèôèêàöèÿ áèçíåñ-ïðîöåññîâ. Ââåäåíû òàêæå íîâûå
ïîíÿòèÿ, íåîáõîäèìûõ äëÿ ôîðìàëüíîé âåðèôèêàöèè.
Îïðåäåëåíèå (êîððåêòíîñòü áèçíåñ-ïðîöåññà). Ïóñòü P — áèçíåñ-ïðîöåññ,
� — ïðåäèêàò, çàâèñÿùèé îò íåêîòîðûõ âõîäíûõ ïåðåìåííûõ îïåðàòîðîâ, à � —
ïðåäèêàò, çàâèñÿùèé îò íåêîòîðûõ âûõîäíûõ ïåðåìåííûõ îïåðàòîðîâ. Íàçîâåì �
è � ïðåä- è ïîñòóñëîâèåì ñîîòâåòñòâåííî.  ýòîì ñëó÷àå áèçíåñ-ïðîöåññ P êîððåê-
òåí îòíîñèòåëüíî � è � òîãäà è òîëüêî òîãäà, êîãäà [ ( ) ( ) ],� �P MP� � �1 1 ãäå
MP — ñîñòîÿíèå âûõîäíûõ ïåðåìåííûõ îïåðàòîðîâ ïîñëå âûïîëíåíèÿ ïðîöåññà P.
Ïóñòü çàäàíû ïðåäóñëîâèå è ïîñòóñëîâèå ïðîöåññà P.
Îïðåäåëåíèå (ñóùåñòâåííàÿ âûõîäíàÿ ïåðåìåííàÿ). Âûõîäíàÿ ïåðåìåí-
íàÿ ïðîöåññà P íàçûâàåòñÿ ñóùåñòâåííîé, åñëè âûñòóïàåò ïåðåìåííîé âûõîäíîãî
êîíòåéíåðà íåêîòîðîãî îïåðàòîðà A N� , îò êîòîðîé çàâèñèò ïîñòóñëîâèå.
Îáîçíà÷èì Ì P( ) ìíîæåñòâî ñóùåñòâåííûõ âûõîäíûõ ïåðåìåííûõ áèçíåñ-
ïðîöåññà P.
Äîáàâèì ê êàæäîìó âåòâÿùåìóñÿ îïåðàòîðó íîâóþ ïåðåìåííóþ r, íàçûâàå-
ìóþ ðåãèñòðîì ñîñòîÿíèÿ è ïðèíèìàþùóþ îäíî èç çíà÷åíèé { }0 1 2, , , .�
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 2 65
1. 0 îçíà÷àåò, ÷òî âåòâÿùèéñÿ îïåðàòîð ïîêà íå âûïîëíåí.
2. n n;( )��1 îçíà÷àåò, ÷òî âåòâÿùèéñÿ îïåðàòîð âûïîëíåí n ðàç.
Ïóñòü P — áèçíåñ-ïðîöåññ è X N C� � . Òîãäà íàçîâåì ñîñòîÿíèåì áèç-
íåñ-ïðîöåññà êîðòåæ, ñîñòîÿùèé èç ïåðåìåííûõ âõîäíûõ êîíòåéíåðîâ îïåðàòî-
ðîâ, óñëîâèé ïåðåõîäà è ñóùåñòâåííûõ âûõîäíûõ ïåðåìåííûõ. Îáîçíà÷èì
B YY N C M�
� � � States( ) äëÿ ìíîæåñòâà âñåõ ñîñòîÿíèé ïðîöåññà, ãäå
States( ) ( )X i X�
�� è States( )M �
��
�
M
DOM( ) , b X( ) — ñîñòîÿíèå
X N C M� � � äëÿ b B� .
Ïóñòü b B A N� �, . Îáîçíà÷èì bA b� � íîâîå ñîñòîÿíèå ïðîöåññà, ïîëó÷åííîå
ïîñëå âûïîëíåíèÿ îïåðàòîðà A ïðè ñîñòîÿíèè ïðîöåññà b. Ïðîöåññ b� îïðåäåëÿ-
åòñÿ ñëåäóþùèì îáðàçîì:
( ( ))
( ( )) , ( )[ , ( , )],
( (
b X
b X î A A X
A
� �
� � � ���
�
�
�
� � � �åñëè
)( ( ))) , , ( , ),b A A X� � �åñëè � ���
�
�
äëÿ âñåõ X N C M� � � .
Äîïóñòèì, b B0 � — íà÷àëüíîå ñîñòîÿíèå ïðîöåññà äî åãî âûïîëíåíèÿ. Ïóñòü
b b P�
0
— ñîñòîÿíèå ïðîöåññà ïîñëå åãî âûïîëíåíèÿ [7], à MP — ìíîæåñòâî çíà-
÷åíèé ñóùåñòâåííûõ âûõîäíûõ ïåðåìåííûõ ñîñòîÿíèÿ b ïîñëå åãî âûïîëíåíèÿ.
Äàëåå ïîêàæåì, ÷òî äëÿ ïîäêëàññà ñâîäèìûõ áèçíåñ-ïðîöåññîâ, íàçûâàåìûõ
êëàññîì øàáëîíîâ áèçíåñ-ïðîöåññîâ [3–6], ñóùåñòâóåò áàçèñ ýëåìåíòàðíûõ ïðî-
öåññîâ — ïðèìèòèâîâ, è ñîîòâåòñòâóþùèå îïåðàöèè íàä ýòèì áàçèñîì, ñ ïî-
ìîùüþ êîòîðûõ ìîæíî ïîñòðîèòü ïðîèçâîëüíûé øàáëîí áèçíåñ-ïðîöåññà.
2. ØÀÁËÎÍÛ ÁÈÇÍÅÑ-ÏÐÎÖÅÑÑÀ
Ââåäåì îãðàíè÷åíèÿ íà òèïû è ðåàëèçàöèè, êîòîðûå ñîîòâåòñòâóþò øàáëîíàì
áèçíåñ-ïðîöåññîâ:
1) T P TB TG( ) ,� { } , ãäå TB TG� �{Unknown, True False} {Unknown, Known}, , ;
2) � � � �A N o A TG A( ( ( )) , ( )DOM ‘Known’).
Òàêèå áèçíåñ-ïðîöåññû íàçûâàþò óíèôèöèðîâàííûìè áèçíåñ-ïðîöåññàìè
(äàëåå — áèçíåñ-ïðîöåññ). Íèæå ðàññìàòðèâàþòñÿ òðè òèïà ïðèìèòîâîâ, èñïîëü-
çóåìûõ â ïîñòðîåíèè ïðîöåññîâ.
2.1. Ïðèìèòèâû. Îïðåäåëåíèå (òèïû ïðèìèòèâîâ). Ïðîñòîé ïðèìèòèâ —
ýòî ïðîñòîé îïåðàòîð. Íàïðèìåð, � �a N — ïðîñòîé ïðèìèòèâ, In( )u �Out( )u �
� �N u a( ) { } .
• Ïðèìèòèâ ñèíõðîíèçàöèè u — óçåë ñîåäèíåíèÿ ñâÿçûâàþùèõ êîííåêòîðîâ,
a a a N e a a c E e a a cm m m m m m1 2 1 1 1 1 1 1, , , , , , , , , ,� � �� �� � �� �! ! ! �E,
c c C c c cm m1 1 1 2 1 1, , ,� ! !� � ��� � ,
N u a a a u a a u am m m( ) , , , , ( ) , , , ( )� � � � �!{ } In { } Out { }1 2 1 1 .
• Ïðèìèòèâ ðàçäåëåíèÿ u — âåòâÿùèéñÿ óçåë âûõîäíûõ êîííåêòîðîâ,
a a a N e a a c E em m1 2 1 1 2 1 1, , , , , , ,� � �� �� �!
�� �� �! !a a c E c c Cm m m1 1 1 1, , , , ,� ,
N u a a a u a u a am m( ) , , , , ( ) , ( ) , ,� � � � �{ } In { } Out { }1 2 1 2 .
Ñõåìû ïðèìèòèâîâ ïðåäñòàâëåíû íà ðèñ. 2.
66 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 2
Îáîçíà÷èì ìíîæåñòâà îïåðàòîðîâ è óïðàâëÿþùèõ êîííåêòîðîâ, ñîäåðæà-
ùèõñÿ â u, ñîîòâåòñòâåííî N u è Eu . Ïóñòü U P( ) — ìíîæåñòâî âñåõ ïðèìèòèâîâ,
ñîäåðæàâøèõñÿ â P áèçíåñ-ïðîöåññå. Îáîçíà÷èì òàêæå òèï ïðèìèòèâà u ÷åðåç
type ( )u � {ïðîñòîé, ñèíõðîíèçàöèÿ, ðàçäåëåíèå}. Ïðåäïîëîæèì, ÷òî BU — ìíî-
æåñòâî âñåõ âîçìîæíûõ ïðèìèòèâîâ. Ïðîñòûå ïðèìèòèâû, à òàêæå ïðèìèòèâû
ðàçäåëåíèÿ íàçîâåì ïðèìèòèâíûìè àöèêëè÷åñêèìè øàáëîíàìè.
Íèæå îïðåäåëåíû äâå îïåðàöèè: êîíêàòåíàöèè è ñëèÿíèÿ, èñïîëüçóþùèåñÿ
äëÿ ðåêóðñèâíîãî ïîñòðîåíèÿ íîâûõ àöèêëè÷åñêèõ øàáëîíîâ BPT ñ ïðèâëå÷åíè-
åì ïîñòðoåííûõ.  êà÷åñòâå íà÷àëüíûõ øàáëîíîâ ðàññìaòðèâàþòñÿ ïðèìèòèâ-
íûå àöèêëè÷åñêèå øàáëîíû.
2.2. Àëãåáðà øàáëîíîâ áèçíåñ-ïðîöåññîâ. Îïðåäåëåíèå (îïåðàöèÿ êîíêà-
òåíàöèè). Êîíêàòåíàöèÿ P P P k c� �Concat( , , , )1 2 äâóõ àöèêëè÷åñêèõ øàáëîíîâ P1
è P2 òàêèõ, ÷òî In Out( ) { }, ( ) { , , },P ip P op opk1 1 1 1 1� � � In ,( )P ip2 1� � Out( )P �
� � � �{ , , },op op
k1 2
k k1 2 0, � , — ýòî àöèêëè÷åñêèé øàáëîí òàêîé, ÷òî:
P Cn P P k c P Pc k� � � "( , , , ) ,1 2 1 2 ÿâëÿåòñÿ áèçíåñ-ïðîöåññîì ñ ãðàôîì G N E( , ) ,
ãäå
N N P N P C C P C P c� � � � �( ) ( ), ( ) ( )1 2 1 2 ,
E E P E P op ip c k kk� � �� � � � �( ) ( ) , , ,1 2 1
1 1,
� � � � � �( ) ( ) ( , ), ( ) ( ) .P P op ip M M P M Pk1 2 1 1 2
Îïðåäåëåíèå (îïåðàöèÿ ñëèÿíèÿ). Ñëèÿíèå P u P k c� � Merge( , , , ) ïðèìèòèâà
ñèíõðîíèçàöèè u ñ àöèêëè÷åñêèì øàáëîíîì P òàêèì, ÷òî In { }( ) ,P ip� 1 Out( )P �
{ }op opko1, , ,� ko � 0, In { }( ) , , ,u iu iu m� �1 Out { }( ) ,u ou� 1 1� �m ko, — ýòî àöèê-
ëè÷åñêèé øàáëîí òàêîé, ÷òî:
P u P k c P
k c
� � � #Merge( , , , )
,
— áèçíåñ-ïðîöåññ ñ ãðàôîì G N E( , ) , ãäå
c c c k k km m�� � � �� � �1 1, , , , , , ãäå k P k k i j i j mi i j� � � � �Out( ), , , ,1 ,
N N u N P C C u C P c M M u M P� � � � � � �( ) ( ), ( ) ( ) , ( ) ( ),
E E u E P� � �( ) ( )
� � �( ) ( )u P
�� � � �� �op iu c op iu ck k m mm1 1 1, , , ,� � � �
( , ) ( , )op iu op iuk k mm1 1 � .
Çäåñü c — óñëîâèå îïåðàöèè äëÿ êîíêàòåíàöèè, â òî âðåìÿ êàê c — óñëîâèå
îïåðàöèè äëÿ ñëèÿíèÿ. Îáîçíà÷èì ñ ïîìîùüþ c u( ) óñëîâèå îïåðàöèè êîíêàòåíà-
öèè èëè ñëèÿíèÿ ïðèìèòèâà u ñ àöèêëè÷åñêèì øàáëîíîì P. Áóäåì ñ÷èòàòü, ÷òî
c u( ) �1, åñëè ïðèìèòèâ íå êîìáèíèðîâàí ñ øàáëîíîì.
Îïðåäåëåíèå (ðåãóëÿðíûé àöèêëè÷åñêèé øàáëîí). Êàæäûé àöèêëè÷åñêèé
øàáëîí, ïîñòðîåííûé èç ìíîæåñòâà ïðèìèòèâîâ BU BU� � ñ èñïîëüçîâàíèåì îïå-
ðàöèé êîíêàòåíàöèè è ñëèÿíèÿ, íàçûâàþò ðåãóëÿðíûì àöèêëè÷åñêèì øàáëîíîì.
Ëåììà 1. Äëÿ êàæäîãî ðåãóëÿðíîãî àöèêëè÷åñêîãî øàáëîíà ñóùåñòâóåò
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 2 67
…
Ðèñ. 2
Ïðîñòîé ïðèìèòèâ Ïðèìèòèâ ñèíõðîíèçàöèè Ïðèìèòèâ ðàçäåëåíèÿ
a1
a1 am!1
am a2 am
a1...
i i ik1 2 ...
o o ot1 2 ...
ïîäìíîæåñòâî ïðèìèòèâîâ BU BU� � òàêîå, ÷òî øàáëîí ìîæíî ïðåäñòàâèòü â
âèäå ïîñëåäîâàòåëüíîñòè îïåðàöèé êîíêàòåíàöèè è ñëèÿíèÿ íàä BU �.
Òàêîå ïðåäñòàâëåíèå íàçîâåì ðàçëîæåíèåì øàáëîíîâ íà ïðèìèòèâû. Ïîêà-
æåì, ÷òî êàæäîìó øàáëîíó îäíîçíà÷íî ñîîòâåòñòâóåò îïðåäåëåííàÿ ïîñëåäîâà-
òåëüíîñòü îïåðàöèé íàä ïðèìèòèâàìè.
Àëãîðèòì D. Ðàçëîæåíèå øàáëîíà íà ïðèìèòèâû
Âõîä: Àöèêëè÷åñêèé øàáëîí P ñ ãðàôîì G N E( , ) .
Âûõîä: Ïîñëåäîâàòåëüíîñòü îïåðàöèé êîíêàòåíàöèè è ñëèÿíèÿ íàä ïðèìè-
òèâàìè
Ìåòîä:
1. Äëÿ âñåõ A N� âûïîëíèòü
• Åñëè | |A� � 0 , òî äîáàâèòü A ê Front ! ó
2. bUnit � � �0, ,N N E Ep p
3. Ïoêà !bUnit âûïîëíèòü
3.1. Âûáðàòü A èç Front-à
3.2. N A Eu u� ��{ , ,} N N A k cp p� ��� �� ��/ , , ,{ } typeOP
3.3. Åñëè | | ,A� � 1 òî:
a) bUnit typeOP Merge� �1,
b) Äëÿ âñåõ e A e A A p� � �� , ( , , ), âûïîëíèòü
• N N A N N A E E e E E eu u p p u u p p� � � � � � � �{ } { } { } { }, / , , /
• äîáàâèòü A� ê k, äîáàâèòü p ê c
3.4. Èëè åñëè | | , , ,A A A A p� �� � � � �1 { } , òî:
a) typeOP Concat� � � �, ,k A c p
b) åñëè | |A� �� 1, òî bUnit � 1
c) èíà÷å åñëè A� �� Front, òî N Au � � �{ } bUnit, 1
d) äëÿ âñåõ e A e A A p� � � � � �� , ( , , ) âûïîëíèòü
• N N A N N A E E e E E eu u p p u u p p� � �� � �� � � �{ } { } { } { }, / , , /
e) Èíà÷å óäàëèòü A èç Front-à
3.5. Âîçâðàòèòü typeOP( , , ( , ), , )� �N E D N E k cu u p p .
Çäåñü è äàëåå âìåñòî âûðàæåíèÿ «ðåãóëÿðíûé àöèêëè÷åñêèé øàáëîí» èñ-
ïîëüçóåòñÿ òåðìèí «àöèêëè÷åñêèé øàáëîí». Ñëåäóþùàÿ îïåðàöèÿ — îïåðàöèÿ
öèêëà, èñïîëüçóåòñÿ äëÿ ïîñòðîåíèÿ öèêëè÷åñêèõ øàáëîíîâ.
Îáîçíà÷èì path( , )a a� ìíîæåñòâî îïåðàòîðîâ, ïðèíàäëåæàùèõ ïóòè ìåæäó
a N� è a N�� .
Îïðåäåëåíèå (îïåðàöèÿ öèêëà). Îïåðàöèÿ öèêëà Cycle( , , , , , )P u u a a p� � ,
ïðèìåíåííàÿ ê øàáëîíó P, — êîìáèíàöèÿ åãî äâóõ ïðèìèòèâîâ u è u� ïîñðå-
äñòâîì ñîåäèíåíèÿ a N a Nu u� �� �, , åñëè ñóùåñòâóåò ïîñëåäîâàòåëüíîñòü ïðèìè-
òèâîâ u u u uk, , , ,1 � �, ñâÿçàííûõ îïåðàöèåé êîíêàòåíàöèè è ñëèÿíèÿ òàê, ÷òî:
° íå ñóùåñòâóåò îáðàòíîãî ïóòè ìåæäó a a a1 � �path( , ) è a a a2 � � ��path( , )
� �! ( , );path a a2 1
° type( )u� �{synchronization}, type {synchronization}( ) , ;u i ki � � �1
° åñëè type {split} { }( ) , , , , ,u u u u u uk� � � � �� � �1 , òî ïðèìèòèâ èìååò òîëüêî
äâà âçàèìíî èñêëþ÷àþùèõ óñëîâèÿ ïåðåõîäîâ.
Îïðåäåëåíèå (ðåãóëÿðíûé öèêëè÷åñêèé øàáëîí). Öèêëè÷åñêèé øàáëîí,
68 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 2
ïîñòðîåííûé íà àöèêëè÷åñêîì øàáëîíå ñ èñïîëüçîâàíèåì îïåðàöèé öèêëà, íàçû-
âàåòñÿ ðåãóëÿðíûì öèêëè÷åñêèì øàáëîíîì.
Ëåììà 2. Êàæäûé ðåãóëÿðíûé öèêëè÷åñêèé øàáëîí ðàçëàãàåòñÿ íà ïîñëåäî-
âàòåëüíîñòü îïåðàöèé öèêëà, ïðèìåíåííûõ ê àöèêëè÷åñêîìó øàáëîíó.
Àëãîðèòì ðàçëîæåíèÿ îñíîâàí íà îáíàðóæåíèè âõîäíûõ âåðøèí öèêëîâ è íà
óäàëåíèè âíóòðåííûõ êîííåêòîðîâ [8]. Çäåñü è äàëåå âìåñòî «ðåãóëÿðíîãî öèêëè-
÷åñêîãî øàáëîíà» èñïîëüçîâàí òåðìèí «öèêëè÷åñêèé øàáëîí». Íèæå ïðåäñòàâëå-
íû îïðåäåëåíèÿ àöèêëè÷åñêèõ è öèêëè÷åñêèõ øàáëîíîâ áèçíåñ-ïðîöåññîâ.
Îïðåäåëåíèå (ìíîæåñòâî àöèêëè÷åñêèõ øàáëîíîâ). AT BU�� , ,Concat
Merge � — ìíîæåñòâî ðåãóëÿðíûõ àöèêëè÷åñêèõ øàáëíîâ, êàæäûé èç êîòîðûõ
ïîñòðîåí íà ïðèìèòèâàõ BU ñ èñïîëüçîâàíèåì íóëåâîãî èëè áîëüøåãî êîëè÷åñ-
òâà îïåðàöèé Concat è Merge.
Îïðåäåëåíèå (ìíîæåñòâî öèêëè÷åñêèõ øàáëîíîâ). CT AT�� �,Cycle —
ìíîæåñòâî ðåãóëÿðíûõ öèêëè÷åñêèõ øàáëîíîâ, êàæäûé èç êîòîðûõ ïîñòðîåí íà
àöèêëè÷åñêèõ øàáëîíàõ AT ñ èñïîëüçîâàíèåì íóëåâîãî èëè áîëüøåãî êîëè÷åñ-
òâà îïåðàöèé Cycle.
Íèæå ïðåäñòàâëåíû âçàèìîñâÿçè ìåæäó øàáëîíàìè è A- è C-ïðîöåññàìè.
Ëåììà 3. Êàæäûé àöèêëè÷åñêèé øàáëîí t AT� ÿâëÿåòñÿ A-ïðîöåññîì.
Ëåììà 4. Êàæäûé öèêëè÷åñêèé øàáëîí t CT� ÿâëÿåòñÿ C-ïðîöåññîì.
Äëÿ ôîðìàëüíîé âåðèôèêàöèè àöèêëè÷åñêèõ øàáëîíîâ ìîæåò áûòü ïðåäëî-
æåí àëãîðèòì âåðèôèêàöèè A-ïðîöåññîâ [10].
Îïðåäåëåíèå (êëàññ øàáëîíîâ áèçíåñ-ïðîöåññîâ — êëàññ BPT). Êëàññîì
øàáëîíîâ áèçíåñ-ïðîöåññîâ ÿâëÿåòñÿ ìíîæåñòâî âñåõ âîçìîæíûõ àöèêëè÷åñêèõ
è öèêëè÷åñêèõ øàáëîíîâ.
3. ÇÀÄÀ×À ÔÎÐÌÀËÜÍÎÉ ÂÅÐÈÔÈÊÀÖÈÈ ØÀÁËÎÍΠÁÈÇÍÅÑ-ÏÐÎÖÅÑÑÎÂ
Îïðåäåëåíèå (ïðåäóñëîâèå èíèöèàëèçàöèè ïðèìèòèâà). Íàçîâåì �( )u ïðåä-
óñëîâèåì èíèöèàëèçàöèè ïðèìèòèâà u BU� , åñëè îíî îïðåäåëåíî äëÿ ïðîâåð-
êè íàëè÷èÿ íà÷àëüíûõ çíà÷åíèé âñåõ ïåðåìåííûõ âõîäà, çíà÷åíèÿ êîòîðûõ
îïðåäåëÿþòñÿ âíå ïðîöåññà, è èñïîëüçóåòñÿ â ïîñòóñëîâèè èëè ïðåäóñëîâèè
ïðîöåññà:
�( )
( ) ( ), ( , ( , )
u i
a u i i a x x i a
a
a
� � $% %
� � � � ���
�
�In OUT }
.
Îïðåäåëåíèå (ïîñòóñëîâèå âûïîëíåíèÿ ïðèìèòèâà). Íàçîâåì �( )u ïî-
ñòóñëîâèåì âûïîëíåíèÿ ïðèìèòèâà u BU� , åñëè îíî îïðåäåëåíî äëÿ ïðîâåðêè
ëîãèêè ïîñëåäîâàòåëüíîñòè âûïîëíåíèÿ îïåðàòîðîâ ïðèìèòèâîâ:
�( )
( ), ( ) , ( ) { },
( ) (
u
b a u u a
b a b
�
� � � �
%
ãäå type ïðîñòàÿ Act
1 a b a
u u a a
2 3
1 2
) ( ),
( ) , ( ) { ,
%
� � � �
ãäå
type ñèíõðîíèçàöèÿ Act , },
( ) ( ) ( ) ( ( ) ( ))),
a
b a pb a pb a pb a pb a
3
1 2 3 3 3% � �& % ãäå
type( ) , ( ) { , , }.u u a a a� � � �
�
�
'
''
'
'
' ðàçäåëåíèå Act 1 2 3
Íîâûå âûõîäíûå ïåðåìåííûå ( ( )b ai è pb ai( )) äîáàâëåíû äëÿ îïðåäåëåíèÿ
ïîñòóñëîâèÿ, b ai( ) «âåðíî» ïîñëå âûïîëíåíèÿ îïåðàòîðà a pb ai i, ( ) ñôîðìóëèðî-
âàí äëÿ ïðîâåðêè âûïîëíåíèÿ îïåðàòîðà ai , åñëè óäîâëåòâîðåíî óñëîâèå åãî ïå-
ðåõîäà. Ýòî îçíà÷àåò, ÷òî pb ai( ) � TRUE, åñëè ai îïåðàòîð âûïîëíåí ïîñëå óäîâ-
ëåòâîðåíèÿ ïîñòóïàþùåãî óñëîâèÿ ïåðåõîäà, â òî âðåìÿ êàê pb ai( ) � FALSE,
åñëè ai îïåðàòîð íå ìîæåò áûòü âûïîëíåí, åñëè ïîñòóïàþùåå óñëîâèå ïåðåõîäà
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 2 69
«ëîæíî».
Îïðåäåëåíèå (ïðåäóñëîâèå èíèöèàëèçàöèè BPT). Äîïóñòèì, P — øàáëîí
áèçíåñ-ïðîöåññà è � — ïðåäóñëîâèå, îïðåäåëåííîå äëÿ P ñ ïîìîùüþ ëîãè÷åñêèõ
êîìáèíàöèé ïðåäóñëîâèé èíèöèàëèçàöèè ïðèìèòèâîâ ïðîöåññà P, ñâÿçàííûõ
ìåæäó ñîáîé îïåðàöèÿìè êîíêàòåíàöèè è ñëèÿíèÿ.  ýòîì ñëó÷àå � íàçîâåì
ïðåäóñëîâèåì èíèöèàëèçàöèè ïðîöåññà P:
� �� % �
�u U P
u c u U p U P
1
1
( )
( )& ( ), ( ) ( ) .
Îïðåäåëåíèå (ïîñòóñëîâèå âûïîëíåíèÿ BPT). Äîïóñòèì, P — øàáëîí
áèçíåñ-ïðîöåññà è � — ïîñòóñëîâèå, îïðåäåëåííîå äëÿ P ñ ïîìîùüþ ëîãè÷åñêèõ
êîìáèíàöèé ïîñòóñëîâèé âûïîëíåíèÿ ïðèìèòèâîâ ïðîöåññà P, ñâÿçàííûõ ìåæäó
ñîáîé îïåðàöèÿìè êîíêàòåíàöèè è ñëèÿíèÿ.  ýòîì ñëó÷àå � íàçîâåì ïîñòóñëî-
âèåì âûïîëíåíèÿ P:
� �� �%
�u U P
u U p U P
1
1
( )
( ), ( ) ( ).
Òåîðåìà 1. Ïóñòü P — øàáëîí áèçíåñ-ïðîöåññà, à � è � — ñîîòâåòñòâåííî
ïðåäóñëîâèå èíèöèàëèçàöèè è ïîñòóñëîâèå âûïîëíåíèÿ, îïðåäåëåííûå äëÿ P. Çà-
äà÷à ôîðìàëüíîé âåðèôèêàöèè øàáëîíà P ðàçðåøèìà îòíîñèòåëüíî � è �.
Äîêàçàòåëüñòâî âûïîëíÿåòñÿ â äâà øàãà. Íà ïåðâîì ïðåäëàãàåòñÿ ïðèìåíèòü
àëãîðèòì ïðåîáðàçîâàíèÿ öèêëè÷åñêîãî øàáëîíà â àöèêëè÷åñêèé. Äàëåå ðàñ-
ñìîòðåí ôîðìàëüíûé àëãîðèòì âåðèôèêàöèè äëÿ àöèêëè÷åñêèõ BPT.
4. ÏÐÅÎÁÐÀÇÎÂÀÍÈÅ ÖÈÊËÈ×ÅÑÊÎÃÎ ØÀÁËÎÍÀ ÁÈÇÍÅÑ-ÏÐÎÖÅÑÑÀ
 ÀÖÈÊËÈ×ÅÑÊÈÉ
Íèæå ïðåäñòàâëåíû îñíîâíûå ïðîöåäóðû è îïðåäåëåíèÿ, èñïîëüçóåìûå àëãî-
ðèòìîì ïðåîáðàçîâàíèÿ, îñíîâàííîì íà èäåå èíòåðâàëîâ, ïðåäëîæåííûõ âïåð-
âûå äëÿ ïðîöåäóðû àíàëèçà ïîòîêà äàííûõ ïðîãðàììû [8], à òàêæå ñîîòâå-
òñòâóþùèå îïðåäåëåíèÿ èíòåðâàëà ôàêòîð-ãðàôà.
Äëÿ óçëà h èíòåðâàë I h( ) — ìàêñèìàëüíûé åäèíñòâåííûé ïîäãðàô âõîäà, ãäå
h — åäèíñòâåííûé óçåë âõîäà è âñå öèêëû ñîäåðæàò h. Óíèêàëüíûé óçåë èíòåðâà-
ëà h íàçûâàþò âõîäíîé âåðøèíîé èíòåðâàëà. Çäåñü è äàëåå áóäåì èñïîëüçîâàòü
îáîçíà÷åíèå a I h� ( ) âìåñòî a N I h� ( ( )) è îáîçíà÷åíèå å I h� ( ) âìåñòî å Å I h� ( ( )) .
Ïðèâåäåì ôîðìàëüíûå îïèñàíèÿ îñíîâíûõ ïðîöåäóð, èñïîëüçóåìûõ â ïðå-
îáðàçîâàíèè öèêëà.
Ïðîöåäóðà 1: construct_IntervalSet
Âõîä: Öèêëè÷åñêèé BPT P T N C E i oE C�� �, , , , , , , , ,� �
ñ ãðàôîì G N E( , )
Âûõîä: ìíîæåñòâî èíòåðâàëîâ SC
Ìåòîä:
1. Ïîñòðîèòü ìíîæåñòâî èíòåðâàëîâ S ñ ïîìîùüþ àëãîðèòìà ïîèñêà èíòåðâà-
ëîâ [18].
2. S I h S a h p E a h p I h
C
� � � � �{ }( ) | ( , , ) & ( , , ) ( ) .
3. Äëÿ âñåõ I h S
C
( )� âûïîëíèòü
L a I h a N a h I h I h L� � � �� �{ path }( ) | , ( , ) , ( ) ( ) \ ;
I h I h e I h e E e L e L( ) ( ) \ ( )| , ( ) ( ) ;� � � � �{ OR }� �1 2
4. Âîçâðàòèòü S
C
.
Âëèÿíèå íà óñëîâèÿ êîððåêòíîñòè: Íåò.
Ïðîöåäóðà 2: remove_Interval
Âõîä:
70 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 2
• Öèêëè÷åñêèé BPT P1 ñ ãðàôîì G N E1 1 1( , )
• Ìíîæåñòâî çíà÷åíèé Ì1 ñóùåñòâåííûõ âûõîäíûõ ïåðåìåííûõ
• I h( ) — èíòåðâàë
• RI h( ) — ìíîæåñòâî ðåãèñòðîâ ñîñòîÿíèÿ
Âûõîä: Öèêëè÷åñêèé BPT P2 ñ ãðàôîì G N E2 2 2( , ) . Ìíîæåñòâî çíà÷åíèé
Ì2 ñóùåñòâåííûõ âûõîäíûõ ïåðåìåííûõ.
Ìåòîä:
1. P P N N A a N a I h E E e E e II h2 1 2 1 1 2 1 1� � � � � � � �; ( ) \ { | ( ) ; \ { | (( ) } h) ;}
Ì Ì Ì�� ��1 2;
2. i A o A o A hI h I h I( ) ; ( ) ; * ( ( ))( ) ( )�� �� ��
3. Äëÿ âñåõ a I h b N b I h� � �( ), , ( ) âûïîëíèòü
3.1.
2 2( , ) ; ( , )( ) ( )b A A bI h I h�� ��
3.2. Äëÿ âñåõ ( , ) ( , )w b a� �
1 âûïîëíèòü
• Îïðåäåëèòü íîâóþ ïåðåìåííóþ �� òàê, ÷òîáû Dom Dom( ) ( )� �� �
• V V i A i AI h I h2 2� � � � � �\ ; ( ) ( )( ) ( ){ } { } } }� � �
•
2 2( , ) ( , ) ( , )
( ) ( )b A b A w
I h I h� � ��
3.3. Äëÿ âñåõ ( , ) ( , )� w a b�
1 âûïîëíèòü
• Îïðåäåëèòü íîâóþ ïåðåìåííóþ �� òàê, ÷òîáû Dom Dom } }( ) ( )� �� � � $
• V V î A î AI h I h2 2� � � � � �\ ; ( ) ( )( ) ( ){ } { } } }� � �
•
( ( , ) ( , ) ( , )( ) ( )A b A b wI h I h� � �2 �
• Åñëè �� Ì
1
, òî Ì Ì Ì Ì2 2� � � �� �� �; \
4. Äëÿ âñåõ a I h b C b I h� � �( ), , ( ) âûïîëíèòü
4.1 Äëÿ âñåõ ( , ) ( , )� w a b�
1 âûïîëíèòü
• Îïðåäåëèòü íîâóþ ïåðåìåííóþ �� òàê, ÷òîáû
Dom Dom { }( ) ( )� �� � � $
• V V î A î AI h I h2 2� � � � � �\ ; ( ) ( )( ) ( ){ } { } { }� � �
5. Äëÿ âñåõ r RI h� ( ) âûïîëíèòü
• Îïðåäåëèòü íîâóþ ïåðåìåííóþ � r òàê, ÷òîáû Dom { }( ) , ,� r � 0 12
• V V i A i Ar I h I h r2 2� � � �} } } }� �, ( ) (( ) ( ))
• o A o AI h I h r* ( ) * ( )( ) ( )� ��
6. Äëÿ âñåõ �� �M âûïîëíèòü
• Îïðåäåëèòü íîâóþ ïåðåìåííóþ �� òàê, ÷òîáû Dom Dom( ) ( )� �� �
• V V î A î A Ì ÌI h I h2 2 2 2� � � � � � � � �\ ; ( ) ( ) ,( ) ( ){ } { } { }� � � �
7. o A o A o A h
I h I h I( ) ( ) * ( ( ))
( ) ( )� �
8. ( ) | ( ) , | ( ) , * ( ( )) ;
( )
A a N a I h e E e I h o A h
I h I�� � � � � �{ } { }
9. Âîçâðàòèòü P M2 2, .
Âëèÿíèå íà óñëîâèÿ êîððåêòíîñòè:
Ñóùåñòâåííûå ïåðåìåííûå: Èçìåíåíû îáëàñòè çíà÷åíèé (øàã 4)
Ñåìàíòèêà ïðîöåññà, ïðåäóñëîâèå, ïîñòóñëîâèå: Íåò
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 2 71
Ïðîöåäóðà 3: construct_BranchActCond
Âõîä:
• Öèêëè÷åñêèé BPT P1 ñ ãðàôîì G N E1 1 1( , )
• Îïåðàòîð A èç èíòåðâàëà I h( )
• I h( ) — èíòåðâàë
• BR
I h( )
— ìíîæåñòâî âåòâÿùèõñÿ îïåðàòîðîâ
• RI h( ) — ìíîæåñòâî ðåãèñòðîâ ñîñòîÿíèé äëÿ èíòåðâàëà
Âûõîä: Óñëîâèÿ pc è p0
Ìåòîä:
1. A r r RI h) � � ��{� | ( ) — ðåãèñòð ñîñòîÿíèÿ b BRI h� ( ) è path( , )b A � � è
� r I h
o A�� * ( )
( )
— ïåðåìåííàÿ ñîñòîÿíèÿ äëÿ r�}
2. A r Rr I h* � ���{� | ( ) — ðåãèñòð ñîñòîÿíèÿ b BRI h� ( ) è path( , )A b � � è
� r I h
o A� � * ( )
( )
ÿâëÿåòñÿ ïåðåìåííîé ñîñòîÿíèÿ äëÿ r�}
3. ro {) � � � � �w b I h d I h| ( ), ( ); path }( , ) ,( , ) ( , )b A w b d� � ��
4. ro {* � � � � �w b I h d I h| ( ), ( ); path }( , ) ,( , ) ( , )A b w b d� � ��
5. Îïðåäåëèòü p a ac
a A a A a ro
� �+
,
-
.
/
0 �+
,
-
.
/
0 � $+
,
-
.
/
0� ) � * � )
& & & && & &2 1 �
a ro� *
� $+
,
-
.
/
0�
6. Îïðåäåëèòü p a a
a A a A ro
0 1 0� �+
,
-
.
/
0 �+
,
-
.
/
0 � $
+
,
-
.
/
0
� ) � * � )
& & & && & &
�
�
�
�
� *
� $+
,
-
.
/
0
ro
7. Âîçâðàòèòü pc è p0.
Âëèÿíèå íà óñëîâèÿ êîððåêòíîñòè: Íåò.
Ïðîöåäóðà 4: construct_TransitionAndDataCon
Âõîä:
• Öèêëè÷åñêèé BPT P1 ñ ãðàôîì G N E1 1 1( , ) (äî çàìåíû èíòåðâàëà)
• Öèêëè÷åñêèé BPT P2 ñ ãðàôîì G N E2 2 2( , ) (ïîñëå çàìåíû èíòåðâàëà)
• I h( ) — èíòåðâàë
• BRI h( ) — ìíîæåñòâî âåòâÿùèõñÿ îïåðàòîðîâ
• RI h( ) — ìíîæåñòâî ðåãèñòðîâ ñîñòîÿíèé äëÿ èíòåðâàëà
Âûõîä: Öèêëè÷åñêèé BPT P2 ñ ãðàôîì G N E2 2 2( , )
Ìåòîä:
1. P P A2 1� ��; out
2. Äëÿ âñåõ a I h b N I h e a b p E� � �� ��( ), \ ( ), , ,1 1 âûïîëíèòü
• E E e2 2� \ { }
• E E eI h I h( )
*
( )
* {� � }
3. Äëÿ âñåõ A BR e EI h I h� �( ) ( )
*, âûïîëíèòü
• { } construct_ BranchActCondp p P A BR Rc
I h I h, ( , , ,( ) ( ))
0
1�
• Îïðåäåëèòü � � � � �e I ho A*
( ){ | ( ) ( ), * ( ))� � � � �Dom Dom
• Îïðåäåëèòü p e p pc� � ��3
0( )& ( ) òàê ÷òîáû i p i e e( ) ( ( )) *� � �� �3
• Åñëè �2 ( )e A� out , òî A A e P peout out { }� � � �� �2 2( ) ; ( )
èíà÷å P P pe e� �2 2( ) ( )� � �
• C C e2 2 3� \ ( ){ }�
72 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 2
4. Äëÿ âñåõ a A� out âûïîëíèòü
• C C Pa2 2� �} }; E E A a P A PI h a I h a2 2 2� � � � ��{ }( ) ( ), , ; ( , )
• Îïðåäåëèòü
2 1( , ) ( , )| ( , ) ( , ), , , ,( ) ( )A P w w A p e b a p EI h a I h� � �� ��{ � �
b I h w w o AI h e� � � �( ) ( , )| * ( )&( )
*} { }� � �
5. Âîçâðàòèòü P2.
Âëèÿíèå íà óñëîâèÿ êîððåêòíîñòè: Íåò.
Íèæå ïðèâåäåí àëãîðèòì ïðåîáðàçîâàíèÿ öèêëè÷åñêîãî BPT â àöèêëè÷åñêèé.
Àëãîðèòì T. Ïðåîáðàçîâàíèå öèêëè÷åñêîãî øàáëîíà áèçíåñ-ïðîöåññà
Âõîä:
• Öèêëè÷åñêèé BPT P T N C E i o ME C�� �, , , , , , , , , ,� �
• Ìíîæåñòâî çíà÷åíèé Ì E ñóùåñòâåííûõ âûõîäíûõ ïåðåìåííûõ
Âûõîä:
• Àöèêëè÷åñêèé BPT P T N C E i o MW �� � � � � � � � � � ��, , , , , , , , ,�
• Ìíîæåñòâî çíà÷åíèé ÌW ñóùåñòâåííûõ âûõîäíûõ ïåðåìåííûõ
Ìåòîä:
1. N N C C E E M M C C P P M ME E�� �� �� �� �� �� � �; ; ; ; ; ; ;� � 1 1
2. S
Ñ
� construct_IntervalSet (PE ) .
3. Äëÿ âñåõ I h SC( )� âûïîëíèòü
a) ïîñòðîèòü ìíîæåñòâî âåòâÿùèõñÿ îïåðàòîðîâ:
BR a I h b I h d I h a b t E a d tI h( ) ( )| ( ), ( ), , , , , ,� � � � � � � �� � �{ 1 2 �E}.
b) ïîñòðîèòü ìíîæåñòâî ðåãèñòðîâ ñîñòîÿíèé:
R r rI h a a( ) |� { ÿâëÿåòñÿ ðåãèñòðîì ñîñòîÿíèÿ a BRI h� ( )}
c) � ��P M P M I h RI h2 2 1 1, ( , , ( ), ( ))remove_ Interval
d) P P P I h BRI h1 1 2� construct_ TransitionAndDataCon( , , ( ), ( ) ( )), RI h
4. Âîçâðàòèòü P1 è M2.
Èìååò ìåñòî ñëåäóþùåå óòâåðæäåíèå.
Ëåììà 5. Ïóñòü P AT� — öèêëè÷åñêèé BPT. Òîãäà Q T P� ( ) — àöèêëè÷åñ-
êèé BPT, òàê ÷òî èìååò ìåñòî ñëåäóþùåå óòâåðæåäåíèå:
[ ( )T P êîððåêòåí/íåêîððåêòåí � P êîððåêòåí/íåêîððåêòíåí.]
Äîêàçàòåëüñòâî. Ïóñòü P — öèêëè÷åñêèé BPT. Ïóñòü � �, — ñîîòâåòñòâåííî
ïðåä- è ïîñòóñëîâèÿ äëÿ P M, — ìíîæåñòâî ñóùåñòâåííûõ âûõîäíûõ ïåðå-
ìåííûõ P. Òîãäà P êîððåêòåí îòíîñèòåëüíî � è �, åñëè [ ( ) ( ) ]� �M MP� � �1 1 .
Ïðåäïîëîæèì, ÷òî ïðèìåíåí àëãîðèòì ïðåîáðàçîâàíèÿ öèêëè÷åñêîãî P
â àöèêëè÷åñêèé BPT Q. Ïîñêîëüêó àëãîðèòì íå ìåíÿåò ñåìàíòèêè ïðîöåññà
ñ òî÷êè çðåíèÿ ôîðìàëüíîé âåðèôèêàöèè, òî ïðîöåññ Q ýêâèâàëåíòåí ïðîöåññó P
ñ òî÷êè çðåíèÿ âåðèôèêàöèè. Ïóñòü � �1 1, — ñîîòâåòñòâåííî ïðåä- è ïîñòóñëî-
âèÿ äëÿ Q, à MQ — ìíîæåñòâî ñóùåñòâåííûõ âûõîäíûõ ïåðåìåííûõ Q. Ïðåä-
óñëîâèå ( )�1 è ïîñòóñëîâèå ( )�1 ïðîöåññà Q ëîãè÷åñêè ýêâèâàëåíòíû � è � ñîîò-
âåòñòâåííî, òàê ÷òî � � � �( ) ( ) ( )) ( ) .M M M Q MPQ Q� � � � � � �1 1 1 11 1
Óòâåðæäåíèå äîêàçàíî.
Ýòî óòâåðæäåíèå äîêàçûâàåò, ÷òî äëÿ êàæäîãî öèêëè÷åñêîãî BPT ñóùåñòâó-
åò àöèêëè÷åñêèé BPT, ýêâèâàëåíòíûé íà÷àëüíîìó ñ òî÷êè çðåíèÿ ôîðìàëüíîé
âåðèôèêàöèè.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 2 73
5. ÔÎÐÌÀËÜÍÀß ÂÅÐÈÔÈÊÀÖÈß AÖÈÊËÈ×ÅÑÊÎÃÎ ØÀÁËÎÍÀ ÁÈÇÍÅÑ-ÏÐÎÖÅÑÑÀ
Íèæå ââåäåíî ïîíÿòèå òðàôàðåòà äëÿ BPTs (ïðèìèòèâû äëÿ îïèñàíèÿ ïîäìíî-
æåñòâ ñîñòîÿíèé ñðåäû) [10, 11].
Ðàçäåëåííîå ìíîæåñòâî — ýòî êîðòåæ, êîìïîíåíòû êîòîðîãî ÿâëÿþòñÿ ïîä-
ìíîæåñòâàìè ñîîòâåòñòâóþùèõ îáëàñòåé ïåðåìåííûõ. Ðàçäåëåííûé òðàôàðåò —
ýòî ïàðà äâóõ ðàçäåëåííûõ ìíîæåñòâ. Îäíî èç íèõ àïïðîêñèìèðóåò ìíîæåñòâî
òåêóùèõ ñîñòîÿíèé ïðîöåññà ñíèçó, â òî âðåìÿ êàê äðóãîå àïïðîêñèìèðóåò
ñâåðõó. Îáîçíà÷èì Ì ìíîæåñòâà âñåõ òðàôàðåòîâ.
Äëÿ ôîðìàëüíîé âåðèôèêàöèè àöèêëè÷åñêèõ øàáëîíîâ ïðåäëîæåí àëãîðèòì
âåðèôèêàöèè A-ïðîöåññîâ [10].
Èìååò ìåñòî ñëåäóþùåå óòâåðæäåíèå î êîððåêòíîñòè BPT îòíîñèòåëüíî � è �,
îñíîâàííîå íà ñðàâíåíèè ðàçäåëåííûõ ìíîæåñòâ.
Ëåììà 6. Ïóñòü P — ÂÐÒ, � — ïðåäóñëîâèå è � — ïîñòóñëîâèå, îïðåäåëåí-
íûå äëÿ P. Òîãäà èìåþò ìåñòî ñëåäóþùèå óòâåðæäåíèÿ:
a) åñëè � � �2 1( ) ( ( ))finalMold mold� , òî P êîððåêòåí îòíîñèòåëüíî � è �;
á) åñëè& �( ( ) ( ( ))� � �� finalMold mold2 , òî P íå êîððåêòåí îòíîñèòåëüíî � è �;
â) èíà÷å óòâåðæäåíèå î êîððåêòíîñòè P îòíîñèòåëüíî � è � íå îïðåäåëåíî.
Àëãîðèòì ôîðìàëüíîé âåðèôèêàöèè àöèêëè÷åñêèõ áèçíåñ-ïðîöåññîâ (äà-
ëåå — Àëãîðèòì AV) è äîêàçàòåëüñòâî ëåììû 6 äåòàëüíî ïðåäñòàâëåíû â [10].
5.1. Ôîðìàëüíàÿ âåðèôèêàöèÿ ïðèìèòèâîâ. Óòâåðæäåíèå 1. Ïóñòü u —
ïðîñòîé ïðèìèòèâ, �( )u — ïðåäóñëîâèå èíèöèàëèçàöèè è �( )u — ïîñòóñëîâèå
âûïîëíåíèÿ äëÿ u. Òîãäà àëãîðèòì AV äàåò îïðåäåëåííûé îòâåò (êîððåêòåí/íå-
êîððåêòåí) î êîððåêòíîñòè u îòíîñèòåëüíî �( )u è �( ).u
Äîêàçàòåëüñòâî. Ïóñòü u — ïðîñòîé ïðèìèòèâ. Òîãäà
In Out { }( ) ( ) ( ) .u u Act u a� � �
Pre AND...AND� � $ � $( ( ) ( ) )in ink1 11 1
Post TRUE� �( ( ) )mb a1
Òðàôàðåò îïðåäåëÿåòñÿ ìåòîäîì äîáàëåíèÿ ñîîòâåñòâåííûõ âõîäíûõ ïåðå-
ìåííûõ a1 è mb a in in mb ak( ) ( ), , ( ), ( )1 1 1 11 1�� �� � �mold . Ïîñëå âû÷èñëåíèÿ
òðàôàðåòîâ äëÿ ïðåä- è ïîñòóñëîâèé èìååì:
mold(Pre) = = <<‘Known’ , … , ‘Known’, $> , <‘Known’ , … , ‘Known’, $ >>;
mold(Post) = = <<{‘Known’, $} , … , {‘Known’, $} , TRUE>, <{‘Known’, $}, ...
… , {‘Known’, $} , TRUE>> .
Ïîñëå âûïîëíåíèÿ ïðîöåññà ïîëó÷èì òðàôàðåò finalMold = <<‘Known’, …
... , ‘Known’, TRUE>, <‘Known’, … , ‘Known’, TRUE>>. Óñëîâèå ( ( )�2 finalMold �
� � �1( )))mold( óäîâëåòâîðåíî äëÿ ïðîöåññà, ïîñêîëüêó <‘Known’,... … , ‘Known’,
TRUE > � < {‘Known’, $} , … , {‘Known’, $} , TRUE > . Ýòî îçíà÷àåò, ÷òî ïðî-
öåññ êîððåêòåí (ëåììà 6).
Óòâåðæäåíèå äîêàçàíî.
Óòâåðæäåíèå 2. Ïóñòü u — ïðèìèòèâ ñèíõðîíèçàöèè, �( )u — ïðåäóñëîâèå
èíèöèàëèçàöèè è �( )u — ïîñòóñëîâèå âûïîëíåíèÿ äëÿ u. Òîãäà àëãîðèòì AV
äàåò îïðåäåëåííûé îòâåò (êîððåêòåí/íåêîððåêòåí) î êîððåêòíîñòè u îòíîñè-
òåëüíî �( )u è �( ).u
Óòâåðæäåíèå 3. Ïóñòü u — ïðèìèòèâ ðàçäåëåíèÿ, �( )u — ïðåäóñëîâèå èíèöè-
àëèçàöèè è �( )u — ïîñòóñëîâèå âûïîëíåíèÿ äëÿ u. Òîãäà àëãîðèòì AV äàåò îïðåäå-
ëåííûé îòâåò (êîððåêòåí/íåêîððåêòåí) î êîððåêòíîñòè u îòíîñèòåëüíî �( )u è �( ).u
Ëåììà 7. Ïóñòü u — ïðèìèòèâ ëþáîãî òèïà, �( )u — ïðåäóñëîâèå èíèöèàëèçà-
öèè è �( )u — ïîñòóñëîâèå âûïîëíåíèÿ äëÿ u. Òîãäà àëãîðèòì AV äàåò îïðåäåëåí-
íûé îòâåò (êîððåêòåí/íåêîððåêòåí) î êîððåêòíîñòè u îòíîñèòåëüíî �( )u è �( ).u
Äîêàçàòåëüñòâî ëåììû 7 íåïîñðåäñòâåííî ñëåäóåò èç óòâåðæäåíèé 1–3.
Îáîçíà÷èì BasicUnitV N Eu u( , ) ïðîöåäóðó ïðîâåðêè êîððåêòíîñòè ïðèìèòè-
âà u ñ ãðàôîì G N Eu u( , ).
74 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 2
5.2. Ôîðìàëüíàÿ âåðèôèêàöèÿ äëÿ îïåðàöèé êîíêàòåíàöèè è ñëèÿíèÿ. Ëåì-
ìà 8. Ïóñòü P1 è P2 — òàêèå àöèêëè÷åñêèå øàáëîíû ïðîöåññîâ, ÷òî In { }( ) ,P ip1 1�
Out { } In { } Out {( ) , , , ( ) , ( ) , ,P op op P ip P opk1 1 1 2 1 1
� � � � � � � op k k
k
� �
2
1 2 0}, , .
Åñëè P1 êîððåêòåí îòíîñèòåëüíî �( )P1 è �( )P1 , à P2 êîððåêòåí îòíîñèòåëüíî
�( )P2 è �( )P2 , òî BPT P P P k c� �Concat( , , , )1 2 òàêæå êîððåêòåí îòíîñèòåëüíî
ïðåäóñëîâèÿ � � �( ) ( )& ( )&P P P c� � 1 2 è ïîñòóñëîâèÿ � � �( ) ( )& ( ).P P P� � 1 2 Åñëè
P1 íå êîððåêòåí îòíîñèòåëüíî �( )P1 è �( )P1 èëè P2 íå êîððåêòåí îòíîñèòåëüíî
�( )P2 è �( )P2 , òî P� òàêæå íå êîððåêòåí îòíîñèòåëüíî �( )P� è �( ).P�
Äîêàçàòåëüñòâî. P1 è P2 — òàêèå àöèêëè÷åñêèå øàáëîíû, ÷òî In }( ) { ,P ip1 1�
Out } In } Out( ) { , , , ( ) { , ( ) { , ,P op op P ip P opk1 1 1 2 1 1� � � � � � � op k kk
� �2 1 2 0}, , .
Òîãäà P P P k c P Pc k� � � "Concat( , , , ) ,1 2 1 2 — àöèêëè÷åñêèé BPT. Ïóñòü óñëî-
âèå � � �( ) ( )& ( )&P P P c� � 1 2 óäîâëåòâîðÿåòñÿ äî âûïîëíåíèÿ P �. Òîãäà �( )P1 òàê-
æå óäîâëåòâîðÿåòñÿ. Â ðåçóëüòàòå P1 êîððåêòåí îòíîñèòåëüíî �( )P1 è �( ).P1 Åñëè
P íåêîððåêòåí, òî �( )P1 íå óäîâëåòâîðÿåòñÿ. Òîãäà �( )P� òàêæå íå óäîâëåòâîðÿ-
åòñÿ è ñîîòâåòñòâåííî P� íå êîððåêòåí îòíîñèòåëüíî �( )P� è �( )P� . Åñëè P1 íå-
êîððåêòåí è c, �( )P2 óäîâëåòâîðÿþòñÿ âñëåäñòâèå òîãî, ÷òî óäîâëåòâîðÿåòñÿ
�( )P� , òî P2 àêòèâèçèðóåòñÿ. Åñëè P
2
íåêîððåêòåí, òî �( )P2 íå óäîâëåòâîðÿåòñÿ.
 ýòîì ñëó÷àå �( )P � òàêæå íå óäîâëåòâîðÿåòñÿ è ñîîòâåòñòâåííî P � íå êîððåêòåí
îòíîñèòåëüíî �( )P � è �( )P� . Åñëè P2 êîððåêòåí, òî �( )P
2
óäîâëåòâîðÿåòñÿ. Â ðå-
çóëüòàòå âåðíî ñëåäóþùåå: � � �( ) ( )& ( ).P P P� � 1 2
Óòâåðæäåíèå äîêàçàíî.
Ëåììà 9. Ïóñòü u — ïðèìèòèâ ñèíõðîíèçàöèè è P — àöèêëè÷åñêèé øàáëîí òàêèå, ÷òî
In { } Out { } Out { }( ) , ( ) , , , , ( ) ,P ip P op op ko u ouko� � � � �
1 1 10 In { }( ) , ,u iu iu m� �1 .
Åñëè u êîððåêòåí îòíîñèòåëüíî �( )u è �( )u , à òàêæå P êîððåêòåí îòíîñèòåëüíî
�( )P è �( )P , òî P u P k c� � Merge( , , , ) êîððåêòåí îòíîñèòåëüíî ïðåäóñëîâèÿ
� �( ) ( )&P u� � & ( )& & &� P c cm1 � è ïîñòóñëîâèÿ � � �( ) ( )& ( )P u P� � , åñëè
c c cm�� � �1, , . Åñëè u íå êîððåêòåí îòíîñèòåëüíî �( )u è �( )u èëè P íå êîððåêòåí
îòíîñèòåëüíî �( )P è �( )P , òî P� òàêæå íå êîððåêòåí îòíîñèòåëüíî �( )P� è �( ).P�
Äîêàçàòåëüñòâî àíàëîãè÷íî ïðåäûäóùåìó äîêàçàòåëüñòâó.
6. ÀËÃÎÐÈÒÌ ÔÎÐÌÀËÜÍÎÉ ÂÅÐÈÔÈÊÀÖÈÈ ÄËß ØÀÁËÎÍÎÂ ÁÈÇÍÅÑ-ÏÐÎÖÅÑÑÎÂ
Íèæå ïðåäñòàâëåí àëãîðèòì ôîðìàëüíûé âåðèôèêàöèè äëÿ øàáëîíîâ îòíîñè-
òåëüíî ïðåäóñëîâèÿ èíèöèàëèçàöèè è ïîñòóñëîâèÿ âûïîëíåíèÿ.
Àëãîðèòì V. Ôîðìàëüíàÿ âåðèôèêàöèÿ BPT.
Âõîä: BPT P ñ ãðàôîì G N E( , )
Âûõîä: Êîððåêòåí/Íåêîððåêòåí
Ìåòîä:
1. Åñëè N ���, òî âîçâðàòèòü Êîððåêòåí
2. Åñëè P èìååò öèêë, òî P T P� ( )
3. Äëÿ âñåõ A N� âûïîëíèòü
• counter(A) � �| | .A
• åñëè counter( ) = 0A , òî äîáàâèòü A ê Front-ó
4. bUnit � � �0, ,N N E Ep p
5. Ïîêà !bUnit âûïîëíèòü
5.1. âûáðàòü A èç Front-a, N A E N N Au u p p� �� �{ } } }, , /
5.2. Åñëè | | ,A� � 1 òî
a) bUnit �1
b) Äëÿ âñåõ e A e A A p� � �� , ( , , ) âûïîëíèòü
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 2 75
N N A N N A E E e E E eu u p p u u p p� � � � � � � �{ } { } { } }, / , , / {
5.3. Èíà÷å åñëè A A A A p� �� � � � �| , { , ,1 }, òî
a) Åñëè | |A� �� 1, òî bUnit �1
b) Èíà÷å åñëè A� �� Front, òî
c) N Au � � �{ } bUnit, 1
d) Äëÿ âñåõ e A e A A p� � � � � �� , ( , , ) âûïîëíèòü
N N A N N A E E e E E eu u p p u u p p� � �� � �� � � �{ } { } { } { }, / , , /
e) Èíà÷å óäàëèòü A èç Front-a
6. Åñëè BasicUnitV N E V N Eu u p p( , )& ( , ), òî âîçâðàòèòü Êîððåêòåí èíà÷å
âîçâðàòèòü Íåêîððåêòåí.
Òåîðåìà 2. Ïóñòü P — øàáëîí áèçíåñ-ïðîöåññà, � è � — ñîîòâåòñòåííî
ïðåäóñëîâèå èíèöèàëèçàöèè è ïîñòóñëîâèå âûïîëíåíèÿ äëÿ P. Òîãäà àëãîðèòì
âåðèôèêàöèè (àëãîðèòì V) äàåò îïðåäåëåííûé îòâåò (êîððåêòåí/íåêîððåêòåí)
î êîððåêòíîñòè P îòíîñèòåëüíî � è �.
Äîêàçàòåëüñòâî òåîðåìû 2 — ïðÿìîå ñëåäñòâèå ëåìì 7–9. Òàêèì îáðàçîì, äîêàçàíî,
÷òî ïðîáëåìà ôîðìàëüíîé âåðèôèêàöèè ðàçðåøèìà äëÿ øàáëîíîâ áèçíåñ-ïðîöåññîâ.
7. ÏÐÅÄÑÒÀÂËÅÍÈÅ ITIL Ñ ÏÎÌÎÙÜÞ ØÀÁËÎÍÎÂ ÁÈÇÍÅÑ-ÏÐÎÖÅÑÑÎÂ
Ïðåäëîæåííûå â ðàáîòå øàáëîíû áèçíåñ-ïðîöåññîâ èñïîëüçóþòñÿ äëÿ îïèñà-
íèÿ áèáëèîòåêè IT Infrastructure Library (ITIL) — áèáëèîòåêè èíôðàñòðóêòóðû
èíôîðìàöèîííûõ òåõíîëîãèé (www.itil-officialsite.com), ñîäåðæàùåé ìíîæåñòâî
øàáëîíîâ ïðîöåññîâ äëÿ óïðàâëåíèÿ IT óñëóãàìè [3–6]. Áèáëèîòåêà ïîñòðîåíà
íà îñíîâå ñîâðåìåííûõ ìåòîäîâ óïðàâëåíèÿ è ñëóæèò â êà÷åñòâå äå-ôàêòî
ñòàíäàðòíîãî ðóêîâîäñòâà äëÿ ñîçäàíèÿ ïðîöåññîâ IT óïðàâëåíèÿ [5].
IBM, HP è Microsoft ïîñòàâëÿþò ñîáñòâåííûå áèáëèîòåêè ïðîöåññîâ äëÿ
óïðàâëåíèÿ IT (IBM PRM-IT 2007; HP ITSM 2003; 2008 MOF). Àíàëèç ýòèõ áèá-
ëèîòåê ïîêàçàë, ÷òî âñå ñîäåðæàùèåñÿ â íèõ øàáëîíû áèçíåñ-ïðîöåññîâ ïîñòðîå-
íû èç ïðèìèòèâîâ, ïðåäëîæåííûõ â íàñòîÿùåé ðàáîòå, ñ èñïîëüçîâàíèåì îïåðà-
öèé êîíêàòåíàöèè, ñëèÿíèÿ è öèêëà. Òàêèì îáðàçîì, îïèñàííûé ïîäõîä, ïîìèìî
âåðèôèêàöèè áèáëèîòåêè ITIL, ïîçâîëÿåò ðåøèòü ïðîáëåìó ôîðìàëüíîé âåðèôè-
êàöèè è äëÿ áèáëèîòåê PRM-IT, ITSM, MOF.
Àâòîð âûðàæàåò áëàãîäàðíîñòü àêàäåìèêó ÍÀÍ Àðìåíèè, äîêòîðó ôèçè-
êî-ìàòåìàòè÷åñêèõ íàóê, ïðîôåññîðó Ñ.Ê. Øóêóðÿíó.
ÑÏÈÑÎÊ ËÈÒÅÐÀÒÓÐÛ
1. T h e i n f r a s t r u c t u r e optimization journey. — Microsoft Corporation, 2008.
2. A i l e e n C . , W u i - G e e T . , M a r k T . Summary of ITIL Adoption Survey Responses. Techn. Rep.,
itSMF Australia Conf., Toowoomba, Australia. — 2006.
3. IT Infrastructure Library, IT Service Management. — http://www.itil.co.uk/.
4. I n t r o d u c i n g the IBM process reference model for IT, Second Edition, IBM, January 2007.
5. T u r n e r M . S . Microsoft solutions framework essentials. — Microsoft Press, 2006.
6. P u l t o r a k D . Microsoft operations framework (MOF): A pocket guide. — Amsterdam: Van Haren
Publ., 2005.
7. L e y m a n n F . , R o l l e r D . Production workflow: Concepts and techniques. — New York: Prentice Hall
Press, 2000.
8. A l l e n F . E . , C o c k e J . A program dataflow analysis procedure // Com. of the ACM. — 1976. —
19(3). — Ð. 137–147.
9. H e c h t M . S . , U l l m a n J . D . Characterizations of reducible flow graphs // J. ACM — 1974. — 21,
N 3. — P. 367–375. DOI= http://doi.acm.org/10.1145/321832.321835.
10. K o s t a n y a n A . , V a r o s y a n A . Partial recognizing algorithm for verification of workflow processes
// FUBUTEC’2008. — 2008. — P. 89–94.
11. S h o u k o u r i a n S . , K o s t a n i a n A . , M a r g a r i a n V . , A s h o u r A . An approach for system
tests design and its applications // Proc. of the 13-th IEEE VLSI Test Symposium, NJ, Princeton, USA. —
1995. — P. 448–453.
Ïîñòóïèëà 14.07.2010
76 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 2
|