基于流程抽象的協(xié)同業(yè)務(wù)過程符合性驗(yàn)證

莫 啟，向吉祥，汪煜祺，代 飛，許小龍，齊連永

(1.云南大學(xué) 軟件學(xué)院，云南 昆明 650091；2.云南大學(xué) 云南省軟件工程重點(diǎn)實(shí)驗(yàn)室, 云南 昆明 650091；3.西南林業(yè)大學(xué) 大數(shù)據(jù)與智能工程學(xué)院，云南 昆明 650091；4.南京信息工程大學(xué) 計(jì)算機(jī)與軟件學(xué)院，江蘇 南京 210044；5.曲阜師范大學(xué) 信息科學(xué)與工程學(xué)院，山東 曲阜 273165)

0 引言

隨著企業(yè)信息化程度不斷提高，企業(yè)經(jīng)營模式發(fā)生了重大轉(zhuǎn)變，從獨(dú)立經(jīng)營模式發(fā)展成為跨企業(yè)合作模式[1]。作為一類跨組織的業(yè)務(wù)過程，協(xié)同業(yè)務(wù)過程[2]在企業(yè)協(xié)作中扮演著重要角色。當(dāng)前協(xié)同業(yè)務(wù)過程被廣泛應(yīng)用于各種行業(yè)中，如醫(yī)療[3]，電子商務(wù)[4]和物聯(lián)網(wǎng)[5]。為確保這些行業(yè)應(yīng)用在實(shí)際中良好地實(shí)施，協(xié)同業(yè)務(wù)過程在設(shè)計(jì)階段通常需要滿足如下3類重要性質(zhì)：

(1)正確性[6]為完成既定業(yè)務(wù)目標(biāo)，協(xié)同業(yè)務(wù)過程應(yīng)能夠正確地執(zhí)行完成，且在執(zhí)行過程中未出現(xiàn)死鎖、活鎖和未指定消息接收等。

(2)一致性[7]協(xié)同業(yè)務(wù)過程的執(zhí)行應(yīng)與事先確定的規(guī)約一致。規(guī)約通常指編排，即從全局視角定義業(yè)務(wù)過程間交互，由參與組織協(xié)商確定[7]。

(3)符合性[8-9]協(xié)同業(yè)務(wù)過程面向特定行業(yè)，其執(zhí)行需與應(yīng)用領(lǐng)域的特性相符。應(yīng)用領(lǐng)域特性是指領(lǐng)域約束，通常來自管理、風(fēng)險(xiǎn)及審計(jì)符合性等相關(guān)方面[8-9]。例如，在信貸業(yè)務(wù)過程中，每次貸款完成前需經(jīng)過相關(guān)職能部門的貸款審查，從而保證貸款操作透明合理。

事實(shí)上，上述3類性質(zhì)均可在設(shè)計(jì)階段通過運(yùn)用形式驗(yàn)證技術(shù)予以確保。例如，若需要判斷協(xié)同業(yè)務(wù)過程與規(guī)約間的一致性，則可利用行為等價(jià)理論(如跡等價(jià)等)進(jìn)行判定[7]。由于當(dāng)前驗(yàn)證協(xié)同業(yè)務(wù)過程正確性及一致性的相關(guān)研究較為成熟，本文關(guān)注如何驗(yàn)證協(xié)同業(yè)務(wù)過程與領(lǐng)域約束的符合性。

目前，國內(nèi)外研究者圍繞如何驗(yàn)證協(xié)同業(yè)務(wù)過程符合性做了大量工作，但是這些研究工作的關(guān)注重點(diǎn)仍是符合性驗(yàn)證中符合性管理框架設(shè)計(jì)、符合性語言設(shè)計(jì)及協(xié)同業(yè)務(wù)過程可視化建模等方面[9-10]，并未涉及業(yè)務(wù)過程中內(nèi)部流程細(xì)節(jié)(包括本地活動(dòng)及由這些活動(dòng)形成控制流)處理，這將導(dǎo)致如下3個(gè)方面問題：①建立的協(xié)同業(yè)務(wù)過程是具有協(xié)同功效的全局模型(即由業(yè)務(wù)過程直接組合形成)，因此將參與組織的內(nèi)部流程信息完全暴露給其他組織，與隱私保護(hù)原則相違背[2]；②從外部環(huán)境觀察，協(xié)同業(yè)務(wù)過程行為表現(xiàn)為業(yè)務(wù)過程間活動(dòng)交互，全局模型中內(nèi)部流程細(xì)節(jié)可能會(huì)導(dǎo)致符合性誤判；③由于是在全局模型上驗(yàn)證領(lǐng)域約束是否相符，導(dǎo)致其驗(yàn)證效率低下。

為此，基于流程抽象(即將業(yè)務(wù)過程中內(nèi)部流程細(xì)節(jié)抽象掉，只保留外部可見部分)，本文提出一種協(xié)同業(yè)務(wù)過程行為符合性驗(yàn)證方法。該方法隱藏所有參與組織的業(yè)務(wù)過程中內(nèi)部流程細(xì)節(jié)，能夠有效地避免暴露組織內(nèi)部流程信息、確保符合性驗(yàn)證結(jié)果的正確性及提高形式驗(yàn)證效率。本文的主要貢獻(xiàn)如下：

(1)基于流程抽象提出一種協(xié)同業(yè)務(wù)過程行為符合性驗(yàn)證方法。即先基于弱軌跡等價(jià)[11]將業(yè)務(wù)過程中含有的內(nèi)部流程細(xì)節(jié)全部移除，得到抽象業(yè)務(wù)過程，并將其并發(fā)組合得到抽象協(xié)同業(yè)務(wù)過程；之后采用線性時(shí)序邏輯(Linear time Temporal Logic，LTL)描述領(lǐng)域約束；最后借助模型檢測技術(shù)自動(dòng)地驗(yàn)證抽象協(xié)同業(yè)務(wù)過程與領(lǐng)域約束是否相符。

(2)理論上證明了給定領(lǐng)域約束在協(xié)同業(yè)務(wù)過程和抽象協(xié)同業(yè)務(wù)過程上的驗(yàn)證結(jié)果一致。這可避免暴露組織內(nèi)部流程信息、確保符合性驗(yàn)證結(jié)果的正確性及提高形式驗(yàn)證效率。

(3)采用實(shí)際協(xié)同業(yè)務(wù)過程集闡述本文提出方法的有效性，并對(duì)所提方法的分析效率進(jìn)行定量評(píng)價(jià)。

1 方法概覽

本文關(guān)注驗(yàn)證協(xié)同業(yè)務(wù)過程與領(lǐng)域約束間的符合性，提出的方法框架如圖1所示，具體包含如下兩個(gè)階段：

(1)建模階段 首先利用標(biāo)號(hào)遷移系統(tǒng)[8]，參與組織建模各自的業(yè)務(wù)過程，然后并發(fā)組合形成協(xié)同業(yè)務(wù)過程；之后為了確定期望的領(lǐng)域約束，參與組織間進(jìn)行協(xié)商并利用符合性語言(Compliance Request Language, CRL)[19]描述。特別地，直接采用命題邏輯或時(shí)序邏輯定義領(lǐng)域約束易于出錯(cuò)且復(fù)雜，而符合性語言能夠以模式方式描述領(lǐng)域約束，對(duì)于參與組織易于使用。

(2)分析階段 首先抽象業(yè)務(wù)過程中內(nèi)部流程細(xì)節(jié)，得到抽象業(yè)務(wù)過程；然后并發(fā)組合這些抽象業(yè)務(wù)過程以建立抽象協(xié)同業(yè)務(wù)過程。上述操作為本文所提方法的核心。之后將符合性語言描述的領(lǐng)域約束映射為以LTL公式表示的性質(zhì)，其中具體映射規(guī)則由符合性語言CRL規(guī)定。最后將抽象協(xié)同業(yè)務(wù)過程轉(zhuǎn)換為PAT(process analysis toolkit)[注]http://pat.comp.nus.edu.sg/。中以CSP#(communicating sequential programs)[12]描述進(jìn)程，并將產(chǎn)生的CSP#進(jìn)程規(guī)約和以LTL公式表示的領(lǐng)域約束作為模型檢測器PAT的輸入，根據(jù)檢測結(jié)果能夠有效地判斷協(xié)同業(yè)務(wù)過程是否滿足期望的領(lǐng)域約束。

具體符合性檢測由PAT自動(dòng)完成，不需要人工干預(yù)。更重要的是，對(duì)協(xié)同業(yè)務(wù)過程進(jìn)行符合性驗(yàn)證可轉(zhuǎn)換為對(duì)抽象協(xié)同業(yè)務(wù)過程驗(yàn)證(它們的驗(yàn)證結(jié)果一致)，從而可避免暴露內(nèi)部流程信息且提高符合性驗(yàn)證效率(抽象協(xié)同業(yè)務(wù)過程狀態(tài)空間極大地壓縮)。同時(shí)，由于屏蔽了內(nèi)部流程細(xì)節(jié)對(duì)符合性驗(yàn)證的影響，可避免誤判。

2 協(xié)同業(yè)務(wù)過程及領(lǐng)域約束建模

根據(jù)圖1所示框架，參與組織首先需對(duì)協(xié)同業(yè)務(wù)過程及領(lǐng)域約束進(jìn)行建模，下面進(jìn)行詳細(xì)闡述。

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

沿用項(xiàng)目組前期工作[13]，在對(duì)業(yè)務(wù)過程建模時(shí)，本文也采用標(biāo)號(hào)遷移系統(tǒng)對(duì)其進(jìn)行描述，然后將業(yè)務(wù)過程并發(fā)組合，以構(gòu)建協(xié)同業(yè)務(wù)過程。

本質(zhì)上，一個(gè)參與組織的內(nèi)部業(yè)務(wù)邏輯(即外部環(huán)境不可見部分)與其外部環(huán)境(即其他參與組織的業(yè)務(wù)過程)的交互[2,14]可以利用一個(gè)業(yè)務(wù)過程進(jìn)行描述，其形式定義如下。

定義1業(yè)務(wù)過程[13]。 業(yè)務(wù)過程是一個(gè)遷移系統(tǒng)N=(S,s0,ψ,γ,Δ)，其中：

(1)S為有窮狀態(tài)集合；

(2)s0∈S是初始狀態(tài)；

(3)ψ?S是終止?fàn)顟B(tài)集；

(4)γ=γl∪γi是活動(dòng)集，γl和γi分別為本地活動(dòng)和交互活動(dòng)集。特別地，γi=γs∪γr，其中：γs和γr分別為異步發(fā)送和接收活動(dòng)集合；

(5)Δ?S×γ×S是刻畫活動(dòng)間控制流的遷移關(guān)系。

為了方便，將一條遷移(p,a,q)∈Δ記為p[a>q。另外，?a∈γs，其形如!m，m是其關(guān)聯(lián)發(fā)送消息。類似地，?a∈γr，其形如?m，m是其關(guān)聯(lián)接收消息。

利用文獻(xiàn)[13]中提出的并發(fā)算子，多個(gè)業(yè)務(wù)過程可組合構(gòu)建為一個(gè)協(xié)同業(yè)務(wù)過程。

協(xié)同業(yè)務(wù)過程的狀態(tài)表示為格局，其形式定義如下。

特別地，將N的初始格局表示為c0=，其中：?i∈[1，…，n]；s0i為Ni的初始狀態(tài)；M=NIL表示N在執(zhí)行前不存在消息；N的終止格局表示為ce=，其中：?i∈[1，…，n]，sei為Ni的一個(gè)終止?fàn)顟B(tài)；M=NIL表示N在執(zhí)行后產(chǎn)生的消息均被接收。

為了對(duì)格局中的狀態(tài)和消息進(jìn)行重置，定義函數(shù)如下：

協(xié)同業(yè)務(wù)過程的執(zhí)行由其點(diǎn)火規(guī)則確定，形式定義如下。

(1)若a∈γl，則c[a>c′，當(dāng)且僅當(dāng)si[a>sj∧c′=c[si←sj]；

(2)若a=!m，則c[a>c′，當(dāng)且僅當(dāng)si[a>si′∧M′=M+ {m}∧c′=c[M←M′]∧c′=c[si←sj]；

(3)若a=?m，則c[a>c′，當(dāng)且僅當(dāng)si[a>sj∧M(m)≠0∧M′(m)=M(m) - {m}∧c′=c[si←sj]。

基于點(diǎn)火規(guī)則，協(xié)同業(yè)務(wù)過程行為可形式化為路徑。

定義7軌跡[13]。 給定路徑r=c0[a1>c1…cn-1[an>cn…，則其跡可定義為a0∧a1…an-1∧an∧…。

特別地，若將a0∧a1…an-1∧an∧…中本地活動(dòng)全部移除，則得到r交互跡，記為χ(a0∧a1…an-1∧an∧…)。本文交互跡主要用于避免本地活動(dòng)對(duì)符合性驗(yàn)證造成影響。另外，若格局c1能夠通過執(zhí)行跡σ遷移至格局c2，則記為c1[σ>c2。

定義8路徑一致。給定兩條有窮路徑ru=cu0[a1>cu1…cu(n-1)[an>cun和rv=cv0[b1>cv1…cv(n-1)[bn>cvn，ru和rv一致，記為ru=rv，當(dāng)且僅當(dāng)ru和rv的交互軌跡相同。

在實(shí)際應(yīng)用中，協(xié)同業(yè)務(wù)過程進(jìn)行符合性驗(yàn)證前需滿足正確性[8]。故本文后續(xù)討論中均默認(rèn)協(xié)同業(yè)務(wù)過程是正確的。目前，為了驗(yàn)證協(xié)同業(yè)務(wù)過程的正確性，研究者提出多種標(biāo)準(zhǔn)，其中應(yīng)用最為廣泛的是合理性[6]及其變體(如弱合理[15]等)。由于合理性主要用于定義組織內(nèi)業(yè)務(wù)過程正確性且較為嚴(yán)格[15]，本文利用弱合理性定義協(xié)同業(yè)務(wù)過程正確性。

定義9弱合理。給定協(xié)同業(yè)務(wù)過程N(yùn)=(S,s0,ψ,γ, Δ)，則N是弱合理的，當(dāng)且僅當(dāng)對(duì)于從s0可達(dá)的任意格局c，存在軌跡σ和一個(gè)終止格局ce∈ψ，使得c[σ]>ce。

定義9本質(zhì)上要求從初始格局可達(dá)的任意格局都能夠到達(dá)終止格局，一方面，它可以確保每個(gè)業(yè)務(wù)流程都能達(dá)到終止?fàn)顟B(tài)，并避免協(xié)同業(yè)務(wù)過程中可能存在的死鎖和活鎖等情形；另一方面，終止格局要求每個(gè)業(yè)務(wù)流程的消息隊(duì)列為空，從而確?？梢院侠淼亟邮諈f(xié)同中生成的所有消息。

2.2 領(lǐng)域約束建模

協(xié)同業(yè)務(wù)過程通常面向特定行業(yè)，其執(zhí)行受到應(yīng)用領(lǐng)域內(nèi)的相關(guān)特征(如行業(yè)規(guī)范、制度規(guī)范及法律法規(guī)等)約束[8-9]。歸納起來，領(lǐng)域約束大致可分為必選領(lǐng)域約束和可選領(lǐng)域約束兩類[16]。前者指協(xié)同業(yè)務(wù)過程在執(zhí)行時(shí)必須滿足的領(lǐng)域約束；而后者則是指協(xié)同業(yè)務(wù)過程在執(zhí)行時(shí)可選的領(lǐng)域約束，不要求必須滿足。例如，在投稿業(yè)務(wù)過程中，若作者投稿被拒，則編輯部(或會(huì)務(wù)組)應(yīng)向作者返回退稿理由，這可視為一個(gè)必選領(lǐng)域約束；而在在線購買中，客戶在購買商品之后，可以自愿地添加該商品評(píng)論，這就可視為一個(gè)可選領(lǐng)域約束。

按形式基礎(chǔ)，現(xiàn)有的研究中通常采用命題邏輯或時(shí)序邏輯描述領(lǐng)域約束[8-9]。相比命題邏輯，時(shí)序邏輯中添加一些額外時(shí)序操作符(如終將時(shí)態(tài)算子◇等)，表達(dá)能力更加強(qiáng)大。因此，本文采用LTL來描述領(lǐng)域約束。

用來描述領(lǐng)域約束的LTL公式是定義在交互跡上的一個(gè)表達(dá)式。

定義10領(lǐng)域約束。 領(lǐng)域約束是一個(gè)LTL公式，采用BNF定義如下：

?::=1 |a(a∈AP) | ?1∧?2| ┑? | ○? | ?1∪?2。

其中：AP為原子領(lǐng)域約束(即表示為交互活動(dòng))集合；以LTL公式表示領(lǐng)域約束用來斷言協(xié)同業(yè)務(wù)過程中的交互跡所滿足的性質(zhì)。對(duì)于任意交互跡σ，σ滿足LTL公式?解釋如下：

σ|=1；

σ|=a?a0=a(a0為σ中第一個(gè)活動(dòng))；

σ|=?1∧?2?σ|=?1∧σ|=?2；

σ|=┐??┐(σ|=?)；

σ|=○??σ1|=?;

σ|=?1∪?2??i≥0:σi|=?2∧?j∈[0,i-1]:σj|=?1。

其中：終將時(shí)態(tài)算子◇和總是時(shí)態(tài)算子□可由上述時(shí)態(tài)算子推出，即◇??1∪?；□φ?┐◇┐?。

特別地，本文中僅考慮涉及協(xié)同業(yè)務(wù)過程行為的領(lǐng)域約束，而包含其他要素(如資源、數(shù)據(jù)等)的領(lǐng)域約束將在下一步工作中討論。從外部視角觀察，協(xié)同業(yè)務(wù)過程的行為表現(xiàn)為活動(dòng)間交互。因此，本文將原子領(lǐng)域約束定義為一個(gè)交互活動(dòng)。更重要的是，基于交互跡定義領(lǐng)域約束可以避免符合性驗(yàn)證中的誤判。例如，若存在某條軌跡σ=a0∧a1∧a2，其中：a0是本地活動(dòng)，而a1和a2是交互活動(dòng)。從外部視角觀察，由于a0不可見，故領(lǐng)域約束?1=a1及?2=a1∪a2滿足，即驗(yàn)證結(jié)果均為true。但是，若直接利用σ進(jìn)行驗(yàn)證，則?1及?2的驗(yàn)證結(jié)果均為false。由于消息跡將σ中的本地活動(dòng)a0移除，驗(yàn)證結(jié)果與觀察到的驗(yàn)證結(jié)果一致。

實(shí)際中的領(lǐng)域約束通常采用符合性語言[8-9]描述。本質(zhì)上，符合性語言是由一些常見模式(如存在模式、次序模式等，用自然語言描述)轉(zhuǎn)換成時(shí)序邏輯公式的映射組成。目前，這方面研究工作較為成熟。為了避免重復(fù)工作，本文利用文獻(xiàn)[9]中的符合性語言CRL來描述領(lǐng)域約束。例如，對(duì)于網(wǎng)店店主不允許客戶添加商品評(píng)論這類存在性領(lǐng)域需求，則可用CRL中isAbsent模式描述，映射LTL公式為□┐(comment)。有關(guān)CRL的詳細(xì)內(nèi)容可以參考文獻(xiàn)[9]。

基于領(lǐng)域約束定義，下面定義領(lǐng)域約束在協(xié)同業(yè)務(wù)過程上的滿足性。

定義11領(lǐng)域約束滿足。 給定協(xié)同業(yè)務(wù)過程N(yùn)，稱N滿足以LTL公式?表示領(lǐng)域約束，記為N|=?，當(dāng)且僅當(dāng)對(duì)于N中任意路徑對(duì)應(yīng)的交互跡σ，N|=?成立。

需說明的是：在跨組織環(huán)境下，領(lǐng)域約束通常通過參與組織之間的協(xié)商得到，并且它們的獲取是一個(gè)循環(huán)迭代的過程。在文獻(xiàn)[9]中描述了如何迭代改進(jìn)獲得領(lǐng)域約束。另一方面，參與組織通過協(xié)商建立的領(lǐng)域約束之間可能存在自然的不一致性，歸納起來可以分為領(lǐng)域約束冗余和領(lǐng)域約束沖突兩類[17]。前者是指一個(gè)領(lǐng)域約束的存在，可以從其他領(lǐng)域約束中推導(dǎo)得出，因此不必分析該領(lǐng)域約束；后者是指存在兩個(gè)領(lǐng)域約束，而協(xié)同業(yè)務(wù)過程不能同時(shí)滿足這兩個(gè)領(lǐng)域約束，因此對(duì)其進(jìn)行分析是徒勞的。文獻(xiàn)[17]在相關(guān)的LTL理論的基礎(chǔ)上詳細(xì)研究了如何消除這兩種類型的不一致。限于篇幅，本文后續(xù)討論中的領(lǐng)域約束均指無冗余和無沖突領(lǐng)域約束。

3 符合性驗(yàn)證

在參與組織定義業(yè)務(wù)過程及利用CRL描述領(lǐng)域約束之后，下面討論符合性驗(yàn)證。如圖1所示框架，符合性驗(yàn)證的核心是將業(yè)務(wù)過程抽象為抽象業(yè)務(wù)過程及構(gòu)建抽象協(xié)同業(yè)務(wù)過程。

本質(zhì)上，抽象業(yè)務(wù)過程對(duì)應(yīng)組織的公共過程，它從單個(gè)組織視角描述其與外部環(huán)境的交互及交互次序[2,14]。相比抽象業(yè)務(wù)過程，符合定義1的業(yè)務(wù)過程中還含有外部環(huán)境不可見的業(yè)務(wù)邏輯，即本地任務(wù)及由這些任務(wù)形成的控制流。因此，可以通過將業(yè)務(wù)過程中本地活動(dòng)及相關(guān)控制流移除后形成抽象業(yè)務(wù)過程。下面先定義隱藏操作，用于將業(yè)務(wù)過程中本地活動(dòng)置為外部不可見活動(dòng)。

定義12隱藏[13]。 給定業(yè)務(wù)過程N(yùn)=(S,s0,ψ,γ,Δ)，則對(duì)N進(jìn)行隱藏后得到的隱藏業(yè)務(wù)過程為Nh=(Sh,sh0,ψh,γh,Δh)，其中：

(1)Sh=S；

(2)sh0=s0；

(3)ψh=ψ；

(4)γh?{τ}∪γ；

(5)?(p,a,q)∈Δ，若a∈γi，則(p,a,q)∈Δh，否則τ-遷移關(guān)系(p,τ,q)∈Δh。

由定義12可以看出，隱藏主要是為了重置BP中的狀態(tài)轉(zhuǎn)移關(guān)系，即如果狀態(tài)轉(zhuǎn)移關(guān)系在N中是交互活動(dòng)，它將在重置的狀態(tài)遷移關(guān)系中保持不變。同時(shí)，將N中本地活動(dòng)設(shè)置為外部不可見活動(dòng)τ，形成τ-遷移關(guān)系。

在獲得隱藏業(yè)務(wù)過程之后，還需將其中所有τ-遷移關(guān)系全部移除。目前，研究人員已經(jīng)提出了多種行為最小化技術(shù)[11]，如軌跡最小化，分支最小化和互模擬最小化等。由于本文的重點(diǎn)是協(xié)同業(yè)務(wù)過程路徑和域約束的一致性，弱軌跡等效性[11]被用于最小化隱藏業(yè)務(wù)流程。具體的最小化過程見算法1。

算法1生成抽象業(yè)務(wù)過程。

輸入: 隱藏業(yè)務(wù)過程N(yùn)=(S, s0, ψ, γ, Δ);

輸出: 抽象業(yè)務(wù)過程N(yùn)a=(Sa, sa0, ψa, γa, Δa)。

1. S0=τ-closure({s0});

2. 置S0為未訪問，并將其添加至Q;

3. whileQ≠φthen

4. 取Q中未訪問的狀態(tài)Su;

5. forN中每一個(gè)交互活動(dòng)ado

6. Sv=τ-closure(tran(Su, a));

7. if Sv?Q then

8. 置Sv為未訪問，并將其添加至Q;

9. 把(Su, a, Sv)加入Δa;

10. else

11. 把(Su, a, Sv)加入Δa;

12. end if

13. end for

14. end while

15. 把S0作為初始狀態(tài)sa0;

16. 把包含ψ的狀態(tài)Se加入ψa;

17. 把Sa和γa分別設(shè)為Q和γ;

18. return Na;

算法1中，給定業(yè)務(wù)過程N(yùn)中狀態(tài)集D∈S,函數(shù)τ-closure(D)定義從D中任意狀態(tài)出發(fā)，通過標(biāo)記為τ的路徑到達(dá)的狀態(tài)集；而函數(shù)tran(D,a)定義從D中任意狀態(tài)出發(fā)，經(jīng)過活動(dòng)a轉(zhuǎn)換到達(dá)的狀態(tài)集。

經(jīng)算法1構(gòu)建抽象業(yè)務(wù)過程也符合定義1中業(yè)務(wù)過程定義。因此，可利用并發(fā)操作符將抽象業(yè)務(wù)過程集組合，得到抽象協(xié)同業(yè)務(wù)過程。

由于模型驗(yàn)證技術(shù)不需要在檢測過程中進(jìn)行人工干預(yù)，并且可以提供反例信息以在驗(yàn)證失敗時(shí)糾正錯(cuò)誤，在構(gòu)建完成抽象協(xié)同業(yè)務(wù)過程后，本文利用模型檢測技術(shù)對(duì)其進(jìn)行符合性驗(yàn)證。目前，較為著名的模型驗(yàn)證工具有NuSMV[注]http://nusmv.fbk.eu/。、PAT及SPIN[注]http://spinroot.com/spin/whatispin.html。等。PAT具有用戶友好界面、內(nèi)置高效LTL檢測器，以及可方便地將LTS轉(zhuǎn)換為PAT輸入語言CSP#等特點(diǎn)，因此本文采用PAT作為符合性自動(dòng)驗(yàn)證工具。

由于CSP#能夠良好地以文本方式描述LTS，且為避免在符合性驗(yàn)證前，顯式地構(gòu)建協(xié)同業(yè)務(wù)過程狀態(tài)空間從而實(shí)現(xiàn)On-the-fly驗(yàn)證，本文提出如表1所示的映射規(guī)則，用于將協(xié)同業(yè)務(wù)過程映射為CSP#進(jìn)程。其核心思想是將協(xié)作中產(chǎn)生的每條消息映射為整形變量，每個(gè)業(yè)務(wù)過程映射為CSP#進(jìn)程及協(xié)同業(yè)務(wù)過程映射為所有業(yè)務(wù)過程進(jìn)程并發(fā)組合，以模擬協(xié)同業(yè)務(wù)過程點(diǎn)火規(guī)則的執(zhí)行。

表1 協(xié)同業(yè)務(wù)過程到CSP#進(jìn)程轉(zhuǎn)換

針對(duì)表1給出的映射規(guī)則，具體說明如下：

針對(duì)協(xié)同業(yè)務(wù)過程中每條消息msg，msg被映射為初值為0的整形變量，表示開始時(shí)msg不存在；

每個(gè)業(yè)務(wù)過程BPi用其初始狀態(tài)標(biāo)識(shí)進(jìn)程表示，且BPi中每個(gè)狀態(tài)均對(duì)應(yīng)一個(gè)進(jìn)程；

對(duì)于每個(gè)業(yè)務(wù)過程中任意遷移，根據(jù)觸發(fā)活動(dòng)不同，將其分為3類：①若觸發(fā)活動(dòng)是異步發(fā)送活動(dòng)，則在該遷移發(fā)生后將消息msg加1(即產(chǎn)生消息msg)，并在執(zhí)行完發(fā)送后遷移至后續(xù)狀態(tài)對(duì)應(yīng)進(jìn)程；②若觸發(fā)活動(dòng)是異步接收活動(dòng)，則在該遷移發(fā)生前需判斷消息msg是否存在。若存在(即msg>0)則執(zhí)行接收，且在接收后將消息msg減1(即消耗消息msg)，并遷移至后續(xù)狀態(tài)對(duì)應(yīng)進(jìn)程；③若觸發(fā)活動(dòng)是本地活動(dòng)，則直接遷移至后續(xù)狀態(tài)對(duì)應(yīng)進(jìn)程。這與定義5中描述協(xié)同業(yè)務(wù)過程點(diǎn)火規(guī)則一致；

最后，協(xié)同業(yè)務(wù)過程映射為每個(gè)業(yè)務(wù)過程對(duì)應(yīng)進(jìn)程的并發(fā)組合。特別地，由于業(yè)務(wù)過程間只涉及異步消息通信，采用CSP#中的交錯(cuò)算子“|||”組合業(yè)務(wù)過程進(jìn)程。

由表1所示映射規(guī)則，在將抽象協(xié)同業(yè)務(wù)過程轉(zhuǎn)換為CSP#進(jìn)程后，則可將以CSP#進(jìn)程表示的抽象協(xié)同業(yè)務(wù)過程和以LTL公式表示的領(lǐng)域約束(領(lǐng)域約束至LTL公式映射可參考CRL的具體內(nèi)容[9])分別作為PAT的模型和性質(zhì)輸入，PAT(其集成了基于LTL公式的模型檢測引擎)將自動(dòng)完成一致性檢測。根據(jù)PAT檢測的結(jié)果，可以判斷協(xié)同業(yè)務(wù)過程是否符合領(lǐng)域約束。如果存在任何差異，則可以根據(jù)反例中的信息找到并糾正協(xié)同業(yè)務(wù)過程中的問題。

4 有效性分析

由于本文默認(rèn)協(xié)同業(yè)務(wù)過程在符合性驗(yàn)證之前具備正確性，基于協(xié)同業(yè)務(wù)過程構(gòu)建抽象協(xié)同業(yè)務(wù)過程也具有正確性。為證明該結(jié)論，下面先給出定理1和引理1。

定理1給定隱藏業(yè)務(wù)過程N(yùn)=(S,s0,ψ, γ, Δ)，經(jīng)算法1生成抽象業(yè)務(wù)過程為Na=(Sa,sa0,ψa, γa, Δa)，則N與Na滿足弱軌跡等價(jià)。

證明：分兩種情況進(jìn)行討論：

(1)若N中無τ-遷移關(guān)系，則由算法1中構(gòu)造的Na可知：

1)對(duì)于任意sa∈Sa，sa=2S；

2)對(duì)于任意狀態(tài)遷移關(guān)系(sa-1,a,sa)={(su-1,a,su) |su-1∈S∧su∈S∧su-1∈sa-1∧su∈sa}；

3)sa0=s0；

4)sae∈ψa為包含ψ的狀態(tài)。

根據(jù)上述條件可推出，對(duì)于軌跡σ∈traces(s0)，存在唯一對(duì)應(yīng)軌跡σ∈traces(sa0)，故N與Na滿足弱軌跡等價(jià)。其中：traces(s)表示從狀態(tài)s出發(fā)可達(dá)任意軌跡。

(2)若N中有τ-遷移關(guān)系，則由算法1中構(gòu)造的Na可知：

1)對(duì)于任意sa∈Sa，sa=2S；

2)對(duì)于任意狀態(tài)遷移關(guān)系(sa-1,a,sa)={(su-1,a,su) |su-1∈S∧su∈S∧su-1∈sa-1∧su∈sa}；

3)sa0=s0；

4)sae∈ψa為包含ψ的狀態(tài)。

根據(jù)上述條件可推出，對(duì)于任意軌跡σ1∈trace(s0)，則存在唯一軌跡σ2∈trace(sa0)，滿足σ1的交互跡與σ2相同，故N與Na滿足弱軌跡等價(jià)。

證畢。

證明：要證明Nt是正確的，則只需明確Nai能夠正確執(zhí)行，且執(zhí)行交互活動(dòng)序列與BPi一致即可。由N是正確的可知，對(duì)于從Ni初始狀態(tài)s0可達(dá)的任意狀態(tài)s，終止?fàn)顟B(tài)sf可以達(dá)到，即存在軌跡σ1和σ2，使得s0[σ1>s[σ2>sf。由定理1可知，Ni與Nai滿足弱軌跡等價(jià)，則可推出sa1[χ(σ1)>sa[χ(σ2)>saf。由于saf是Ni終止?fàn)顟B(tài)，則根據(jù)算法1可知sf∈saf，推出saf是Nai的終止?fàn)顟B(tài)。根據(jù)定義9推出Nt具有正確性。

證畢。

證明：Na可看成是對(duì)N做n次替換后生成，即每次用Nai替換Ni(i∈[1,…,n])。根據(jù)引理1，每次替換后產(chǎn)生的協(xié)同業(yè)務(wù)過程也具有正確性，則經(jīng)過n次替換后生成抽象協(xié)同業(yè)務(wù)過程為Na也是正確的。

證畢。

之后，證明給定任意符合性約束?，其在協(xié)同業(yè)務(wù)過程和對(duì)應(yīng)抽象協(xié)同業(yè)務(wù)過程上的驗(yàn)證結(jié)果一致。下面先給出引理2和引理3。

證明：采用反證法證明。設(shè)Nt與N不是弱軌跡等價(jià)，則根據(jù)弱軌跡等價(jià)定義可知，存在兩個(gè)格局ct∈C(Nt)和c∈C(N)違反弱軌跡等價(jià)，其中函數(shù)C(N)定義N中所有可達(dá)格局。不妨設(shè)ct1和c1是第一個(gè)違反弱軌跡等價(jià)的格局，則可知這種違反是由Nai為Ni引起。根據(jù)定理2可知，在N正確的情況下，Nt也是正確的，從而推出若存在違反，則這種違反是由Nai為Ni間不具有弱軌跡等價(jià)引起，而這與定理1結(jié)論矛盾。

證畢。

證明：Na可看成是對(duì)N做n次替換后生成，即每次用Nai替換Ni(i∈[1,…,n])。根據(jù)引理2，每次替換后產(chǎn)生的協(xié)同業(yè)務(wù)過程與替換前具有弱軌跡等價(jià)，則經(jīng)過n次替換后生成抽象協(xié)同業(yè)務(wù)過程為Na與N滿足弱軌跡等價(jià)。

證畢。

證明：由引理3可知N和Na滿足弱軌跡等價(jià)，則可推出N中任意一條交互跡，Na中存在唯一軌跡與之對(duì)應(yīng)。因此，根據(jù)定義10可知，若N|=?，則Na|=?，反之亦然。

證畢。

由定理3，可將對(duì)協(xié)同業(yè)務(wù)過程符合性驗(yàn)證轉(zhuǎn)換為對(duì)其抽象協(xié)同業(yè)務(wù)過程的驗(yàn)證。在保護(hù)流程隱私信息的前提下，這將極大地提高符合性驗(yàn)證效率。

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

本文提出一種基于流程抽象的協(xié)同業(yè)務(wù)過程符合性驗(yàn)證方法，利用實(shí)際數(shù)據(jù)集來闡述本文所提方法的有效性。通過與其他相關(guān)符合性驗(yàn)證方法的實(shí)驗(yàn)對(duì)比，從避免暴露組織內(nèi)部流程信息、符合性驗(yàn)證結(jié)果正確性及驗(yàn)證效率等方面來分析不同符合性驗(yàn)證方法的差異性。

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

本文采用實(shí)際數(shù)據(jù)集來評(píng)價(jià)所提方法的有效性，但當(dāng)前可供實(shí)驗(yàn)的針對(duì)協(xié)同業(yè)務(wù)過程公開數(shù)據(jù)集較少。因此選擇實(shí)際數(shù)據(jù)集UA(university admission)[注]https://ai.wu.ac.at/emisa2015/contest.php。。UA中包括9個(gè)德國大學(xué)入學(xué)申請(qǐng)流程，它們均涉及多個(gè)組織間的交互，能夠較為實(shí)際準(zhǔn)確地反映協(xié)同業(yè)務(wù)過程的協(xié)作場景。

為了進(jìn)行實(shí)驗(yàn)，隨機(jī)地從數(shù)據(jù)集UA中選取5個(gè)協(xié)同業(yè)務(wù)過程。它們所具有的屬性如表2所示，將協(xié)同業(yè)務(wù)過程中含有參與組織個(gè)數(shù)表示為 No. of peers，同時(shí)協(xié)同業(yè)務(wù)過程中含有的狀態(tài)數(shù)及遷移數(shù)分別表示為No. of states, trans。

特別地，UA中每個(gè)入學(xué)申請(qǐng)流程均采用標(biāo)準(zhǔn)業(yè)務(wù)流程建模與標(biāo)注(Business Process Modeling Notation，BPMN)描述。為便于實(shí)驗(yàn)，將上述5個(gè)入學(xué)流程中的每個(gè)業(yè)務(wù)過程先基于文獻(xiàn)[10]中方法轉(zhuǎn)換為Petri網(wǎng)描述，再將其轉(zhuǎn)換為LTS描述。

表2 協(xié)同業(yè)務(wù)過程屬性

同時(shí)，本文選擇此類中典型方法[9-10]作為實(shí)驗(yàn)比較對(duì)象，從避免暴露組織內(nèi)部流程信息、符合性驗(yàn)證結(jié)果正確性及驗(yàn)證效率等方面進(jìn)行對(duì)比分析。

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

首先，通過對(duì)符合性驗(yàn)證之前協(xié)同業(yè)務(wù)過程中的本地活動(dòng)分析，來評(píng)價(jià)本文方法在支持避免暴露組織內(nèi)部流程信息方面的有效性。本文提出內(nèi)部流程信息可見度(簡稱可見度)概念，用來定量評(píng)估組織內(nèi)部流程信息暴露程度。

可見度計(jì)算式如式(1)所示:

(1)

式中，n為協(xié)同業(yè)務(wù)過程中含有業(yè)務(wù)過程數(shù)量。ψi如式(2)所示，用于計(jì)算第i個(gè)業(yè)務(wù)過程(即Ni)內(nèi)部流程信息暴露程度，其中#Ni表示Ni中含有本地活動(dòng)數(shù)量，而#N′i則表示在開展符合性驗(yàn)證前Nai中含有本地活動(dòng)個(gè)數(shù)。對(duì)于可見度而言，其計(jì)算值越高，則表示其在更大程度上暴露組織內(nèi)部流程信息。

(2)

利用式(1)，針對(duì)選取協(xié)同業(yè)務(wù)過程，文獻(xiàn)[9-10]方法和本文提出方法計(jì)算得到的可見度如表3所示。

表3 可見度計(jì)算結(jié)果比較 %

由表3可知，文獻(xiàn)[9-10]方法由于沒有涉及對(duì)內(nèi)部流程細(xì)節(jié)的處理，導(dǎo)致每個(gè)業(yè)務(wù)過程中內(nèi)部流程細(xì)節(jié)全部暴露，因此可見度計(jì)算結(jié)果均為100%，這與跨組織環(huán)境下的隱私保護(hù)原則相違背。而本文方法考慮流程抽象，即針對(duì)每個(gè)業(yè)務(wù)過程，采用弱軌跡等價(jià)將其中含有的內(nèi)部流程細(xì)節(jié)全部移除，因此能夠?qū)崿F(xiàn)組織內(nèi)部流程細(xì)節(jié)全部隱藏，即可見度計(jì)算結(jié)果均為0%。

例如，針對(duì)TU_Munich，通過本文方法構(gòu)建協(xié)同業(yè)務(wù)過程N(yùn)TUM=Application||TUM，其中：業(yè)務(wù)過程Application和TUM分別如圖2a和圖2b所示。由圖2可知，NTUM沒有包含任何本地活動(dòng)，而只含有交互活動(dòng)，故ψ=0%。

通過對(duì)符合性驗(yàn)證結(jié)果進(jìn)行分析，評(píng)估本文所提方法的有效性，以支持驗(yàn)證過程中不會(huì)引入誤判。通過項(xiàng)目組討論分析并咨詢?nèi)雽W(xué)申請(qǐng)領(lǐng)域?qū)＜?，設(shè)計(jì)兩個(gè)領(lǐng)域約束為每個(gè)協(xié)同業(yè)務(wù)過程的測試用例。其中：TCtrue表示測試用例與模型一致，而TCfalse表示測試用例與模型存在不一致。首先，將每個(gè)協(xié)同業(yè)務(wù)過程轉(zhuǎn)換為CSP#流程，然后調(diào)用PAT來驗(yàn)證是否符合領(lǐng)域約束，結(jié)果如表4所示。

表4 驗(yàn)證結(jié)果比較

從表4可以看出，本文方法可以識(shí)別出協(xié)同業(yè)務(wù)過程是否滿足給定的領(lǐng)域約束(即TCtrue和TCfalse)，這表明本文的方法有效。但是，文獻(xiàn)[9-10]提出的方法僅能識(shí)別TCfalse，而針對(duì)TCtrue則會(huì)引起誤判。

例如，針對(duì)協(xié)同業(yè)務(wù)過程Hoh，通過咨詢?nèi)雽W(xué)申請(qǐng)領(lǐng)域?qū)＜遥O(shè)計(jì)如下領(lǐng)域約束Scenario A及Scenario B，其中：Scenario A對(duì)應(yīng)TCtrue，而Scenario B對(duì)應(yīng)TCfalse。

Scenario A：若Hohenheim向Application System提交入學(xué)申請(qǐng)(application)，則最后可以從Office獲得申請(qǐng)結(jié)果(即reject、accept及reservation place)，且Admission Committee在收到Office發(fā)來文檔(doc)后，下一步會(huì)向Office發(fā)送最終確認(rèn)(final confirmation)。

Scenario B：若Hohenheim向Application System提交入學(xué)申請(qǐng)(application)，則只有在提交的入學(xué)申請(qǐng)被接受時(shí)，才能從Office獲得申請(qǐng)結(jié)果(即accept及reservation place)。

通過利用文獻(xiàn)[9]中LeadsTo和DirectlyFollowedBy模式，Scenario A對(duì)應(yīng)的LTL公式如下：

Scenario A_LTL：□ (!application→◇?reject∨◇?resePlace∨◇?accept)∧□ (?doc→○!finalConfimation)。

而通過利用文獻(xiàn)[9]中LeadsTo和isAbsent模式，Scenario B對(duì)應(yīng)的LTL公式如下：

ScenarioB_LTL：□ (!application→◇?resePlace∨◇?accept)∧□ (┐?reject)。

針對(duì)本文所提方法，調(diào)用PAT驗(yàn)證TCtrue及TCfalse的結(jié)果如圖3a所示，而針對(duì)文獻(xiàn)[9-10]方法調(diào)用PAT驗(yàn)證TCtrue及TCfalse的結(jié)果則如圖3b所示。

從圖3可看出，本文方法針對(duì)TCtrue及TCfalse的驗(yàn)證結(jié)果分別為true和false，與期望結(jié)果一致；而文獻(xiàn)[9-10]方法針對(duì)TCtrue及TCfalse的驗(yàn)證結(jié)果均為false。針對(duì)TCtrue，文獻(xiàn)[9-10]方法驗(yàn)證結(jié)果與期望不一致主要是由Admission Committee中執(zhí)行本地活動(dòng)(如Receive application等)導(dǎo)致。

最后，基于影響符合性驗(yàn)證的相關(guān)因素，對(duì)本文提出方法的效率進(jìn)行定量評(píng)價(jià)。文獻(xiàn)[18]通過對(duì)實(shí)際數(shù)據(jù)集SAP參考模型[19]進(jìn)行交互模擬，發(fā)現(xiàn)協(xié)同業(yè)務(wù)過程中含有節(jié)點(diǎn)數(shù)量遠(yuǎn)大于交互數(shù)量。同樣，也通過對(duì)選取協(xié)同業(yè)務(wù)過程進(jìn)行分析，其中含有節(jié)點(diǎn)數(shù)量及交互數(shù)量對(duì)比如圖4所示。

從圖4可看出，針對(duì)每個(gè)選取協(xié)同業(yè)務(wù)過程，其中含有交互數(shù)量均遠(yuǎn)小于節(jié)點(diǎn)數(shù)量(例如，Mue中含有55個(gè)節(jié)點(diǎn)數(shù)，但只有16個(gè)交互)，表明協(xié)同業(yè)務(wù)過程中內(nèi)部流程細(xì)節(jié)所占比例遠(yuǎn)大于交互比例。

具體地，本文提出方法和文獻(xiàn)[9-10]方法均采用的形式化分析方法為模型驗(yàn)證技術(shù)。其基本思想是：采用一個(gè)狀態(tài)遷移模型M來表示待驗(yàn)證的系統(tǒng)，并采用時(shí)序邏輯公式?表示需驗(yàn)證的性質(zhì)，進(jìn)而就可以將“系統(tǒng)是否滿足所期望的性質(zhì)”轉(zhuǎn)化為“M是否滿足公式?，即M|=?”。由于狀態(tài)遷移模型M的狀態(tài)空間決定了模型驗(yàn)證的效率及時(shí)間。為了對(duì)上述兩類方法的符合性驗(yàn)證效率進(jìn)行對(duì)比，采用文獻(xiàn)[20]中的可達(dá)狀態(tài)(reachable state)、有效遷移(fair transition)及系統(tǒng)直徑(system diameter)三個(gè)指標(biāo)進(jìn)行評(píng)價(jià)。系統(tǒng)直徑表示系統(tǒng)從初始狀態(tài)到最遠(yuǎn)可達(dá)狀態(tài)的距離深度；而可達(dá)狀態(tài)和有效遷移則直接影響了模型驗(yàn)證的效率[20]，因?yàn)槠鋽?shù)量反映了系統(tǒng)狀態(tài)空間規(guī)模的大小。需要指出的是，此處的M指由選取協(xié)同業(yè)務(wù)過程(如Col等)根據(jù)定義5中點(diǎn)火規(guī)則生成的狀態(tài)空間；而性質(zhì)?是用來表示領(lǐng)域約束的時(shí)序邏輯公式(如上文中Scenario A_LTL等)。

針對(duì)選取協(xié)同業(yè)務(wù)過程集，本文方法和文獻(xiàn)[9-10]方法在符合性分析效率對(duì)比如圖5所示。

從圖5可看出，由于文獻(xiàn)[11-12]方法在分析過程中沒有對(duì)業(yè)務(wù)過程內(nèi)部流程細(xì)節(jié)進(jìn)行處理，導(dǎo)致其產(chǎn)生的可達(dá)狀態(tài)、有效遷移及系統(tǒng)直徑均遠(yuǎn)大于本文提出方法，因此文獻(xiàn)[9-10]方法的分析效率顯著低于本文提出方法。

例如，針對(duì)協(xié)同業(yè)務(wù)過程Mue，文獻(xiàn)[9-10]方法進(jìn)行符合性驗(yàn)證時(shí)需要搜索狀態(tài)空間如圖6a所示，而本文提出方法進(jìn)行符合性驗(yàn)證時(shí)需要搜索狀態(tài)空間則如圖6b所示。

由圖6可以看出，本文方法進(jìn)行符合性驗(yàn)證時(shí)，需要搜索的狀態(tài)空間遠(yuǎn)小于文獻(xiàn)[9-10]方法，這表明由于本文方法將組織內(nèi)部流程細(xì)節(jié)進(jìn)行抽象，故符合性驗(yàn)證效率遠(yuǎn)高于文獻(xiàn)[9-10]方法。

6 相關(guān)工作

協(xié)同業(yè)務(wù)過程的正確性、一致性及符合性是與本文工作相關(guān)的研究。接下來是對(duì)這3方面的一些典型文獻(xiàn)的介紹和分析。

6.1 正確性驗(yàn)證方法

協(xié)同業(yè)務(wù)過程的正確性是指在設(shè)計(jì)階段對(duì)協(xié)同業(yè)務(wù)過程進(jìn)行驗(yàn)證，以判斷其功能正確性(如無死鎖等)。在國際上，文獻(xiàn)[8]較早提出了跨組織工作流網(wǎng)(Inter-Organizational Workflow，IOWF)概念，被用于跨組織工作流建模。并利用組織內(nèi)業(yè)務(wù)過程合理性的思想提出了IOWF正確性的定義，即要求每個(gè)參與組織業(yè)務(wù)過程是合理的，且IOWF的展開也是合理的。之后這方面的工作主要是以此為基礎(chǔ)開展。為了有效地開展業(yè)務(wù)協(xié)同，文獻(xiàn)[21]最初提出了一種利用面向交互的Petri網(wǎng)(Interaction-Oriented Petri Net, IOPN)構(gòu)建的業(yè)務(wù)流程協(xié)作模型來描述業(yè)務(wù)協(xié)同，該模型由組織內(nèi)的業(yè)務(wù)流程和組織之間的交互組成。然后引入了IOPN的弱合理性概念來定義IOPN的正確性?；诓蛔兞糠纸夥椒?，將弱合理的無回路IOPN分解為一組順序圖，以檢查其邏輯結(jié)構(gòu)的正確性。文獻(xiàn)[22]首先提出跨組織邏輯工作流網(wǎng)(interorganizational Logical Workflow nets,LWNs)用來建?？缃M織環(huán)境下的協(xié)同，并以此為基礎(chǔ)給出了邏輯結(jié)構(gòu)正確性的定義并進(jìn)行了分析。文獻(xiàn)[23]首先提出非對(duì)稱自由選擇網(wǎng)(Asymmetric-Choice Workflow Nets,ACWF-nets)用來建模不同業(yè)務(wù)過程間的交互，并以合理性定義ACWF-nets邏輯結(jié)構(gòu)正確性；之后對(duì)ACWF-nets的合理性與ACWF-nets的結(jié)構(gòu)性質(zhì)間的關(guān)系進(jìn)行討論，從而將ACWF-nets的合理性驗(yàn)證轉(zhuǎn)換為對(duì)其弱合理性的驗(yàn)證。文獻(xiàn)[3]在工作流網(wǎng)WF-Net的基礎(chǔ)上擴(kuò)充資源和消息要素，提出了資源消息工作流程網(wǎng)RM_WF_net(Resource and Message WF-net)用于建模組織內(nèi)業(yè)務(wù)過程，繼而為得到協(xié)同業(yè)務(wù)過程，利用庫所熔合技術(shù)合并業(yè)務(wù)過程間的消息庫所。之后為了保證得到的每個(gè)參與組織的業(yè)務(wù)過程是正確的，使用合理性定義協(xié)同業(yè)務(wù)過程的正確性。因此，協(xié)同業(yè)務(wù)過程執(zhí)行中產(chǎn)生的消息全部被接受，協(xié)同業(yè)務(wù)過程執(zhí)行首尾狀態(tài)一致且不存在死變遷，并借助Petri網(wǎng)可達(dá)圖驗(yàn)證協(xié)同業(yè)務(wù)過程邏輯結(jié)構(gòu)的正確性。鑒于公共管理所具有的交互特性，為了對(duì)其進(jìn)行描述，文獻(xiàn)[24]首先采用BPMN，然后將其轉(zhuǎn)化為基于Petri網(wǎng)的模型，并對(duì)其具有的相關(guān)性質(zhì)(如死鎖等)采用Petri網(wǎng)的展開技術(shù)(unfolding-based technique)進(jìn)行描述?；诖?，可以確保公共管理交互特性的良好執(zhí)行。

協(xié)同業(yè)務(wù)過程正確性關(guān)注其執(zhí)行時(shí)需滿足的普適性質(zhì)[8]，通常采用合理性及其變體(如弱合理等)定義， 對(duì)其進(jìn)行驗(yàn)證的目的是確?？梢哉_執(zhí)行協(xié)同業(yè)務(wù)過程的前提下，實(shí)現(xiàn)特定的業(yè)務(wù)目標(biāo)。一般情況下，只有在確保協(xié)同業(yè)務(wù)過程正確的前提下才有必要對(duì)其符合性進(jìn)行驗(yàn)證[16]，因此協(xié)同業(yè)務(wù)過程正確性可視為其符合性驗(yàn)證的前提。

6.2 一致性驗(yàn)證方法

協(xié)同業(yè)務(wù)過程一致性是指構(gòu)建出的協(xié)同業(yè)務(wù)過程與在構(gòu)建前由參與組織協(xié)商確認(rèn)的規(guī)約(即編排)一致。文獻(xiàn)[25]較早對(duì)協(xié)同業(yè)務(wù)過程一致性驗(yàn)證方法開展研究，它先采用消息順序圖(Message Sequence Chart，MSC)來直觀地建模編排，即從全局視角定義活動(dòng)間同步及異步交互；之后采用IOWF構(gòu)建協(xié)同業(yè)務(wù)過程；最后基于1-consistency來驗(yàn)證協(xié)同業(yè)務(wù)過程是否與編排一致。由于引入1-consistency，該方法能夠在一定程度上緩解狀態(tài)空間爆炸問題。為了增強(qiáng)可用性，文獻(xiàn)[7]提出一種可視化的建模及一致性驗(yàn)證方法，該方法由建模和驗(yàn)證兩個(gè)階段組成。具體地，在建模階段首先利用Web服務(wù)編排定義語言(WS Choreography Definition Language ，WS-CDL)及業(yè)務(wù)流程執(zhí)行語言(Business Process Execution Language ，BPEL)來可視化地描述編排及可執(zhí)行過程，之后將可執(zhí)行過程中內(nèi)部流程細(xì)節(jié)移除，得到抽象業(yè)務(wù)過程；而在驗(yàn)證階段，首先將編排轉(zhuǎn)換為通信順序進(jìn)程(Communicating Sequential Process，CSP)；之后將抽象業(yè)務(wù)過程也轉(zhuǎn)換為CSP進(jìn)程，進(jìn)而將抽象業(yè)務(wù)過程對(duì)應(yīng)CSP進(jìn)程并發(fā)組合得到抽象協(xié)同業(yè)務(wù)過程進(jìn)程；最后為了驗(yàn)證抽象協(xié)同業(yè)務(wù)過程是否與編排間具有精化關(guān)系(即跡等價(jià))來判定一致性是否滿足，可以采用模型檢測工具FDR2(failures-divergences refinement)進(jìn)行自動(dòng)驗(yàn)證。為了從交互及業(yè)務(wù)意圖兩個(gè)層面來驗(yàn)證一致性，文獻(xiàn)[26]提出一種基于Agent方法。該方法首先采用承諾(能夠反映業(yè)務(wù)意圖)及承諾模式(如Outsourcing模式等)來建模編排；然后采用統(tǒng)一建模語言(Unified Modeling Language ,UML)中順序圖來描述協(xié)同業(yè)務(wù)過程；最后將描述協(xié)同業(yè)務(wù)過程的順序圖和定義編排的承諾分別轉(zhuǎn)換為NuSMV規(guī)約和CTL公式，并調(diào)用NuSMV自動(dòng)判定一致性是否滿足。

本質(zhì)上，編排關(guān)注全局交互，而本文中的領(lǐng)域約束則關(guān)注局部交互，它們從兩個(gè)不同視角規(guī)定協(xié)同業(yè)務(wù)過程執(zhí)行應(yīng)滿足的性質(zhì)。在實(shí)際驗(yàn)證中，它們可以結(jié)合使用，故一致性驗(yàn)證可視為符合性驗(yàn)證的有益補(bǔ)充。

6.3 符合性驗(yàn)證方法

協(xié)同業(yè)務(wù)過程符合性意味著協(xié)同業(yè)務(wù)過程的執(zhí)行符合域約束。文獻(xiàn)[27]提出了用于多個(gè)業(yè)務(wù)流程組合驗(yàn)證的概念框架。為了表示進(jìn)程，該框架首先將BPMN建模的協(xié)同業(yè)務(wù)過程轉(zhuǎn)換為以時(shí)間通信順序進(jìn)程CSP+T(communicating sequential processes+time)，然后為了定義預(yù)期的業(yè)務(wù)規(guī)則，使用時(shí)序邏輯公式，并利用在工具FDR2上自動(dòng)驗(yàn)證該模型方法的符合性是否滿足。因此，可以確定協(xié)同業(yè)務(wù)過程可以正確地調(diào)整以適應(yīng)業(yè)務(wù)規(guī)則。為了確保協(xié)同業(yè)務(wù)過程與規(guī)定領(lǐng)域約束一致，文獻(xiàn)[9]提出一種符合性管理框架。它先結(jié)合行為及資源等要素定義符合性語言CRL，并對(duì)CRL中包含模式及模式到LTL公式映射規(guī)則進(jìn)行詳細(xì)地闡述；然后提出利用SPIN模型檢測器進(jìn)行符合性檢測的方法，并實(shí)現(xiàn)業(yè)務(wù)流程合規(guī)管理工具套件(Business Process Compliance Management tool suite ,BPCM)的原型工具。文獻(xiàn)[12]提出一種驗(yàn)證協(xié)同業(yè)務(wù)過程的執(zhí)行符合性方法。首先為了對(duì)協(xié)同業(yè)務(wù)過程進(jìn)行建模，采用BPMN技術(shù)，然后組織的流程轉(zhuǎn)換為ECATNets(Recursive ECATNets)，最后為了得到ECATNets中描述的模型，利用庫所融合技術(shù)將每個(gè)組織的流程進(jìn)行組合。由于該模型語義可以被解釋為條件重寫邏輯，為了有效地驗(yàn)證協(xié)同業(yè)務(wù)過程的行為滿足相關(guān)約束，可以使用Maude LTL模型檢測器來驗(yàn)證協(xié)同業(yè)務(wù)過程的執(zhí)行符合性。然而，上述這些研究工作的關(guān)注重點(diǎn)仍是符合性驗(yàn)證中協(xié)同業(yè)務(wù)過程可視化建模、符合性管理框架設(shè)計(jì)、符合性語言設(shè)計(jì)等方面，并未涉及業(yè)務(wù)過程中內(nèi)部流程細(xì)節(jié)處理。在實(shí)際驗(yàn)證中，忽視內(nèi)部流程細(xì)節(jié)處理將導(dǎo)致組織隱私信息暴露、符合性驗(yàn)證誤判及符合性驗(yàn)證效率低下等問題。

7 結(jié)束語

協(xié)同業(yè)務(wù)過程面向特定行業(yè)(如教育、制造及財(cái)務(wù)等)，驗(yàn)證其與給定應(yīng)用領(lǐng)域特征(如行業(yè)特征、管理規(guī)范及法律法規(guī)等)相符是其有效實(shí)施的一個(gè)關(guān)鍵問題?；诹鞒坛橄螅疚奶岢鲆环N協(xié)同業(yè)務(wù)過程行為符合性驗(yàn)證方法。該方法通過將針對(duì)協(xié)同業(yè)務(wù)過程符合性驗(yàn)證轉(zhuǎn)化為對(duì)抽象協(xié)同業(yè)務(wù)過程符合性驗(yàn)證，能夠有效地避免暴露組織內(nèi)部流程信息、確保符合性驗(yàn)證結(jié)果的正確性及提高形式驗(yàn)證效率。

未來工作主要從以下兩方面展開：①本文中僅考慮涉及協(xié)同業(yè)務(wù)過程行為的領(lǐng)域約束，如何驗(yàn)證包含其他要素(如資源、數(shù)據(jù)等)的領(lǐng)域約束將在下一步工作中詳細(xì)討論；②為避免重復(fù)符合性驗(yàn)證，如何基于給定領(lǐng)域約束對(duì)協(xié)同業(yè)務(wù)過程進(jìn)行修正是一個(gè)值得研究課題。