協(xié)同業(yè)務(wù)過(guò)程的建模及正確性修正?

莫 啟,代 飛,笪 建,朱 銳,謝仲文,李 彤

1(云南大學(xué) 軟件學(xué)院,云南 昆明 650091)

2(云南省軟件工程重點(diǎn)實(shí)驗(yàn)室(云南大學(xué)),云南 昆明 650091)

3(西南林業(yè)大學(xué) 大數(shù)據(jù)與智能工程學(xué)院,云南 昆明 650091)

4(淮安開(kāi)放大學(xué) 信息工程系,江蘇 淮安 223001)

隨著全球經(jīng)濟(jì)化的發(fā)展和企業(yè)信息化程度的不斷提高,企業(yè)的經(jīng)營(yíng)模式發(fā)生了重大的變化,企業(yè)的業(yè)務(wù)活動(dòng)已從企業(yè)內(nèi)單目標(biāo)為導(dǎo)向的獨(dú)立發(fā)展模式發(fā)展成為跨企業(yè)多目標(biāo)合作的協(xié)同模式[1].在現(xiàn)代商業(yè)環(huán)境下,沒(méi)有一個(gè)企業(yè)是孤立的[2,3].企業(yè)作為參與者參與到協(xié)作中,在協(xié)作過(guò)程中,它們彼此進(jìn)行交互以完成特定業(yè)務(wù)功能.近年來(lái),隨著Internet 成為主流的計(jì)算平臺(tái),尤其是面向服務(wù)計(jì)算(service-oriented computing,簡(jiǎn)稱SOC)的快速興起,使得不同組織業(yè)務(wù)過(guò)程間的交互成為可能,如企業(yè)信息系統(tǒng)[4]、電子商務(wù)[5]等.為實(shí)現(xiàn)共同的商業(yè)目標(biāo),每個(gè)組織的業(yè)務(wù)過(guò)程通常需要跨越組織邊界,與其他組織的業(yè)務(wù)過(guò)程進(jìn)行交互和協(xié)作以形成相對(duì)穩(wěn)定的過(guò)程視圖.學(xué)術(shù)界和工業(yè)界稱這種存在復(fù)雜交互關(guān)系的業(yè)務(wù)過(guò)程為協(xié)同業(yè)務(wù)過(guò)程[6].

針對(duì)協(xié)同業(yè)務(wù)過(guò)程,國(guó)內(nèi)外研究者提出多種建模方法.歸納起來(lái),這些建模方法可分為兩類:(1)自頂向下建模方法[7,8].該方法要求首先給出協(xié)同全局契約,然后定義映射規(guī)則并以此為基礎(chǔ)從契約中生成每個(gè)組織的業(yè)務(wù)過(guò)程;(2)自底向上建模方法[9].該方法允許組織獨(dú)立地定義各自的業(yè)務(wù)過(guò)程,之后以此為基礎(chǔ)直接構(gòu)建具有協(xié)同功效的協(xié)同業(yè)務(wù)過(guò)程.由于受限于映射規(guī)則集,利用自頂向下建模方法通常僅能建立具有有限結(jié)構(gòu)形態(tài)業(yè)務(wù)過(guò)程,靈活性和普適性不足[7,8].因此,本文關(guān)注自底向上建模方法.

然而,自底向上建模方法中的業(yè)務(wù)過(guò)程由不同組織開(kāi)發(fā),無(wú)法在設(shè)計(jì)階段就預(yù)見(jiàn)其潛在的所有交互可能,因此在實(shí)際協(xié)作中,參與協(xié)作的業(yè)務(wù)過(guò)程間可能存在不一致(如死鎖等),無(wú)法保證協(xié)同業(yè)務(wù)過(guò)程正確地實(shí)施.因此,對(duì)協(xié)同業(yè)務(wù)過(guò)程的正確性(正確性可根據(jù)實(shí)際需要定義,如合理性等,在此不作區(qū)分)進(jìn)行分析是當(dāng)前業(yè)務(wù)過(guò)程管理(business process management,簡(jiǎn)稱BPM)領(lǐng)域內(nèi)的研究熱點(diǎn).

針對(duì)協(xié)同業(yè)務(wù)過(guò)程正確性分析,國(guó)內(nèi)外學(xué)者做了大量工作[9,10].這些研究工作主要圍繞正確性檢測(cè)方法開(kāi)展.該方法先構(gòu)建形式化的協(xié)同業(yè)務(wù)過(guò)程并定義正確性約束(如無(wú)死鎖、無(wú)活鎖及未指定接收等),然后采用某種形式的驗(yàn)證技術(shù)(如模型檢測(cè)等)在協(xié)同業(yè)務(wù)過(guò)程中檢測(cè)相容性是否滿足.正確性檢測(cè)方法通常具有檢測(cè)過(guò)程自動(dòng)化,不需要人工干預(yù),且在檢測(cè)失敗時(shí)能夠給出診斷信息,便于業(yè)務(wù)設(shè)計(jì)人員發(fā)現(xiàn)并修正錯(cuò)誤.但其不足是,若協(xié)同業(yè)務(wù)過(guò)程中存在多處不正確,則需要經(jīng)過(guò)多次檢測(cè),且在每次檢測(cè)后都需要對(duì)協(xié)同業(yè)務(wù)過(guò)程重新調(diào)整.重復(fù)地進(jìn)行檢測(cè)及調(diào)整使得協(xié)同業(yè)務(wù)過(guò)程正確性分析復(fù)雜且耗時(shí).

一種替代方法是正確性修正方法.該方法關(guān)注早期設(shè)計(jì)階段,根據(jù)正確性約束對(duì)業(yè)務(wù)過(guò)程內(nèi)部結(jié)構(gòu)進(jìn)行修改以自動(dòng)構(gòu)建滿足正確性約束的業(yè)務(wù)過(guò)程[11,12].這方面的研究工作較少,且大多關(guān)注組織內(nèi)單個(gè)業(yè)務(wù)過(guò)程,能夠用于協(xié)同業(yè)務(wù)過(guò)程正確性修正方法[13-15]也存在如下不足:(1)修正后的協(xié)同業(yè)務(wù)過(guò)程是集中式的,與協(xié)同業(yè)務(wù)過(guò)程的實(shí)際特征(如自治、分布及面向流程協(xié)作等)[16]不符;(2)這些方法基于過(guò)程挖掘技術(shù)[17]而提出,不能夠保證修正協(xié)同業(yè)務(wù)過(guò)程中含有修正前協(xié)同業(yè)務(wù)過(guò)程中的所有完整軌跡(即完整的簡(jiǎn)單路徑對(duì)應(yīng)活動(dòng)執(zhí)行序列),還可能引入隱藏軌跡(即不屬于修正前協(xié)同業(yè)務(wù)過(guò)程中的其他軌跡),這需要進(jìn)行額外確認(rèn);(3)協(xié)同業(yè)務(wù)過(guò)程實(shí)質(zhì)上是由多個(gè)業(yè)務(wù)過(guò)程構(gòu)成的并發(fā)交互系統(tǒng),復(fù)雜程度高[16].直接利用這些方法對(duì)其進(jìn)行修正存在修正效率低下的問(wèn)題.例如,我們課題組最近的工作[13]即結(jié)合Petri 網(wǎng)和過(guò)程挖掘的相關(guān)理論,提出了一種針對(duì)協(xié)同業(yè)務(wù)過(guò)程修正方法.但是,該方法構(gòu)建的協(xié)同業(yè)務(wù)過(guò)程存在中心流程(即只能通過(guò)該中心流程協(xié)調(diào)原有業(yè)務(wù)過(guò)程執(zhí)行).同時(shí),修正協(xié)同業(yè)務(wù)過(guò)程與修正前協(xié)同業(yè)務(wù)過(guò)程中含有的所有完整軌跡也可能不一致,且存在執(zhí)行失敗的情況.這在后文的實(shí)驗(yàn)部分將給出詳細(xì)闡述.

針對(duì)上述問(wèn)題,本文采用標(biāo)號(hào)遷移系統(tǒng)LTS(labeled transition system)來(lái)描述業(yè)務(wù)過(guò)程,并將其并發(fā)組合建模協(xié)同業(yè)務(wù)過(guò)程.在考慮活動(dòng)同步及異步交互的情況下,通過(guò)將協(xié)同業(yè)務(wù)過(guò)程的行為抽象為簡(jiǎn)單路徑,在此基礎(chǔ)上,提出了針對(duì)部分正確的協(xié)同業(yè)務(wù)過(guò)程修正方法.該修正方法能夠確保修正協(xié)同業(yè)務(wù)過(guò)程與修正前的協(xié)同業(yè)務(wù)過(guò)程中含有的軌跡相一致,且修正協(xié)同業(yè)務(wù)過(guò)程具有自治、分布及面向流程組合等特性.

本文主要貢獻(xiàn)如下:

(1)在考慮活動(dòng)同步及異步交互的情況下,提出了簡(jiǎn)單路徑用來(lái)刻畫(huà)協(xié)同業(yè)務(wù)過(guò)程的行為,并提出將完整的簡(jiǎn)單路徑合并為核的算法.本質(zhì)上,核中包含了修正前的協(xié)同業(yè)務(wù)過(guò)程中所有正確的任務(wù)執(zhí)行系列(即完整軌跡).以核為基礎(chǔ),提出了將其映射為修正業(yè)務(wù)過(guò)程的方法,將所有的修正業(yè)務(wù)過(guò)程并發(fā)組合建立修正的協(xié)同業(yè)務(wù)過(guò)程;

(2)理論上證明了修正協(xié)同業(yè)務(wù)過(guò)程與修正前協(xié)同業(yè)務(wù)過(guò)程中含有的軌跡是一致的,從而避免了額外確認(rèn),降低了修正代價(jià);

(3)通過(guò)實(shí)驗(yàn)分析得出:相對(duì)已有方法,在考慮協(xié)同業(yè)務(wù)過(guò)程實(shí)際特征(如自治、分布及面向流程組合等)的情況下,本文方法可實(shí)現(xiàn)更加有效的正確性修正并能夠極大地提高修正效率,縮短修正時(shí)間.

本文第1 節(jié)給出方法概覽.第2 節(jié)給出協(xié)同業(yè)務(wù)過(guò)程定義.第3 節(jié)對(duì)正確性進(jìn)行分析.第4 節(jié)對(duì)正確性修正方法進(jìn)行討論.第5 節(jié)通過(guò)實(shí)驗(yàn)對(duì)本文方法的有效性及效率進(jìn)行評(píng)估.第6 節(jié)為相關(guān)工作.第7 節(jié)為全文總結(jié).

1 方法概述

本文正確性修正方法提出是建立在如下一種事實(shí),即采用自底向上建模方法在建立協(xié)同業(yè)務(wù)過(guò)程中無(wú)法預(yù)見(jiàn)其所有潛在的交互可能,從而導(dǎo)致建立模型中可能存在異常(如死鎖等),這將嚴(yán)重地阻礙業(yè)務(wù)過(guò)程間的正確協(xié)作.本文提出的正確性修正方法框架如圖1 所示.

Fig.1 Overview of correctness repair圖1 正確性修正方法概覽

具體地,該正確性修正方法由如下兩個(gè)階段組成.

(1)建模階段.參與組織首先獨(dú)立地采用LTS 建模各自業(yè)務(wù)過(guò)程,并將這些業(yè)務(wù)過(guò)程并發(fā)組合建立協(xié)同業(yè)務(wù)過(guò)程;之后參與組織間經(jīng)協(xié)商,確定期望的系統(tǒng)正確性,本文以弱合理[11]定義;

(2)分析階段.分析階段將協(xié)同業(yè)務(wù)過(guò)程和正確性約束輸入,自動(dòng)構(gòu)建具有正確性的協(xié)同業(yè)務(wù)過(guò)程.分析階段包含如下4 個(gè)具體步驟.

(a)基于弱合理將協(xié)同業(yè)務(wù)過(guò)程行為抽象為完整的簡(jiǎn)單路徑;

(b)將抽象的完整簡(jiǎn)單路徑合并以構(gòu)建核,核中包含修正前的協(xié)同業(yè)務(wù)過(guò)程中所有正確的任務(wù)執(zhí)行系列;

(c)將核隱藏、最小化后生成每個(gè)參與組織的中間業(yè)務(wù)過(guò)程;

(d)將中間業(yè)務(wù)過(guò)程協(xié)調(diào)映射為修正業(yè)務(wù)過(guò)程,通過(guò)將修正業(yè)務(wù)過(guò)程并發(fā)組合建立修正協(xié)同業(yè)務(wù)過(guò)程.

下面將對(duì)圖1 所示的正確性修正方法進(jìn)行詳細(xì)的闡述.

2 協(xié)同業(yè)務(wù)過(guò)程定義

為了實(shí)現(xiàn)協(xié)同業(yè)務(wù)過(guò)程與需求一致性檢測(cè),參與組織需要首先對(duì)協(xié)同業(yè)務(wù)過(guò)程及期望需求進(jìn)行建模.

2.1 協(xié)同業(yè)務(wù)過(guò)程建模

對(duì)協(xié)同業(yè)務(wù)過(guò)程進(jìn)行形式定義是實(shí)現(xiàn)協(xié)同業(yè)務(wù)過(guò)程正確性修正的基礎(chǔ).本節(jié)采用標(biāo)號(hào)遷移系統(tǒng)對(duì)業(yè)務(wù)過(guò)程建模,并將其并發(fā)組合形成協(xié)同業(yè)務(wù)過(guò)程.

業(yè)務(wù)過(guò)程由參與組織活動(dòng)集和建立其上的控制流組成,它由該組織自治管理,是構(gòu)建協(xié)同業(yè)務(wù)過(guò)程的基礎(chǔ).本文采用標(biāo)號(hào)遷移系統(tǒng)建模業(yè)務(wù)過(guò)程.

定義1(業(yè)務(wù)過(guò)程).業(yè)務(wù)過(guò)程是一個(gè)遷移系統(tǒng)BP=(S,s0,F,A,Δ),其中,

(1)S為狀態(tài)集合;

(2)s0∈S為初始狀態(tài);

(3)F?S為終止?fàn)顟B(tài)集合;

(4)A=Al∪Ai為活動(dòng)集合,其中,Al為本地活動(dòng)集合,Ai為交互活動(dòng)集合;

(5)Ai=Asi∪Aai,其中,Asi為同步交互活動(dòng)集合,Aai為異步交互活動(dòng)集合;

(6)Aai=Aas∪Aar,其中,Aas為異步發(fā)送活動(dòng)集合,Aar為異步接收活動(dòng)集合;

(7)Δ?S×A×S為狀態(tài)遷移關(guān)系集,用來(lái)刻畫(huà)活動(dòng)間執(zhí)行順序,即控制流.對(duì)于?(r,a,s)∈Δ,記為遷移,表示BP在執(zhí)行活動(dòng)a后由狀態(tài)r轉(zhuǎn)換為狀態(tài)s.

特別地,稱BP是確定的當(dāng)且僅當(dāng)對(duì)于其中的任意兩條遷移,若a1=a2,則s1=s2.本文中所討論的業(yè)務(wù)過(guò)程均默認(rèn)是確定的.對(duì)于任意同步交互活動(dòng)a∈Asi,則協(xié)同業(yè)務(wù)過(guò)程中至少存在一個(gè)其他業(yè)務(wù)過(guò)程BP′,BP′的同步交互活動(dòng)集合中包含a;而對(duì)于任意異步交互活動(dòng)a∈Aai,若a∈Aas,則a記為!m,表示發(fā)送消息m的活動(dòng),“!”表示發(fā)送動(dòng)作,若a∈Aar,則a記為?m,表示接收消息m的活動(dòng),“?”表示接收動(dòng)作.對(duì)于業(yè)務(wù)過(guò)程BP,其發(fā)送消息集為={m|!m∈Aas},而接收消息集為={m|?m∈Aar}.

采用標(biāo)號(hào)遷移系統(tǒng)建模業(yè)務(wù)過(guò)程有如下3 個(gè)方面的原因:(1)標(biāo)號(hào)遷移系統(tǒng)具有直觀圖形表示,可以形式化地刻畫(huà)系統(tǒng)的行為,是系統(tǒng)行為深入分析的可靠工具[17];(2)遷移系統(tǒng)作為一種中間表示,任意具有執(zhí)行語(yǔ)義的過(guò)程模型(如利用Petri 網(wǎng)或進(jìn)程代數(shù)建模過(guò)程模型)都可以方便地轉(zhuǎn)換為本文中以標(biāo)號(hào)遷移系統(tǒng)描述業(yè)務(wù)過(guò)程[17];(3)便于后文中映射生成修正業(yè)務(wù)過(guò)程.特別需要說(shuō)明的是,由于Petri 網(wǎng)具有直觀圖形化表示,嚴(yán)格形式語(yǔ)義和豐富的形式分析技術(shù),被廣泛地用于業(yè)務(wù)過(guò)程建模和分析中.本文沒(méi)有采用Petri 網(wǎng)進(jìn)行協(xié)同業(yè)務(wù)過(guò)程修正的根本原因是在具體修正中需要首先生成協(xié)同業(yè)務(wù)過(guò)程完整簡(jiǎn)單路徑,然后合成核(本質(zhì)上是標(biāo)號(hào)遷移系統(tǒng)),最后通過(guò)對(duì)核進(jìn)行協(xié)調(diào)映射生成每個(gè)修正業(yè)務(wù)過(guò)程(也為標(biāo)號(hào)遷移系統(tǒng)).而若采用Petri 網(wǎng)建模協(xié)同業(yè)務(wù)過(guò)程,則具體修正仍然需要對(duì)應(yīng)到標(biāo)號(hào)遷移系統(tǒng)上開(kāi)展,不夠直觀.

以業(yè)務(wù)過(guò)程為基礎(chǔ)可建模協(xié)同業(yè)務(wù)過(guò)程.本質(zhì)上,協(xié)同業(yè)務(wù)過(guò)程可視為由多個(gè)業(yè)務(wù)過(guò)程構(gòu)成的并發(fā)交互系統(tǒng).進(jìn)程代數(shù)能夠自然地以模塊的方式構(gòu)建復(fù)雜的交互并發(fā)系統(tǒng)[18],借鑒其思想,本文提出并發(fā)操作符概念.并發(fā)操作符提供了一種通過(guò)組合業(yè)務(wù)過(guò)程構(gòu)建協(xié)同業(yè)務(wù)過(guò)程方法.

定義2(協(xié)同業(yè)務(wù)過(guò)程).設(shè)參與協(xié)同的業(yè)務(wù)過(guò)程為BP1,…,BPn,由這n個(gè)業(yè)務(wù)過(guò)程構(gòu)成的協(xié)同業(yè)務(wù)過(guò)程記為CBP=BP1||…||BPn.

特性需要說(shuō)明的是,定義2 只是將多個(gè)業(yè)務(wù)過(guò)程在形式上列為并發(fā)關(guān)系,CBP中的活動(dòng)執(zhí)行及交互可按實(shí)際場(chǎng)景來(lái)定義.本文同時(shí)考慮活動(dòng)間同步交互及基于消息通信的活動(dòng)間異步交互,參見(jiàn)定義5.

對(duì)于任意協(xié)同業(yè)務(wù)過(guò)程,其狀態(tài)用格局來(lái)表示.它由每個(gè)參與組織的運(yùn)行狀態(tài)及所配置的先進(jìn)先出消息隊(duì)列組成向量表示,其形式定義如下.

定義3(格局).協(xié)同業(yè)務(wù)過(guò)程CBP狀態(tài)表示為一個(gè)格局c=〈s1,Q1,…,sn,Qn〉,其中,?i∈[1..n],si為業(yè)務(wù)過(guò)程BPi的運(yùn)行狀態(tài);Qi為業(yè)務(wù)過(guò)程BPi的先進(jìn)先出消息隊(duì)列,用來(lái)存儲(chǔ)其接收消息,本文中Qi的長(zhǎng)度默認(rèn)為無(wú)窮.

特別地,CBP的初始格局記為c0=〈s01,NIL,…,s0n,NIL〉,其中,?i∈[1..n],s0i為BPi的初始狀態(tài),且其消息隊(duì)列為空,即為NIL;CBP的終止格局記為ce=〈se1,NIL,…,sen,NIL〉,其中,?i∈[1..n],sei為BPi的終止?fàn)顟B(tài),且其消息隊(duì)列為空,表示所有的消息均被接收.

可對(duì)格局中的運(yùn)行狀態(tài)及消息隊(duì)列進(jìn)行重置,形式定義如下.

定義4(格局重置).設(shè)格局c=〈s1,Q1,…,sn,Qn〉,將業(yè)務(wù)過(guò)程BPi的運(yùn)行狀態(tài)由si重置為s′i,記為,而將BPi的消息隊(duì)列由Qi重置為Q′i,記為.

在協(xié)同業(yè)務(wù)過(guò)程中,活動(dòng)執(zhí)行除了受到本地控制流的約束外,還受到其他業(yè)務(wù)過(guò)程中活動(dòng)執(zhí)行情況的影響.歸納起來(lái),可分為如下3 種情況.

1)若a∈Al,則活動(dòng)a執(zhí)行僅受到本地控制流的影響;

2)若a∈Asi,則活動(dòng)a執(zhí)行除了受到本地控制流的影響外,還需要所有含有同步交互活動(dòng)a的業(yè)務(wù)過(guò)程同時(shí)參與完成;

3)若a=!m,則活動(dòng)a執(zhí)行除了受到本地控制流的影響外,還受到其他需要接收消息m的業(yè)務(wù)過(guò)程的消息隊(duì)列Q的影響,即Q不滿,且存在接收消息m的業(yè)務(wù)過(guò)程BP.在發(fā)送消息m之后,消息m被添加至BP消息隊(duì)列的尾部;而若a=?m,則活動(dòng)a執(zhí)行除了受到本地控制流的影響外,還受到自身消息隊(duì)列Q的影響,即Q不空,且Q的第1 個(gè)元素是消息m.在接收消息m之后,消息m從Q的頭部移除.

根據(jù)上述對(duì)活動(dòng)執(zhí)行情況的分析,我們定義協(xié)同業(yè)務(wù)過(guò)程點(diǎn)火規(guī)則.

定義5(點(diǎn)火規(guī)則).設(shè)CBP=BP1||BP2||…||BPn為一個(gè)協(xié)同業(yè)務(wù)過(guò)程,其格局為c=〈s1,Q1,…,sn,Qn〉,則其點(diǎn)火規(guī)則定義如下.

(1)若a∈Al,則,當(dāng)且僅當(dāng);

(2)若a∈Asi,則,當(dāng)且僅當(dāng);

(3)若a=!m,則,當(dāng)且僅當(dāng)(是Qj的長(zhǎng)度);

(4)若a=?m,則,當(dāng)且僅當(dāng).

特別需要說(shuō)明的是,給定協(xié)同業(yè)務(wù)過(guò)程CBP,若利用點(diǎn)火規(guī)則可產(chǎn)生無(wú)窮個(gè)格局,則稱CBP具有無(wú)窮狀態(tài)空間,否則稱其具有有窮狀態(tài)空間.本文關(guān)注具有有窮狀態(tài)空間的協(xié)同業(yè)務(wù)過(guò)程.

基于點(diǎn)火規(guī)則,我們可定義協(xié)同業(yè)務(wù)過(guò)程的行為,表示為路徑.下面給出幾個(gè)與路徑相關(guān)的定義.

定義6(路徑).給定協(xié)同業(yè)務(wù)過(guò)程CBP,其行為表示為路徑,是CBP的格局和活動(dòng)(即本地活動(dòng)或交互活動(dòng))組成的有窮或無(wú)窮序列.對(duì)于任意路徑σ,其形如:,其中,?i∈[1..n],遷移符合定義5 給出的點(diǎn)火規(guī)則,ci為CBP的格局,c0為初始格局.

定義7(路徑的軌跡).對(duì)于任意路徑r,r=,則將r中的活動(dòng)依次連接,得到活動(dòng)執(zhí)行序列l(wèi)=a0∧a1…an-1∧an∧…稱為r的跡,表示為trace(r).

特別地,若格局c可通過(guò)執(zhí)行跡l遷移至格局c′,則記為.

定義8(路徑一致).設(shè)為兩條有窮路徑,稱rp和rq一致,記為rp=rq,當(dāng)且僅當(dāng)rp的跡與rq的跡相同.

3 正確性分析

為了對(duì)協(xié)同業(yè)務(wù)過(guò)程進(jìn)行修正,首先需要明確協(xié)同業(yè)務(wù)過(guò)程的正確性.目前,研究者提出多種針對(duì)協(xié)同業(yè)務(wù)過(guò)程的正確性標(biāo)準(zhǔn),其中,以合理性[9]及其變體(如弱合理[11]等)應(yīng)用最為廣泛.由于合理性主要用于定義組織內(nèi)業(yè)務(wù)過(guò)程的正確性且較為嚴(yán)格[11],因此本文利用弱合理性定義協(xié)同業(yè)務(wù)過(guò)程的正確性.

定義9(弱合理).給定協(xié)同業(yè)務(wù)過(guò)程CBP,c0和ce分別為初始格局和終止格局,稱CBP是弱合理的,當(dāng)且僅當(dāng)對(duì)于從c0可達(dá)的任意格局c,存在跡σ,使得.

從定義9 可以看出,弱合理性要求從初始格局可達(dá)的任意格局都能夠到達(dá)終止格局.這可確保每個(gè)業(yè)務(wù)過(guò)程均能到達(dá)終止?fàn)顟B(tài),因此可避免協(xié)同業(yè)務(wù)過(guò)程運(yùn)行中可能出現(xiàn)的死鎖和活鎖等情形.同時(shí),終止格局(見(jiàn)定義3)要求每個(gè)業(yè)務(wù)過(guò)程的消息隊(duì)列均為空,能夠確保協(xié)同中產(chǎn)生的消息均可合理地被接收.

本文中的正確性分析是基于路徑開(kāi)展的.實(shí)際中的協(xié)同業(yè)務(wù)過(guò)程通常含有循環(huán)結(jié)構(gòu),循環(huán)結(jié)構(gòu)將導(dǎo)致路徑數(shù)量和長(zhǎng)度變?yōu)闊o(wú)窮,進(jìn)而導(dǎo)致正確性檢測(cè)無(wú)法判定.為了將問(wèn)題收縮至有窮范圍,同時(shí)記錄下必要的循環(huán)結(jié)構(gòu),本文定義簡(jiǎn)單路徑如下.

定義10(簡(jiǎn)單路徑).設(shè)為協(xié)同業(yè)務(wù)過(guò)程CBP中的一條路徑,稱σ是簡(jiǎn)單路徑,當(dāng)且僅當(dāng)對(duì)于任意格局ci在σ中最多出現(xiàn)2 次,即對(duì)于?ci,N={cj|ci=cj∧j≠i}∧|N|≤2.

特別地,簡(jiǎn)單路徑對(duì)應(yīng)的軌跡稱為簡(jiǎn)單軌跡.下面給出算法1 用來(lái)計(jì)算一個(gè)協(xié)同業(yè)務(wù)過(guò)程中的簡(jiǎn)單路徑.

Algorithm1.Generating simple routes.

本質(zhì)上,算法1 是一種深度優(yōu)先搜索算法.設(shè)CBP中格局?jǐn)?shù)為n,且在搜索過(guò)程中每個(gè)格局入棧次數(shù)為{c1,…,cn},則算法1 的時(shí)間復(fù)雜度為.進(jìn)一步地,對(duì)于?i∈[1..n],根據(jù)定義10 可知,ci最大值為2(對(duì)應(yīng)算法第8 行),即ci存在于循環(huán)結(jié)構(gòu)中被記錄2 次.因此,算法1 在最壞情況下的時(shí)間復(fù)雜度為O(2n2).特別地,由于本文關(guān)注具有有窮狀態(tài)空間的協(xié)同業(yè)務(wù)過(guò)程,即其中含有的格局?jǐn)?shù)是有窮的.因此,可推出算法1 是可以終止的,進(jìn)而可推出其中含有的簡(jiǎn)單路徑數(shù)量及長(zhǎng)度也是有窮的.

定義11(完整的簡(jiǎn)單路徑).設(shè)為協(xié)同業(yè)務(wù)過(guò)程CBP中的一條簡(jiǎn)單路徑,稱σ為完整簡(jiǎn)單路徑,當(dāng)且僅當(dāng)cn為終止格局.

特別地,完整的簡(jiǎn)單路徑所對(duì)應(yīng)的軌跡稱為完整軌跡.由弱合理及簡(jiǎn)單路徑,對(duì)協(xié)同業(yè)務(wù)過(guò)程進(jìn)行合理性分析可轉(zhuǎn)換為對(duì)簡(jiǎn)單路徑的分析,見(jiàn)定理1.

定理1.設(shè)R為協(xié)同業(yè)務(wù)過(guò)程CBP中所有的簡(jiǎn)單路徑集合,若對(duì)于任意簡(jiǎn)單路徑r∈R,r是完整簡(jiǎn)單路徑,則CBP是弱合理的.

證明:設(shè)cm為從c0出發(fā)且經(jīng)跡σ到達(dá)的任意一個(gè)格局,則可推出存在路徑,滿足trace(r)=σ,分下面兩種情況加以討論.

1)若cm為終止格局,則推出存在空跡t,使得.

2)若cm為非終止格局,再分下面兩種情況加以討論.

(1)若r滿足?1≤i,j≤m∧j≠i,ci≠cj,則可知r為某條簡(jiǎn)單路徑ra∈R的前綴片段.由于rs是完整路徑,則可知必定存在跡t,使得.

(2)若r存在片段,滿足ci=cj=ck∧?i

綜合上述(1)和(2)及定義9,結(jié)論成立.證畢. □

基于定理1,設(shè)R為協(xié)同業(yè)務(wù)過(guò)程CBP中所有的簡(jiǎn)單路徑集合,R中所有的完整簡(jiǎn)單路徑為Rc.若|Rc|=0,表示R中每條簡(jiǎn)單路徑均不是完整路徑,則稱CBP是完全不正確的;若|Rc|≠0∧|Rc|<|R|,表示R中有部分簡(jiǎn)單路徑是完整簡(jiǎn)單路徑,則稱CBP是部分正確的;若|Rc|=|R|,表示R中所有的簡(jiǎn)單路徑均是完整路徑.根據(jù)定理1 可知,CBP滿足弱合理性,稱CBP是完全正確的.

只有在部分正確的情況下,才可能且有必要對(duì)協(xié)同業(yè)務(wù)過(guò)程進(jìn)行修正.以獲得的所有完整簡(jiǎn)單路徑為基礎(chǔ),下面詳細(xì)地闡述針對(duì)協(xié)同業(yè)務(wù)過(guò)程的修正方法.

4 正確性修正

針對(duì)部分正確的協(xié)同業(yè)務(wù)過(guò)程,其修正可分3 步進(jìn)行:(1)將所有完整的簡(jiǎn)單路徑合并為核;(2)將核映射為修正業(yè)務(wù)過(guò)程;(3)將產(chǎn)生的修正業(yè)務(wù)過(guò)程利用并發(fā)操作符組合,構(gòu)建修正協(xié)同業(yè)務(wù)過(guò)程.

對(duì)于部分正確的協(xié)同業(yè)務(wù)過(guò)程而言,根據(jù)第3 節(jié)中的闡述可知,其中必定含有完整的簡(jiǎn)單路徑(即能夠正確地執(zhí)行完成路徑)和非完整的簡(jiǎn)單路徑(即導(dǎo)致協(xié)同業(yè)務(wù)過(guò)程執(zhí)行失敗路徑).為了捕獲其中含有的所有正確路徑(即完整的簡(jiǎn)單路徑),本文提出了核的概念.本質(zhì)上,對(duì)于一個(gè)部分正確的協(xié)同業(yè)務(wù)過(guò)程,它對(duì)應(yīng)的核是含有其中所有完整簡(jiǎn)單路徑的一個(gè)遷移系統(tǒng).

定義12(核).核是五元組c=(C,c0,Ce,A,Δ),其中,

(1)C為格局集合;

(2)c0∈C為初始格局;

(3)Ce∈C為終止格局集;

(4)A為活動(dòng)集合;

(5)Δ∈C×A×C為格局遷移關(guān)系集合.

特別地,對(duì)于任意核c,其行為也可由路徑表示.對(duì)于c中任意路徑,滿足?i∈[1..n],,當(dāng)且僅當(dāng)(ci-1,ai,ci)∈Δ.

下面提出算法2,用來(lái)將所有完整的簡(jiǎn)單路徑合并以構(gòu)建核.

Algorithm2.Generating core.

算法2 的基本思想是通過(guò)將完整的簡(jiǎn)單路徑中的格局集和格局遷移集分別設(shè)置為核中的格局集和格局遷移集,從而構(gòu)建核.算法2 的時(shí)間復(fù)雜度取決于完整的簡(jiǎn)單路徑的條數(shù)及其長(zhǎng)度.不妨設(shè)完整的簡(jiǎn)單路徑條數(shù)為m,每條完整的簡(jiǎn)單路徑的長(zhǎng)度為n,則算法2 的時(shí)間復(fù)雜度為O(m×n).

特別需要說(shuō)明的是:由于完整的簡(jiǎn)單路徑中記錄了循環(huán)結(jié)構(gòu),因此最終構(gòu)建的核中循環(huán)結(jié)構(gòu)不會(huì)丟失.由此可以推斷,對(duì)于部分正確的協(xié)同業(yè)務(wù)過(guò)程,通過(guò)算法2 生成的核中只含有此協(xié)同業(yè)務(wù)過(guò)程中所有完整的簡(jiǎn)單路徑,見(jiàn)定理2.

定理2.給定部分正確的協(xié)同業(yè)務(wù)過(guò)程CBP,CBP中含有的所有完整的簡(jiǎn)單路徑記為Rc.設(shè)c是根據(jù)Rc構(gòu)建的核,則對(duì)于CBP中任意完整的簡(jiǎn)單路徑rc,c中也存在rc,反之亦然.

1)若rc滿足?1≤i,j≤n∧j≠i,ci≠cj,可知rc為完整的簡(jiǎn)單路徑,推出rc∈Rc.由算法2 可知,由Rc構(gòu)建后的c中必定存在格局遷移關(guān)系集合{(c0,a1,c1),…,(cn-1,an,cn)}?Δ,由此格局遷移關(guān)系可生成路徑rc.

2)若rc中存在路徑片段,滿足ci=cj=ck∧?ig),使得cu=cv,r′c中存在,由算法2 可知,(cg-1,ag,cg)∈Δ.因此,從左至右掃描rc,對(duì)于非循環(huán)結(jié)構(gòu)路徑片段,r′c中存在,則可推出其可由c中(cg-1,ag,cg)∈Δ生成,而對(duì)于多次重復(fù)的循環(huán)結(jié)構(gòu),r′c中存在,則可推出其可由{(ci,ai+1,ci+1),…,(cj-1,aj,ci)}?Δ生成,重復(fù)這一過(guò)程,最終可由c生成rc.

必要性.可按類似方式證明,限于篇幅,這里從略. □

給定部分正確協(xié)同業(yè)務(wù)過(guò)程CBP=BP1||BP2||…||BPn,根據(jù)算法2 生成的CBP的核為c.本文中,對(duì)CBP進(jìn)行修正目標(biāo)是要保證CBP中完整簡(jiǎn)單路徑對(duì)應(yīng)軌跡可在修正后的協(xié)同業(yè)務(wù)過(guò)程CBPr=BPr1||BPr2||…||BPrn中重現(xiàn),且CBPr中僅含有這些完整簡(jiǎn)單路徑的軌跡,以避免后續(xù)有效性確認(rèn),提高修正效率.其中,BPr1,…,BPrn分別為業(yè)務(wù)過(guò)程BP1,…,BPn對(duì)應(yīng)的修正業(yè)務(wù)過(guò)程.根據(jù)定理2,這一問(wèn)題可轉(zhuǎn)換為保證CBPr和核c的行為一致.

為了生成與CBP行為一致的CBPr,基于核c,本文提出協(xié)調(diào)映射概念.協(xié)調(diào)映射是指在映射過(guò)程中引入?yún)f(xié)調(diào)因子(對(duì)應(yīng)活動(dòng)),用于建模協(xié)調(diào)交互以實(shí)現(xiàn)協(xié)調(diào)邏輯,從而確保由映射生成BPr1,…,BPrn并發(fā)組合形成CBPr能夠遵循cc行為.從外界視角來(lái)觀察,在忽視協(xié)調(diào)因子的情況下,協(xié)調(diào)映射可使得CBPr只包含CBP中所有完整簡(jiǎn)單路徑的軌跡.

在實(shí)際應(yīng)用中,不是CBP中的每個(gè)活動(dòng)都需要進(jìn)行協(xié)調(diào).以核為基礎(chǔ),本文提出協(xié)調(diào)活動(dòng)的概念.

定義13(協(xié)調(diào)活動(dòng)).給定部分正確協(xié)同業(yè)務(wù)過(guò)程CBP=BP1||BP2||…||BPn,CBP對(duì)應(yīng)的核c=(C,c0,Ce,A,Δ),稱活動(dòng)a∈A1∪A2∪…∪An為協(xié)調(diào)活動(dòng),當(dāng)且僅當(dāng)存在格局c1∈C,使得,且c2?C,其中,?i∈[1..n],Ai為業(yè)務(wù)過(guò)程BPi的活動(dòng)集.

由定義13 可知,協(xié)調(diào)活動(dòng)是指在協(xié)同業(yè)務(wù)過(guò)程執(zhí)行中若不加以控制,則可能導(dǎo)致隱藏路徑產(chǎn)生的活動(dòng),即從初始格局c0至c2或由c2引出路徑.因此,需要對(duì)這些活動(dòng)進(jìn)行協(xié)調(diào),使其執(zhí)行后到達(dá)正確格局c1,避免達(dá)到異常格局c2.而對(duì)于除協(xié)調(diào)活動(dòng)以外的其他活動(dòng),由于其執(zhí)行后總能夠到達(dá)正確狀態(tài),因此無(wú)需協(xié)調(diào).

以核為基礎(chǔ),映射生成修正業(yè)務(wù)過(guò)程之前需先將核中不相關(guān)活動(dòng)(即不屬于此業(yè)務(wù)過(guò)程及不是協(xié)調(diào)活動(dòng)的其他活動(dòng))隱藏,形式定義如下.

定義14(隱藏).給定部分正確協(xié)同業(yè)務(wù)過(guò)程CBP,BP=(S,s0,F,A,Δ)為CBP中一個(gè)業(yè)務(wù)過(guò)程,CBP對(duì)應(yīng)的核c=(C,c0,Ce,A,Δ),協(xié)調(diào)活動(dòng)集為Ac,則根據(jù)BP及Ac對(duì)c進(jìn)行隱藏后得到隱藏核為c′=(C′,c′0,C′e,A′,Δ′),其中,

(1)C′=C;

(2)A′={τ}∪{a|?(r,a,s)∈c.Δ∧a∈A∪Ac};

(3)對(duì)于?(r,a,s)∈Δ,如果a∈A∪Ac,則(r,a,s)∈Δ′,否則,τ格局遷移關(guān)系(r,τ,s)∈Δ′.

由定義14 可知,隱藏是將c中格局遷移關(guān)系重置.即若格局遷移關(guān)系中活動(dòng)是BP中活動(dòng)或是協(xié)調(diào)活動(dòng),則在重置的格局遷移關(guān)系中保持不變,否則將其設(shè)置為不可見(jiàn)活動(dòng)τ.

在對(duì)c進(jìn)行隱藏后,需要將產(chǎn)生的隱藏核c′最小化以生成修正業(yè)務(wù)過(guò)程.當(dāng)前,研究者提出多種行為最小化技術(shù)[19],如軌跡最小化、分支最小化及互模擬最小化等.由于本文關(guān)注協(xié)同業(yè)務(wù)過(guò)程間的路徑一致,即路徑對(duì)應(yīng)軌跡相同,因此我們采用文獻(xiàn)[20]中提出的弱軌跡最小化算法對(duì)隱藏核進(jìn)行最小化操作,最小化后生成一個(gè)中間有窮自動(dòng)機(jī).本質(zhì)上,標(biāo)號(hào)遷移系統(tǒng)是一類特殊有窮自動(dòng)機(jī).因此,通過(guò)將中間有窮自動(dòng)機(jī)中的狀態(tài)集、開(kāi)始狀態(tài)、結(jié)束狀態(tài)集、活動(dòng)集及狀態(tài)遷移關(guān)系分別對(duì)應(yīng)到標(biāo)號(hào)遷移系統(tǒng)中的狀態(tài)集、初始狀態(tài)、終止?fàn)顟B(tài)集、活動(dòng)集及狀態(tài)遷移關(guān)系,則可由隱藏核生成一個(gè)中間業(yè)務(wù)過(guò)程.這種轉(zhuǎn)換過(guò)程非常直觀,限于篇幅,這里不再贅述.通過(guò)利用文獻(xiàn)[20]中提出的最小化方法,可確保中間業(yè)務(wù)過(guò)程與隱藏核保持弱軌跡等價(jià),且中間業(yè)務(wù)過(guò)程中不含有不可見(jiàn)活動(dòng).

基于最小化后生成的中間業(yè)務(wù)過(guò)程,根據(jù)協(xié)調(diào)活動(dòng)集,下面給出協(xié)調(diào)映射定義,以生成修正業(yè)務(wù)過(guò)程.

定義15(協(xié)調(diào)映射).給定部分正確協(xié)同業(yè)務(wù)過(guò)程CBP=BP1||BP2||…||BPn,BP=(S,s0,F,A,Δ)為CBP中的一個(gè)業(yè)務(wù)過(guò)程,Ac為CBP中的協(xié)調(diào)活動(dòng)集,最小化后生成中間業(yè)務(wù)過(guò)程為BPm=(Sm,sm0,Fm,Am,Δm),則根據(jù)BP和Ac對(duì)BPm進(jìn)行協(xié)調(diào)映射后得到修正業(yè)務(wù)過(guò)程為BPr=(Sr,sr0,F,Ar,Δr),其中,

(1)Sr=Sm∪{sc|?(r,a,s)∈Δm∧a?A∧a∈Ac}∪{sc1,sc2|?(r,a,s)∈Δm∧a∈A∧a∈Ac};

(2)sr0=sm0;

(3)Fr=Fm;

(4)Ar={a|?(r,a,s)∈cc.Δm∧a∈A∧a?Ac}∪{SYNC_1_a,SYNC_2_a|?(r,a,s)∈Δm∧a∈A∧a∈Ac}∪{SYNC_1_a,SYNC_2_a|?(r,a,s)∈Δm∧a?A∧a∈Ac};

(5)Δr={(r,SYNC_1_a,sc),(sc,SYNC_2_a,s)|?(r,a,s)∈Δm∧a?A∧a∈Ac}∪{(r,SYNC_1_a,sc1),(sc1,a,sc2),(sc2,SYNC_2_a,s)|?(r,a,s)∈Δm∧a∈A∧a∈Ac}∪{(r,a,s)|?(r,a,s)∈cc.Δm∧a∈A∧a?Ac}.

定義15 中,對(duì)于BPm中的一個(gè)活動(dòng)a:(1)若a不屬于BP但需協(xié)調(diào),則引入?yún)f(xié)調(diào)因子SYNC_1_a、SYNC_2_a及協(xié)調(diào)狀態(tài)sc,用于將BPm中的格局遷移關(guān)系(r,a,s)設(shè)置為(r,SYNC_1_a,sc)和(sc,SYNC_2_a,s),表示在狀態(tài)r通過(guò)協(xié)調(diào)因子SYNC_1_a對(duì)活動(dòng)a開(kāi)始進(jìn)行協(xié)調(diào),并通過(guò)協(xié)調(diào)因子SYNC_2_a對(duì)活動(dòng)a結(jié)束協(xié)調(diào);(2)若a屬于BP且需協(xié)調(diào),則引入?yún)f(xié)調(diào)因子SYNC_1_a、SYNC_2_a及協(xié)調(diào)狀態(tài)sc1和sc2,用于將格局遷移關(guān)系(r,b,s)設(shè)置為3 個(gè)狀態(tài)遷移關(guān)系(r,SYNC_1_a,sc1)、(sc1,a,sc2)和(sc2,SYNC_2_a,s),表示在a執(zhí)行前需進(jìn)行協(xié)調(diào),通過(guò)SYNC_1_a來(lái)實(shí)現(xiàn),執(zhí)行完成后進(jìn)行結(jié)束協(xié)調(diào),通過(guò)SYNC_2_a來(lái)實(shí)現(xiàn);(3)若a屬于BP且無(wú)需協(xié)調(diào),則格局遷移關(guān)系(r,b,s)保持不變.

本質(zhì)上,修正業(yè)務(wù)過(guò)程是一個(gè)遷移系統(tǒng).特別地,給定一個(gè)業(yè)務(wù)過(guò)程BP,其修正業(yè)務(wù)過(guò)程BP′受BP行為(即遷移序列)和協(xié)調(diào)因子的影響.根據(jù)我們的實(shí)驗(yàn)可以發(fā)現(xiàn)(見(jiàn)第5.2 節(jié)),BP′結(jié)構(gòu)通常較BP更復(fù)雜.同時(shí),本文中BP′采用LTS 進(jìn)行描述,LTS 描述模型較其他圖形化方式(如BPMN、BPEL 和Petri 網(wǎng))描述的模型復(fù)雜、難懂.這就限制了本文方法在實(shí)際中被用戶接受的程度.事實(shí)上,研究者已經(jīng)提出了一些方法[21]用于將以LTS 描述模型轉(zhuǎn)換為Petri 網(wǎng)描述模型,且能夠保持轉(zhuǎn)換前后行為一致(如保持強(qiáng)互模擬等).因此,針對(duì)修正業(yè)務(wù)過(guò)程對(duì)于用戶較難理解這個(gè)問(wèn)題,可以考慮利用工具Petrify(https://www.merriam-webster.com/dictionary/petrify)將其轉(zhuǎn)換為Petri網(wǎng)來(lái)增強(qiáng)其實(shí)用性.有關(guān)Petrify 介紹及使用可以參見(jiàn)文獻(xiàn)[21],限于篇幅,這里不再闡述.

通過(guò)將修正業(yè)務(wù)過(guò)程集利用并發(fā)操作符加以組合,得到如下定義的修正協(xié)同業(yè)務(wù)過(guò)程.

定義16(修正協(xié)同業(yè)務(wù)過(guò)程).給定部分正確協(xié)同業(yè)務(wù)過(guò)程CBP=BP1||BP2||…||BPn,BPr1,…,BPrn分別為業(yè)務(wù)過(guò)程BP1,…,BPn對(duì)應(yīng)的修正業(yè)務(wù)過(guò)程,則修正協(xié)同業(yè)務(wù)過(guò)程為CBPr=BPr1||BPr2||…||BPrn.

在忽視協(xié)調(diào)因子的情況下,修正協(xié)同業(yè)務(wù)過(guò)程中只含有修正前的協(xié)同業(yè)務(wù)過(guò)程中的所有完整軌跡,可見(jiàn)定理3.

定理3.給定部分正確協(xié)同業(yè)務(wù)過(guò)程CBP=BP1||BP2||…||BPn,CBPr=BPr1||BPr2||…||BPrn為CBP的修正協(xié)同業(yè)務(wù)過(guò)程,則如下結(jié)論成立.

(1)對(duì)于CBP中任意完整的簡(jiǎn)單路徑r,CBPr中存在一條完整的簡(jiǎn)單路徑r′,滿足trace(r)=trace(r′)↑Acf;

(2)對(duì)于CBPr中任意完整的簡(jiǎn)單路徑r,CBP中存在一條完整的簡(jiǎn)單路徑r′,滿足trace(r′)=trace(r)↑Acf;

其中,Acf為CBP中所有協(xié)調(diào)因子集合;trace(r)↑Acf表示將r的任務(wù)執(zhí)行序列中的協(xié)調(diào)因子移除后形成的新任務(wù)執(zhí)行序列.

證明:1)設(shè)c為根據(jù)算法2 生成CBP的核,為c中任意一條完整的簡(jiǎn)單路徑.由定義14 可知,對(duì)于r中任意遷移,每個(gè)業(yè)務(wù)過(guò)程BPn(1≤i≤n)對(duì)應(yīng)隱藏核中存在如下遷移,記為C1:

由文獻(xiàn)[20]中提出的最小化方法可知,所有的τ-格局遷移關(guān)系(即由τ引起的格局遷移關(guān)系)均被移除,且滿足弱軌跡等價(jià),則最小化隱藏核后生成的業(yè)務(wù)過(guò)程BP中有如下遷移,記為C2:

根據(jù)定義15,每個(gè)修正業(yè)務(wù)過(guò)程BPrj(1≤j≤n)中的遷移進(jìn)行如下協(xié)調(diào)映射,記為C3:

從左至右依次掃描r,根據(jù)定義5 中的點(diǎn)火規(guī)則可生成如下路徑r′,滿足:

根據(jù)C3,由于r為完整的簡(jiǎn)單路徑,則可推出r′中km也為終止格局,故r′是完整的簡(jiǎn)單路徑.進(jìn)一步地,推出trace(r)=trace(r′)↑Acf成立.根據(jù)定理2,c與CBP中完整的簡(jiǎn)單路徑一致,故結(jié)論(1)成立.

2)采用反證法證明.設(shè)CBPr中存在路徑片段,且c中存在對(duì)應(yīng)路徑片段r2,滿足trace(r2)=trace(r1)↑Acf.但CBPr中存在后續(xù)遷移使得路徑片段不為c中任意完整的簡(jiǎn)單路徑的前綴.按如下兩步證明后續(xù)活動(dòng)a不能發(fā)生.

(1)首先明確活動(dòng)a是協(xié)調(diào)活動(dòng),即a∈Ac.針對(duì)路徑片段r1,由于c中存在對(duì)應(yīng)路徑片段r2,滿足trace(r2)=trace(r1)↑Acf.因此,從左至右掃描r1,對(duì)于r1中路徑片段:,或者ki-1ki,則用替換,重復(fù)這一過(guò)程,最終可求得kk對(duì)應(yīng)于ck.由C3 可知,若后續(xù)遷移發(fā)生后使得r3不為c中任意完整簡(jiǎn)單路徑的前綴,那么a∈Ac.

(2)再證明協(xié)調(diào)活動(dòng)a在CBPr中不能發(fā)生.分下面兩種情況加以討論.

i)a不在c中出現(xiàn),即a?c.A.由C3 可知,后續(xù)遷移不存在;

ii)a在c中出現(xiàn),即a∈c.A.設(shè)有后續(xù)有效遷移,使得為c中某條完整簡(jiǎn)單路徑的前綴.若活動(dòng)a能執(zhí)行,再分如下兩種情況進(jìn)行討論.

①若a和b屬于同一個(gè)修正業(yè)務(wù)過(guò)程BPrj(1≤j≤n),則推出a和b處于選擇關(guān)系.由C3 可知,若a能夠執(zhí)行,則b不能執(zhí)行.但遷移是有效的,故活動(dòng)a不能執(zhí)行;

② 若a和b屬于不同的修正業(yè)務(wù)過(guò)程,不妨設(shè)分別屬于業(yè)務(wù)過(guò)程BPri和BPrj(1≤i,j≤n).根據(jù)C3 可推出,BPrj中存在遷移.根據(jù)定義5 給出的點(diǎn)火規(guī)則,若活動(dòng)a能夠執(zhí)行,則活動(dòng)b不能執(zhí)行.但遷移是有效的,故活動(dòng)a不能執(zhí)行.

綜合上述(1)和(2)推導(dǎo)可知,結(jié)論(2)成立. □

定理3 中的結(jié)論(1)表明修正前的協(xié)同業(yè)務(wù)過(guò)程中所有完整的簡(jiǎn)單路徑都可以在修正協(xié)同業(yè)務(wù)過(guò)程中重現(xiàn);而結(jié)論(2)則表明未引入隱藏軌跡.這將避免修正后進(jìn)行有效性確認(rèn),從而提高了修正效率.

特別需要明確的是,本文方法可支持帶有一般循環(huán)結(jié)構(gòu)的過(guò)程模型,其原因在于修正是基于完整簡(jiǎn)單路徑開(kāi)展.完整簡(jiǎn)單路徑能夠記錄循環(huán)結(jié)構(gòu)(即自循環(huán)和一般循環(huán)結(jié)構(gòu)[17]),故通過(guò)算法2 構(gòu)建的核中循環(huán)結(jié)構(gòu)也不會(huì)丟失.最終,通過(guò)對(duì)核進(jìn)行協(xié)調(diào)映射產(chǎn)生修正業(yè)務(wù)過(guò)程也含有已有環(huán)結(jié)構(gòu).

5 實(shí)驗(yàn)評(píng)價(jià)

本文提出一種協(xié)同業(yè)務(wù)過(guò)程正確性修正方法.為了評(píng)估該方法的有效性,本節(jié)使用具有實(shí)際意義的協(xié)同業(yè)務(wù)過(guò)程集,通過(guò)與相關(guān)正確性修正方法進(jìn)行實(shí)驗(yàn)對(duì)比,從修正協(xié)同業(yè)務(wù)過(guò)程具有協(xié)同業(yè)務(wù)過(guò)程實(shí)際特征、重現(xiàn)完整軌跡及未引入隱藏軌跡等方面來(lái)分析不同正確性修正方法之間的有效性差異.

5.1 實(shí)驗(yàn)準(zhǔn)備

當(dāng)前針對(duì)協(xié)同業(yè)務(wù)過(guò)程沒(méi)有公開(kāi)的數(shù)據(jù)集可供實(shí)驗(yàn)[22],而為了評(píng)價(jià)本文提出方法的有效性,我們從已有的研究論文[23,24]及BPMN 案例庫(kù)(http://www.bpmn.org/)中選取6 個(gè)較為典型的協(xié)同業(yè)務(wù)過(guò)程進(jìn)行實(shí)驗(yàn).其中,Order Product(記為OP)、Purchase Order(記為PO)及Travel Booking System(記為T(mén)BS)分別作為文獻(xiàn)[23,24]中的啟發(fā)案例,用來(lái)闡述跨組織業(yè)務(wù)過(guò)程建模并分析方法的有效性,代表性較強(qiáng);Amazon Online Purchase(記為AOP)、The Nobel Prize(記為T(mén)NP)和Incident Management(記為IM)則來(lái)自BPMN 案例庫(kù),能夠反映實(shí)際的協(xié)同業(yè)務(wù)過(guò)程場(chǎng)景.

選取的6 個(gè)協(xié)同業(yè)務(wù)過(guò)程具有的屬性見(jiàn)表1,其中,No.of peers 表示協(xié)同業(yè)務(wù)過(guò)程中含有參與組織的個(gè)數(shù),“No.of peer states,trans”表示協(xié)同業(yè)務(wù)過(guò)程中含有的狀態(tài)數(shù)及遷移數(shù).采用標(biāo)號(hào)遷移系統(tǒng)表示過(guò)程模型中的結(jié)構(gòu)有順序、選擇和循環(huán)3 類.為了表明選取過(guò)程模型的普遍性,選取的6 個(gè)協(xié)同業(yè)務(wù)過(guò)程中含有這3 類結(jié)構(gòu).特別地,循環(huán)結(jié)構(gòu)包含自循環(huán)和一般意義上的循環(huán)結(jié)構(gòu)這兩類[17].這兩類循環(huán)結(jié)構(gòu)也反映在過(guò)程模型中,如Purchase Order 中含有自循環(huán),而Order 中則含有一般循環(huán)結(jié)構(gòu)等.

Table 1 Properties of collaborative business processes表1 協(xié)同業(yè)務(wù)過(guò)程屬性

特別地,由于本文提出正確性修正方法面向部分正確協(xié)同業(yè)務(wù)過(guò)程,因此通過(guò)項(xiàng)目組討論對(duì)選取6 個(gè)協(xié)同業(yè)務(wù)過(guò)程的內(nèi)部結(jié)構(gòu)進(jìn)行修改以注入錯(cuò)誤,其中錯(cuò)誤類型為死鎖、活鎖及消息未合理接收等.

目前,針對(duì)協(xié)同業(yè)務(wù)過(guò)程的正確性修正方法較少.本文選擇此類中的典型方法[13-15]作為實(shí)驗(yàn)比較對(duì)象,從支持協(xié)同業(yè)務(wù)過(guò)程的實(shí)際特征、重現(xiàn)完整軌跡及引入隱藏軌跡等方面進(jìn)行對(duì)比分析.

特別地,文獻(xiàn)[13]中方法的處理步驟是:先將每個(gè)業(yè)務(wù)過(guò)程采用Petri 網(wǎng)進(jìn)行建模,利用文獻(xiàn)[9]中提到的庫(kù)所熔合和變遷熔合技術(shù)構(gòu)建全局模型,并獲得其所有完備軌跡[17].這里的完備是指在全局模型中,若活動(dòng)b能夠在活動(dòng)a執(zhí)行后立即執(zhí)行,則存在一條軌跡σ,σ中存在位置i,滿足σ(i)=a,且σ(i+1)=b;然后,將獲得完備軌跡作為文獻(xiàn)[13]中正確性修正方法輸入,則可生成中心流程;最后,將中心流程與每個(gè)業(yè)務(wù)過(guò)程進(jìn)行變遷熔合,則構(gòu)建修正協(xié)同業(yè)務(wù)過(guò)程.而文獻(xiàn)[14,15]中方法的處理步驟是:先將每個(gè)業(yè)務(wù)過(guò)程采用Petri 網(wǎng)進(jìn)行建模;然后利用文獻(xiàn)[9]中庫(kù)所熔合和變遷熔合技術(shù)構(gòu)建全局模型.針對(duì)構(gòu)建的全局模型,為保持修正模型的一致性,獲得其完備軌跡;最后,將獲得的完備軌跡作為文獻(xiàn)[14,15]中模型修正方法輸入,即構(gòu)建出修正協(xié)同業(yè)務(wù)過(guò)程.

所有實(shí)驗(yàn)在一臺(tái)PC 上開(kāi)展,軟件環(huán)境為:Windows 10 及JDK 1.7,硬件環(huán)境為:處理器為Inter(R)Core(TM)i5-8250U CPU@ 1.60GHz、內(nèi)存為8GB.

5.2 實(shí)驗(yàn)結(jié)果及分析

5.2.1 支持個(gè)性化特征分析

通過(guò)對(duì)修正協(xié)同業(yè)務(wù)過(guò)程進(jìn)行分析,可以分析出本文方法在支持協(xié)同業(yè)務(wù)過(guò)程實(shí)際特征方面的有效性.跨組織業(yè)務(wù)過(guò)程建模研究表明[6-10],協(xié)同業(yè)務(wù)過(guò)程通常具有4 類特征:自治性、分布性、交互性和隱私性.其中,自治性是指每個(gè)業(yè)務(wù)過(guò)程由其所屬組織管理及運(yùn)行;分布性是指協(xié)同業(yè)務(wù)過(guò)程在結(jié)構(gòu)和執(zhí)行上具有分布性;交互性是指業(yè)務(wù)過(guò)程在執(zhí)行中需要與其他業(yè)務(wù)過(guò)程進(jìn)行交互以推動(dòng)全局流程演進(jìn);隱私性是指在跨組織環(huán)境下,參與組織希望在建模及分析過(guò)程中避免將其內(nèi)部流程信息暴露給其他參與組織.特別地,在實(shí)際應(yīng)用中,這4 類特征主要是針對(duì)構(gòu)建后的協(xié)同業(yè)務(wù)過(guò)程形態(tài)(即是否表現(xiàn)為分布式、有無(wú)中心流程等)及構(gòu)建時(shí)是否暴露流程信息給參與組織來(lái)進(jìn)行體現(xiàn).因此,上文在定義協(xié)同業(yè)務(wù)過(guò)程和闡述方法時(shí)沒(méi)有提及這4 類特征.此外,應(yīng)用這4 類特征對(duì)協(xié)同業(yè)務(wù)過(guò)程評(píng)價(jià)主要是從定性角度開(kāi)展,因此本文未在上文具體證明中及本節(jié)中應(yīng)用實(shí)驗(yàn)數(shù)據(jù)驗(yàn)證這個(gè)結(jié)果.

特別需要說(shuō)明的是,實(shí)驗(yàn)中默認(rèn)本文方法和文獻(xiàn)[13-15]中的方法對(duì)協(xié)同業(yè)務(wù)過(guò)程進(jìn)行修正均是由可信第三方TTP(trusted third party)[25]來(lái)完成,因此均能支持隱私性.在實(shí)際應(yīng)用中,參與組織先將各自的業(yè)務(wù)過(guò)程提交給TTP;之后TTP 對(duì)由其組合建立協(xié)同業(yè)務(wù)過(guò)程,并對(duì)其修正;最后TTP 將每個(gè)修正業(yè)務(wù)過(guò)程返給對(duì)應(yīng)參與組織.在跨組織環(huán)境下,為保護(hù)隱私性,這種通過(guò)TTP 對(duì)協(xié)同業(yè)務(wù)過(guò)程進(jìn)行分析是常見(jiàn)和合理的[25].

針對(duì)選取的5 個(gè)協(xié)同業(yè)務(wù)過(guò)程,本文方法和文獻(xiàn)[13-15]中的方法建立的修正協(xié)同業(yè)務(wù)過(guò)程對(duì)上述4 類特征支持情況見(jiàn)表2,其中.A表示自治性,D表示分布性,I表示交互性,P表示隱私性.

Table 2 Feature support results表2 特征支持結(jié)果

從表2 可以看出,經(jīng)本文方法建立的修正協(xié)同業(yè)務(wù)過(guò)程能夠良好地支持上述4 類特征,而經(jīng)文獻(xiàn)[13-15]中的方法建立的修正協(xié)同業(yè)務(wù)過(guò)程僅能支持隱私性.因此,相較文獻(xiàn)[13-15]中的方法,本文方法能夠更加有效地支持協(xié)同業(yè)務(wù)過(guò)程具有實(shí)際特征.

例如,對(duì)于協(xié)同業(yè)務(wù)過(guò)程集中訂單采購(gòu)OP,OP 中業(yè)務(wù)過(guò)程Customer 和Vendor 如圖2 所示.

Fig.2 Business processes customer and vendor in OP圖2 OP 中業(yè)務(wù)過(guò)程Customer 及Vendor

利用本文方法建立修正協(xié)同業(yè)務(wù)過(guò)程O(píng)Pr-o如圖3 所示,修正業(yè)務(wù)過(guò)程Customerr和Vendorr并發(fā)組合形成.

Fig.3 Repaired business processes Customerr and Vendorr圖3 修正業(yè)務(wù)過(guò)程Customerr 及Vendorr

利用文獻(xiàn)[13]中的方法建立的修正協(xié)同業(yè)務(wù)過(guò)程O(píng)Pr-z如圖4 所示,其中,虛線表示任務(wù)同步關(guān)系.

利用文獻(xiàn)[14,15]的中方法建立的修正協(xié)同業(yè)務(wù)過(guò)程O(píng)Pr-a如圖5 所示.

通過(guò)分析OPr-o、OPr-z和OPr-a可知,OPr-o由修正業(yè)務(wù)過(guò)程Customerr和Vendorr并發(fā)組合形成,即OPr-o=Customerr||Vendorr.由于這兩個(gè)修正業(yè)務(wù)過(guò)程獨(dú)立存在,且每個(gè)修正業(yè)務(wù)過(guò)程由各自組織管理,同時(shí),OPr-o按照定義5 中給出的點(diǎn)火規(guī)則運(yùn)行,表明其具有自治、分布及交互特性.同時(shí),具體修正由TTP 完成,表明其具有隱私性;而由文獻(xiàn)[13-15]中的方法建立的修正協(xié)同業(yè)務(wù)過(guò)程O(píng)Pr-z和OPr-a實(shí)質(zhì)上均是集中式的.特別地,業(yè)務(wù)過(guò)程Customer 和Vendor 中活動(dòng)及活動(dòng)間的交互不是并發(fā)執(zhí)行的,而是通過(guò)Center 和OPr-a中控制流的約束來(lái)執(zhí)行.例如,Customer 內(nèi)本地活動(dòng)browProduct執(zhí)行需要與Center 內(nèi)活動(dòng)browProduct執(zhí)行同步;而活動(dòng)!orderA和?orderA間的交互則由Center 內(nèi)控制流來(lái)約束.

Fig.4 Repaired business process POr-z圖4 修正業(yè)務(wù)過(guò)程POr-z

Fig.5 Repaired business process POr-a圖5 修正業(yè)務(wù)過(guò)程POr-a

5.2.2 軌跡有效性分析

本小節(jié)分析修正協(xié)同業(yè)務(wù)過(guò)程中重現(xiàn)完整軌跡和未引入隱藏軌跡的有效性.基于簡(jiǎn)單軌跡,本文提出精確度和泛化度這兩個(gè)有效性計(jì)算指標(biāo).

精確度的計(jì)算公式如式(1)所示.

式(1)中,TM′為修正協(xié)同業(yè)務(wù)過(guò)程中所有的簡(jiǎn)單軌跡;TM為修正前協(xié)同業(yè)務(wù)過(guò)程中所有的完整簡(jiǎn)單軌跡;acc(TM,TM′)為被TM接受的TM′中的軌跡子集.對(duì)于精確度而言,計(jì)算結(jié)果值越高,則表示修正協(xié)同業(yè)務(wù)過(guò)程中引入的隱藏軌跡越少,修正效果越好.

泛化度的計(jì)算公式如式(2)所示.

式(2)中,TM′為修正協(xié)同業(yè)務(wù)過(guò)程中所有的簡(jiǎn)單軌跡;TM為修正前協(xié)同業(yè)務(wù)過(guò)程中所有的完整簡(jiǎn)單軌跡;acc(TM′,TM)為被TM′接受的TM中的軌跡子集.對(duì)于泛化度指標(biāo),計(jì)算結(jié)果值越高,則表示修正協(xié)同業(yè)務(wù)過(guò)程中重現(xiàn)修正前協(xié)同業(yè)務(wù)過(guò)程中的完整簡(jiǎn)單軌跡越多,修正效果越好.

根據(jù)式(1)和式(2),本文方法和文獻(xiàn)[13-15]中方法的精確度和泛化度的計(jì)算結(jié)果分別如圖6(a)～圖6(b)所示.

由圖6(a)可以看出,本文方法的精確度高于文獻(xiàn)[13-15]中方法的精確度.同時(shí),本文方法的泛化度與文獻(xiàn)[14,15]中方法的泛化度相同,但遠(yuǎn)高于文獻(xiàn)[13]中的方法.由此,我們可以得出如下結(jié)論.

(1)由于本文方法能夠事先保證修正協(xié)同業(yè)務(wù)過(guò)程中含有修正前協(xié)同業(yè)務(wù)過(guò)程中所有完整的軌跡,且未引入隱藏軌跡,使得本文方法的精確度和泛化度均為1.0.圖6 所示實(shí)驗(yàn)結(jié)果也與理論分析相一致;

(2)文獻(xiàn)[14,15]中的方法在精確度方面表現(xiàn)良好,其均為1.0,表明修正協(xié)同業(yè)務(wù)過(guò)程能夠重現(xiàn)修正前的協(xié)同業(yè)務(wù)過(guò)程中所有完整的軌跡.在泛化度方面,文獻(xiàn)[14,15]中方法的值介于0.5～1.0 之間,表明在修正協(xié)同業(yè)務(wù)過(guò)程中引入了隱藏軌跡.分析發(fā)現(xiàn),這些隱藏軌跡是由修正協(xié)同業(yè)務(wù)過(guò)程中存在異常(如死鎖等)引起;

(3)文獻(xiàn)[13]中的方法在精確度和泛化度方面的表現(xiàn)都是最差的,其精確度和泛化度在選取的協(xié)同業(yè)務(wù)過(guò)程中大多為0.0,表明修正前協(xié)同業(yè)務(wù)過(guò)程中幾乎所有完整軌跡在修正協(xié)同業(yè)務(wù)過(guò)程中丟失.分析發(fā)現(xiàn),這是由于修正協(xié)同業(yè)務(wù)過(guò)程中存在異常(如死鎖等)和一些活動(dòng)丟失(如POr-z中活動(dòng)checkStock丟失等)所致.

Fig.6 Comparison in terms of precision and generality圖6 精確度和泛化度比較

5.2.3 修正時(shí)間耗費(fèi)分析

通過(guò)分析建立修正協(xié)同業(yè)務(wù)過(guò)程時(shí)間耗費(fèi),可評(píng)價(jià)本文方法的修正效率.利用本文方法和文獻(xiàn)[13-15]中的方法對(duì)協(xié)同業(yè)務(wù)過(guò)程進(jìn)行正確性修正所耗費(fèi)的時(shí)間為T(mén)cr=Tct+Tr,其中,Tct為獲取修正前協(xié)同業(yè)務(wù)過(guò)程中所有完整的軌跡時(shí)間,Tr為進(jìn)行修正所耗費(fèi)的時(shí)間;同時(shí),利用文獻(xiàn)[13-15]中的方法對(duì)協(xié)同業(yè)務(wù)過(guò)程進(jìn)行修正后還需要進(jìn)行有效性確認(rèn),所耗費(fèi)的時(shí)間為T(mén)cv=Tvp+Tvg,其中,Tvp為計(jì)算精確度時(shí)間,Tvg為計(jì)算泛化度時(shí)間.本文方法和文獻(xiàn)[13-15]中的方法建立修正協(xié)同業(yè)務(wù)過(guò)程的時(shí)間耗費(fèi)見(jiàn)表3,其中,Ttotal為修正總耗費(fèi)時(shí)間,即為正確性修正耗費(fèi)時(shí)間和有效性確認(rèn)所耗費(fèi)時(shí)間之和.特別地,為了確保結(jié)果的客觀性,每次實(shí)驗(yàn)重復(fù)10 次,然后取平均值作為建立修正協(xié)同業(yè)務(wù)過(guò)程的時(shí)間耗費(fèi).

從表3 可以看出:

(1)利用本文方法修正所耗費(fèi)的時(shí)間遠(yuǎn)遠(yuǎn)小于文獻(xiàn)[13-15]中的方法.例如,針對(duì)Travel Book System,本文方法的修正耗費(fèi)時(shí)間為3 570ms,而文獻(xiàn)[13]和文獻(xiàn)[14,15]中的方法分別耗費(fèi)133 750ms 和281 667ms.分析發(fā)現(xiàn),文獻(xiàn)[13-15]中方法修正效率低下的原因是由于上述6 個(gè)協(xié)同業(yè)務(wù)過(guò)程中含有較多完備軌跡(如Travel Book System 中含有1 458 條完備軌跡)和采用過(guò)程挖掘技術(shù)所致.可以預(yù)見(jiàn),若對(duì)更加復(fù)雜的協(xié)同業(yè)務(wù)過(guò)程進(jìn)行修正,則其時(shí)間將進(jìn)一步增加.而本文方法只需獲取所有的完整簡(jiǎn)單路徑(如Travel Book System 中只含有384 條),并對(duì)核協(xié)調(diào)映射即可生成修正協(xié)同業(yè)務(wù)過(guò)程,避免文獻(xiàn)[13-15]中方法使用過(guò)程模型挖掘算法(如α算法等)、案例差異檢測(cè)等步驟,從而縮短了修正時(shí)間;

(2)由于本文方法能夠事先保證修正協(xié)同業(yè)務(wù)過(guò)程中含有修正前協(xié)同業(yè)務(wù)過(guò)程中所有的完整軌跡,且未引入隱藏軌跡,這使得本文方法無(wú)須進(jìn)行有效性確認(rèn),即有效性確認(rèn)耗費(fèi)時(shí)間為0ms.而文獻(xiàn)[13-15]中方法的有效性確認(rèn)所耗費(fèi)的時(shí)間均較高.例如,針對(duì)Travel Book System,文獻(xiàn)[13]和文獻(xiàn)[14,15]中方法進(jìn)行有效性確認(rèn)耗費(fèi)的時(shí)間分別為20 900ms 和59 696ms.分析發(fā)現(xiàn),這是由于選取的協(xié)同業(yè)務(wù)過(guò)程和對(duì)應(yīng)修正協(xié)同業(yè)務(wù)過(guò)程中均含有較多的簡(jiǎn)單軌跡和完整軌跡所致.可以預(yù)見(jiàn),若對(duì)更加復(fù)雜的協(xié)同業(yè)務(wù)過(guò)程進(jìn)行有效性確認(rèn),則其所耗費(fèi)的時(shí)間將進(jìn)一步增加;

(3)從修正耗費(fèi)總時(shí)間來(lái)看,相較文獻(xiàn)[13]和文獻(xiàn)[14,15]中的方法,本文方法的修正效率有極大的提高,分別提高14 倍和42 倍.

綜上分析,可以得出如下結(jié)論:相比文獻(xiàn)[13-15]中所提出的正確性修正方法,在考慮協(xié)同業(yè)務(wù)過(guò)程實(shí)際特征的情況下,由于本文方法能夠事先確保修正協(xié)同業(yè)務(wù)過(guò)程中含有修正前協(xié)同業(yè)務(wù)過(guò)程中所有完整的軌跡,且未引入隱藏軌跡,從而使得本文方法可以對(duì)協(xié)同業(yè)務(wù)過(guò)程進(jìn)行更加有效的修正,并且能夠極大地縮短修正所耗費(fèi)的時(shí)間.

6 相關(guān)工作

目前,針對(duì)協(xié)同業(yè)務(wù)過(guò)程的正確性分析方法可分為兩類:正確性檢測(cè)方法和正確性修正方法.下面對(duì)這兩類方法中的一些典型文獻(xiàn)進(jìn)行介紹和分析.

6.1 正確性檢測(cè)方法

國(guó)內(nèi)外研究者針對(duì)協(xié)同業(yè)務(wù)過(guò)程的正確性檢測(cè)方法開(kāi)展了大量的研究.歸納起來(lái),這些方法可分為3 類:基于Petri 網(wǎng)的檢測(cè)方法、基于進(jìn)程代數(shù)的檢測(cè)方法及基于自動(dòng)機(jī)的檢測(cè)方法.

以傳統(tǒng)的組織內(nèi)業(yè)務(wù)過(guò)程建模方法為基礎(chǔ),文獻(xiàn)[9]較早地在國(guó)際上提出了 IOWF(inter-organizational workflow)用于建?？缃M織業(yè)務(wù)過(guò)程.針對(duì)構(gòu)建跨組織業(yè)務(wù)過(guò)程提出合理性概念用來(lái)定義其正確性,并基于Petri網(wǎng)的可達(dá)圖提出跨組織業(yè)務(wù)過(guò)程正確性檢測(cè)方法.之后,國(guó)內(nèi)外研究者以此為基礎(chǔ)開(kāi)展了大量的研究.如文獻(xiàn)[10]針對(duì)跨部門(mén)業(yè)務(wù)過(guò)程協(xié)同呈現(xiàn)出越來(lái)越復(fù)雜的特點(diǎn),對(duì)WF-net 擴(kuò)展資源和消息等要素以建模參與部門(mén)的業(yè)務(wù)過(guò)程,繼而使用庫(kù)所熔合技術(shù)將資源庫(kù)所和消息庫(kù)所加以熔合從而得到跨部門(mén)協(xié)調(diào)業(yè)務(wù)過(guò)程模型.針對(duì)構(gòu)建跨部門(mén)業(yè)務(wù)過(guò)程,基于合理性定義其正確性并提出驗(yàn)證方法.跨組織工作流網(wǎng)IWF-nets(inter-organizational workflow nets)可以有效地建模協(xié)同業(yè)務(wù)過(guò)程間基于消息的協(xié)作.為了確保協(xié)同業(yè)務(wù)實(shí)施的正確性,文獻(xiàn)[26]引入了兼容性和弱兼容性的概念,并針對(duì)IWF-nets 的網(wǎng)結(jié)構(gòu)提出了用于判定兼容性或弱兼容性的充要條件.針對(duì)公共管理呈現(xiàn)出交互的特征,為確保其正確實(shí)施,文獻(xiàn)[27]首先使用BPMN(business process modeling notation)對(duì)其進(jìn)行描述,之后將其BPMN 模型轉(zhuǎn)換成基于Petri 網(wǎng)的模型,并采用Petri 網(wǎng)的展開(kāi)技術(shù)(unfolding-based technique)對(duì)相關(guān)性質(zhì)(如死鎖等)進(jìn)行驗(yàn)證.為了有效地驗(yàn)證協(xié)同業(yè)務(wù)過(guò)程的行為正確性,文獻(xiàn)[28]首先利用BPMN 建模協(xié)同業(yè)務(wù)過(guò)程,然后將每個(gè)參與組織的流程轉(zhuǎn)換為一類高級(jí)Petri網(wǎng)ECATNets(recursive ECATNets),最后基于庫(kù)所熔合技術(shù)將其組合得到以ECATNets 來(lái)描述的模型.由于該模型的語(yǔ)義被解釋為條件重寫(xiě)邏輯,進(jìn)而可以利用Maude LTL 模型檢測(cè)器對(duì)協(xié)同業(yè)務(wù)過(guò)程的行為正確性性質(zhì)進(jìn)行驗(yàn)證.

基于Pi 演算,文獻(xiàn)[16]較早地提出一種利用進(jìn)程代數(shù)建模跨組織業(yè)務(wù)過(guò)程方法.即利用Pi 演算的并發(fā)算子,將跨組織業(yè)務(wù)過(guò)程建模為一組自治且并發(fā)執(zhí)行的組織內(nèi)子流程的組合,子流程建模為組織內(nèi)本地流程定義和組織間控制約束的組合,并利用工具M(jìn)WB(mobile workbench)驗(yàn)證抽象正確性.為了檢測(cè)協(xié)同業(yè)務(wù)過(guò)程能否正確地協(xié)調(diào),文獻(xiàn)[29]提出了一種針對(duì)多個(gè)業(yè)務(wù)過(guò)程組合驗(yàn)證的概念框架.它將BPMN 建模的協(xié)同業(yè)務(wù)過(guò)程轉(zhuǎn)換以時(shí)間通信順序進(jìn)程CSP+T(communicating sequential processes+time)表示進(jìn)程,之后采用時(shí)序邏輯公式定義期望正確性性質(zhì),并利用模型檢測(cè)方法在工具FDR2(failures-divergences refinement)上自動(dòng)驗(yàn)證正確性性質(zhì)是否滿足.為實(shí)現(xiàn)面向Web 服務(wù)的流程無(wú)縫集成,文獻(xiàn)[30]提出了一種基于遞歸組合代數(shù)的Web 服務(wù)交互流程建模和驗(yàn)證方法.首先利用遞歸組合代數(shù)建模Web 服務(wù)流程交互,并將其轉(zhuǎn)換為遞歸組合交互圖,之后利用遞歸組合規(guī)約語(yǔ)言來(lái)描述需求,并通過(guò)遞歸組合交互圖自動(dòng)地驗(yàn)證需求是否滿足與否.

為了使得多個(gè)基于Web 服務(wù)的業(yè)務(wù)過(guò)程的組合符合用戶定義適配需求,文獻(xiàn)[31]提出一種描述及驗(yàn)證多業(yè)務(wù)過(guò)程間行為適配的方法.它采用LTS 描述業(yè)務(wù)過(guò)程及適配器,進(jìn)而將業(yè)務(wù)過(guò)程與適配器組合來(lái)檢測(cè)其是否相容以判斷多業(yè)務(wù)過(guò)程的組合是否符合用戶定義適配的需求.互操作是業(yè)務(wù)協(xié)同正確實(shí)施須具備的先決條件,為確保每個(gè)參與組織的互操作是否符合規(guī)定的需求,文獻(xiàn)[32]首先使用BPMN 來(lái)描述協(xié)同業(yè)務(wù)過(guò)程,之后將其BPMN 模型轉(zhuǎn)換成模型檢測(cè)工具UPPAAL 中的時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)(timed automata network,簡(jiǎn)稱TAN),并采用時(shí)序邏輯TCTL(time computation tree logic)描述互操作需求,從而實(shí)現(xiàn)互操作自動(dòng)檢測(cè).特別地,BPMN 模型中每個(gè)參與組織業(yè)務(wù)過(guò)程在TAN 中對(duì)應(yīng)一個(gè)時(shí)間自動(dòng)機(jī)(timed automata,簡(jiǎn)稱TA),這些TA 并發(fā)組合構(gòu)成了TAN,即協(xié)同業(yè)務(wù)過(guò)程.在后續(xù)工作中,為了更加有效地存儲(chǔ)和描述互操作需求,文獻(xiàn)[33]首先提出了一種領(lǐng)域描述語(yǔ)言用來(lái)描述互操作需求,繼而將描述需求自動(dòng)轉(zhuǎn)換為時(shí)序邏輯TCTL,并采用TAN 建模協(xié)同業(yè)務(wù)過(guò)程.通過(guò)UPPAAL 實(shí)現(xiàn)互操作需求的自動(dòng)驗(yàn)證.

上面提出的正確性檢測(cè)方法通常具有檢測(cè)過(guò)程自動(dòng)化,不需要人工干預(yù),且在檢測(cè)失敗時(shí)能夠給出診斷信息,便于業(yè)務(wù)設(shè)計(jì)人員發(fā)現(xiàn)并修正錯(cuò)誤.但其不足是,若協(xié)同業(yè)務(wù)過(guò)程中存在多處不正確,則需要經(jīng)過(guò)多次檢測(cè),且在每次檢測(cè)后都需要對(duì)協(xié)同業(yè)務(wù)過(guò)程重新調(diào)整.這種設(shè)計(jì)、驗(yàn)證、分析及糾錯(cuò)的過(guò)程使得協(xié)同業(yè)務(wù)過(guò)程的正確性分析變得復(fù)雜且耗時(shí).

6.2 正確性修正方法

相比正確性檢測(cè)方法,針對(duì)業(yè)務(wù)過(guò)程正確性修正方法是較新的課題,相關(guān)研究工作較少.文獻(xiàn)[11,12]針對(duì)以Artifact 為中心的業(yè)務(wù)過(guò)程提出一種正確性保持的設(shè)計(jì)方法.它首先采用Petri 網(wǎng)建模以Artifact 為中心的業(yè)務(wù)過(guò)程,之后以合規(guī)性和弱合理定義其正確性,最后將業(yè)務(wù)過(guò)程與正確性合成以自動(dòng)構(gòu)建具有正確性的業(yè)務(wù)過(guò)程.文獻(xiàn)[34]采用開(kāi)放工作流網(wǎng)oWFN(open workflow nets)建?？缃M織環(huán)境下的業(yè)務(wù)過(guò)程,利用CTL 公式定義期望正確性性質(zhì),根據(jù)以CTL 公式定義性質(zhì)對(duì)業(yè)務(wù)過(guò)程內(nèi)部結(jié)構(gòu)進(jìn)行修改來(lái)構(gòu)建跨組織環(huán)境下具有正確性的業(yè)務(wù)過(guò)程.然而,上面提出的正確性修正方法均面向組織內(nèi)的單個(gè)業(yè)務(wù)過(guò)程.由于協(xié)同業(yè)務(wù)過(guò)程具有自治性、分布性及涉及多個(gè)業(yè)務(wù)過(guò)程間的同步或異步交互,因此上面提出的方法不適用于跨組織環(huán)境下的協(xié)同業(yè)務(wù)過(guò)程.

近年來(lái),面向軌跡的業(yè)務(wù)過(guò)程修正方法引起一些學(xué)者的關(guān)注.文獻(xiàn)[14]首次在國(guó)際上提出此類方法.首先利用已有的一致性檢測(cè)來(lái)發(fā)現(xiàn)過(guò)程模型與軌跡間差異,并將體現(xiàn)這些差異的軌跡從原軌跡中分離出來(lái),以子軌跡來(lái)加以表示.針對(duì)這些子軌跡,構(gòu)建其對(duì)應(yīng)子結(jié)構(gòu)并將其添加至原業(yè)務(wù)過(guò)程中,從而完成業(yè)務(wù)過(guò)程的修正.隨后,文獻(xiàn)[15]對(duì)文獻(xiàn)[14]的工作進(jìn)行了一些改進(jìn),即針對(duì)一致性檢測(cè)中發(fā)現(xiàn)的循環(huán)結(jié)構(gòu),構(gòu)建其對(duì)應(yīng)的子過(guò)程并將其添加至修正模型中.文獻(xiàn)[35]提出的修正方法沿用了文獻(xiàn)[14,15]的思路.針對(duì)工作流模型,首先利用監(jiān)控矩陣刻畫(huà)實(shí)際工作流模型足跡,通過(guò)比較工作流模型的軌跡與足跡間的差異,提出4 種用于修正的工作流模型算法.我們課題組最近的工作[13]是結(jié)合Petri 網(wǎng)和過(guò)程挖掘的相關(guān)理論,提出一種針對(duì)協(xié)同業(yè)務(wù)過(guò)程的修正方法.該方法首先獲取部分正確協(xié)同業(yè)務(wù)過(guò)程中所有完整的軌跡,之后利用α算法從這些完整的軌跡構(gòu)建相容協(xié)同業(yè)務(wù)過(guò)程,最后通過(guò)設(shè)置協(xié)同業(yè)務(wù)過(guò)程與業(yè)務(wù)過(guò)程間的任務(wù)執(zhí)行同步關(guān)系以協(xié)調(diào)業(yè)務(wù)過(guò)程的正確運(yùn)行.然而,利用上述方法建立的修正業(yè)務(wù)過(guò)程仍是集中式的,也存在修正前協(xié)同業(yè)務(wù)過(guò)程中完整軌跡可能會(huì)丟失和修正協(xié)同業(yè)務(wù)過(guò)程中可能會(huì)引入隱藏軌跡等問(wèn)題.相較而言,本文方法構(gòu)建的協(xié)同業(yè)務(wù)過(guò)程是完全分布式的(即不存在中心流程),它的執(zhí)行能夠正確終止且與修正前協(xié)同業(yè)務(wù)過(guò)程中含有的所有完整軌跡相一致.

面向Web 服務(wù)流程的自動(dòng)組合方法也是與協(xié)同業(yè)務(wù)過(guò)程正確性修正比較相關(guān)的工作.文獻(xiàn)[36]首先裁剪合理性定義正確性(即相容性),針對(duì)部分相容Web 服務(wù)流程采用Petri 網(wǎng)建模每個(gè)服務(wù)的流程,然后將其進(jìn)行組合并分析其相容性.若分析結(jié)果部分相容,則產(chǎn)生適配器將來(lái)協(xié)調(diào)服務(wù)流程,使之前部分相容的服務(wù)流程轉(zhuǎn)換為完整相容,且未改變?cè)蟹?wù)流程的內(nèi)部結(jié)構(gòu).為了應(yīng)對(duì)服務(wù)流程間存在時(shí)序約束及消息匹配問(wèn)題,文獻(xiàn)[37]首先采用Petri 網(wǎng)建模每個(gè)服務(wù)的流程,然后根據(jù)消息匹配情況及時(shí)序約束構(gòu)建適配器,從而使得所有服務(wù)的流程與適配器組合執(zhí)行是正確的,以避免出現(xiàn)時(shí)序異常.面向Web 服務(wù)流程組合與通過(guò)傳統(tǒng)業(yè)務(wù)過(guò)程組合建立協(xié)同業(yè)務(wù)過(guò)程的最大區(qū)別是服務(wù)使用者通常沒(méi)有修改第三方服務(wù)的權(quán)限,也不能要求服務(wù)提供者按照自己的需求修改提供的服務(wù).因此,針對(duì)Web 服務(wù)流程自動(dòng)組合通常利用適配器來(lái)實(shí)現(xiàn),而針對(duì)業(yè)務(wù)過(guò)程組合主要是由可信第三方在設(shè)計(jì)階段修改業(yè)務(wù)過(guò)程的內(nèi)部結(jié)構(gòu)來(lái)實(shí)現(xiàn)[36].

7 總結(jié)

在考慮活動(dòng)同步及異步交互的情況下,本文基于完整簡(jiǎn)單路徑提出一種協(xié)同業(yè)務(wù)過(guò)程正確性修正方法.該方法將部分正確的協(xié)同業(yè)務(wù)過(guò)程中所有的完整簡(jiǎn)單路徑合并以構(gòu)建核,通過(guò)協(xié)調(diào)映射來(lái)生成修正業(yè)務(wù)過(guò)程,將修正業(yè)務(wù)過(guò)程并發(fā)組合建立修正協(xié)同業(yè)務(wù)過(guò)程.該方法一方面可確保修正協(xié)同業(yè)務(wù)過(guò)程符合其典型特征(如自治、分布等);另一方面,修正協(xié)同業(yè)務(wù)過(guò)程只含有修正前協(xié)同業(yè)務(wù)過(guò)程中所有完整簡(jiǎn)單路徑對(duì)應(yīng)的軌跡,可避免有效性確認(rèn),提高了修正效率.

未來(lái)工作主要針對(duì)以下3 個(gè)方面的問(wèn)題開(kāi)展研究.

(1)本文定義正確性關(guān)注控制流,而數(shù)據(jù)流也是影響業(yè)務(wù)過(guò)程協(xié)作的一個(gè)重要因素.因此,下一步將提出同時(shí)考慮控制流和數(shù)據(jù)流的協(xié)同業(yè)務(wù)過(guò)程正確性修正方法;

(2)弱合理可歸于一般意義上的正確性[17],而參與組織期望系統(tǒng)功能或特性可能多種多樣.如何在考慮用戶需求層面對(duì)協(xié)同業(yè)務(wù)過(guò)程進(jìn)行修正是值得深入研究的課題;

(3)本文方法在修正中需要首先生成協(xié)同業(yè)務(wù)過(guò)程完整簡(jiǎn)單路徑,然后合成核,最后通過(guò)對(duì)核進(jìn)行協(xié)調(diào)映射生成每個(gè)修正業(yè)務(wù)過(guò)程.在實(shí)際應(yīng)用中,由于受限于協(xié)同業(yè)務(wù)過(guò)程的狀態(tài)空間,本文方法也面臨狀態(tài)空間爆炸的問(wèn)題.然而,本文主要關(guān)注修正方法的有效性(即修正協(xié)同業(yè)務(wù)過(guò)程符合實(shí)際特征及修正前后完整簡(jiǎn)單軌跡保持一致)和效率(即修正耗費(fèi)時(shí)間較短)問(wèn)題.如何避免修正中出現(xiàn)的狀態(tài)空間爆炸問(wèn)題將在未來(lái)工作中著重加以討論.