基于活動依賴實現業務流程可變性的ＢＰＭＳ模型

摘 要:從活動依賴性的角度提出一種支持業務專家修改業務流程的BPMS模型D-BPMS(dependence based business process management system)， 即能夠使業務專家按照業務需求通過調整業務活動之間的依賴關系和配置業務活動的屬性達到調整業務流程的目的。它在體系結構上分為表示層、流程邏輯層、業務邏輯層和數據層四個層次。在流程邏輯層采用消息傳遞機制設計算法實現流程結構變化模式，證明了D-BPMS模型變化模式的完備性和變化的可驗證性，并可用Petri網來驗證流程變化的正確性。

關鍵詞:業務流程; 依賴性; 可變性; 消息傳遞機制; Petri網

中圖分類號:TP311文獻標志碼:A

文章編號:1001-3695(2009)09-3348-06

doi:10.3969/j.issn.1001-3695.2009.09.042

Model of BPMS for supporting variability ofbusiness process based on dependence

HONG Yu-ke ZHAO Wei YAO Qing

(1.College of Computer Science Technology， Shandong University， Jinan 250061，China; 2.Information Center，Qingdao Power Company， Shandong Electric Power Group， Qingdao Shandong 266002， China)

Abstract:From the view of business dependence， this paper provided a business process management system model named D-BPMS， which could support business process experts to adjust the structure of business process directly. Divided the architecture of D-BPMS into four layers: presentation layer， process logic layer， business logic layer and data layer. In the business process logic layer， it provided the message link mechanism to achieve the process change mode. By adjusting the dependence between the business activities and configurating the business activities attributes， D-BPMS had the ability to achieve the business expert’s aim of adjusting the structure of business process according to the business requirement， also the changed business process could be verified by the Petri-net.

Key words:business process; dependence; variability; message link mechanism; Petri nets

業務流程可變性的研究是業務流程管理研究的一個重要方面，總體上分為兩類:a)從建模角度，研究如何在實際業務流程中提取出可變性部分進行建模，如應用過程代數[1]、EPC[2]、BPMN[3]建模;b)從實現方面，研究在軟件系統架構中實現這些業務流程的變化，包括組件技術和SOA (service-oriented architecture)技術。

本文結合已有的研究成果，為實現業務流程可變性提出一種支持業務人員修改業務流程的系統模型(D-BPMS)，使業務人員在不依賴IT專家的基礎上按照業務領域需求調整業務流程。在流程調整時，D-BPMS模型的流程邏輯層對流程的結構進行調整，而無須考慮底層的實現。D-BPMS模型的業務邏輯層和數據層根據流程結構的變化進行相應調整。

1 相關工作

實現業務流程可變性技術方面的研究，主要出現了:

a)面向對象的方法(OOP)。它采用抽象的概念，對業務活動進行封裝，通過繼承來擴展被封裝的業務活動;利用接口，多態機制實現業務流程的可變性。

b)面向組件的方法。組件技術支持業務流程可變性，分布在網絡中不同位置的組件通過通信進行協作來完成任務。通過改變組件之間的協作方式和消息交互格式來支持流程的可變性。

c)面向領域技術。它對應用領域對象和角色進行建模，對象和角色承擔業務功能[4，5]。通過對象和角色的結合來構成業務流程，不同的結合過程構成不同的業務流程，從而實現可變性。

d)面向服務的方法(SOA)。它將不同的服務通過定義良好的接口聯結起來構成業務流程，給BPMS帶來了靈活性和可變性[6]。文獻[5]給出了組合Web service構造業務流程的方法，在這個基礎上提出了基于SOA的BPMS模型，為實現業務流程可變性提供了參考方案[7~9]。

除了以上主要的方法，還有其他一些實現方法。消息中間件，通過協調不同部件之間的消息來實現業務流程的可變性。業務流程可變性的研究也采用了agent的思想10]，通過agent的智能組合來實現流程的可變性。文獻[11]也進行了基于網格的業務流程可變性研究。

在綜合分析現有實現業務流程可變性的方法后，本文提出了D-BPMS模型。該模型從實現的角度解決了在脫離IT專家的參與下，業務人員能夠根據業務要求調整流程的結構。

2 D-BPMS模型

2.1 D-BPMS模型定義

定義1 消息(M)

M=〈id，name〉，id為惟一標號，name為消息命名。

定義2 功能活動(FA)

FA=〈id，interface，fun，attr〉，id為惟一標號，interface為CA調用接口，attr∈{角色，設備，組件，Webservice，服務組合}。

定義3 連接活動(CA)

CA=〈status，rcmsg，needmsg，sendmsg，sendtoactivity〉，status為CA的狀態，Rcmsg為{M}，Needmsg為{M}，Sendmsg為{M}，{M}為M的集合，sendtoactivity為{M-CA}，M-CA為發送M到CA。

定義4 業務活動(BA)

BA={FA}∪{CA}，{FA}∩{BA}=。

定義5 活動依賴性(CD)

CD=(a，b，oper) a∈CAset，b∈CAset，oper∈{，，，，}。

(a，b，):a順序依賴b

(a，b，):a，b并行依賴

(a，b，):a，b互斥依賴

(a，b，):滿足BDD中a，b依賴性的定義

(a，b，):a，b無依賴

定義6 流程邏輯結構(FLM)

FLM={seq，sel，syn，mex，loop}，seq為順序結構，sel為選擇結構，syn為并行結構，mex為互斥結構，loop為循環結構，M(CAa，CAb)為CAa、CAb具有M結構，{CAa，CAb }CAset， CAa∩Cab=， M∈ FLM( FLM中任意元素的組合)。

定義7 消息傳遞路徑(PATH)

PATH=〈head，tail，CAset，CFset〉，head為路徑的頭節點，Tail為路徑的尾節點，CAset位于head、tail之間由CFset連接成一條傳遞路徑。

定義8 消息鏈(ML)

ML=〈CAset，CFset〉，CAs∈CAset，CAe∈CAset，CAsetBPN，{CAset，CFset}BPN.CFset，PATH∧(PATH.head=CAs)∧(PATH.tail=CAe)∧(PATH.CFsetBPM.CFset)。

定義9 業務流程網(BPN)

BPN=〈CAset，FAset，Mset，CAs，CAe，CFm，FMm，CFset，CDset〉，CAset為CA的非空有限集合，FAset為FA的非空有限集合，CAset∩FAset=，Mset為M的非空有限集合，CAs為惟一起始節點，CAs.needmsg=，CAe為惟一結束節點，CAe.sendmsg=， CAe.sendtoactivity=，CFm:CAset→FAset的雙射函數，FMm為CFset→Mset的雙射函數，CFset={CA×CA}∧CFset≠∧|CFset|≥1，CDset:CD的非空有限集合，{ca，cb}CAset→(ca.needmsg∩cb.needmsg=)∧(ca.sendmsg∩cb.sendmsg=)，ca∈CAset→ ML∧ca∈ML。

定義10 業務字典(BDD)

BDD=〈BCDset，BCAset，BFAset，BAset〉，CDsetBCDset，FAsetBFAset，CDsetBCDset，BABAset。

2.2 D-BPMS模型結構和實現業務流程可變性的關鍵問題

D-BPMS在體系結構上分為表示層、流程邏輯層、業務邏輯層和數據層四個層次，如圖1所示。FA的交互界面位于表示層、向用戶顯示和收集數據。CA位于流程邏輯層，實現流程的構造，通過調整業務依賴關系實現可變性。FA位于業務邏輯層，實現流程的實際功能。數據層包含BDD，存儲流程的數據和運行時的狀態信息。

D-BPMS模型的定義和結構表明實現流程可變性的關鍵是流程邏輯層業務活動依賴關系和變化模式的實現，因此下文分析流程可變性的實現機制，變化模式的完備性證明和流程變化正確性的驗證。

3 流程變化的實現，完備性證明和正確性驗證

3.1 業務流程的構造方法和可變性的實現

1)業務流程的構造

業務流程(圖2)描述如下: BPN開始于C1，結束于C7;C1執行完后同時向C2發送M2，C3發送M3;C2和C3接收到消息后檢查執行條件是否滿足，若滿足則啟動C2和C3;C2和C3啟動關聯的FA;在C2和C3執行完成后，C2向C4發送M4，C4檢查是否滿足執行條件;C3向C5發送M5，向C6發送M6;C5和C6檢查是否滿足執行條件，滿足條件則執行;C7檢查是否滿足執行條件，滿足條件則執行。

根據D-BPMS模型的定義，圖2中BPN定義為:

BPN=〈CAset，FAset，Mset，CAs，CAe，CFm，FMm，CFset，CDset〉

CAset ={C1，C2，C3，C4，C5，C6，C7}

C1=(T，Φ， Φ，{M2，M3}，{M2-C2，M3-C3})

C2=(F， Φ，{M2}，{M4}，{M4-M4})

C3=(F， Φ，{M3}，{M5，M6}，{M5-C5，M6-C6})

C4=(F， Φ，{M4}，{M7}，{M4-C7})

C5=(F， Φ，{M5}，{M8}，{M8-C7})

C6=( F， Φ，{M6}，{M9}，{M9-C7})

C7=( F， Φ，{M7，M8，M9}，Φ， Φ)

FAset={F1，F2，F3，F4，F5，F6，F7}

Mset={M2，M3，M4，M5，M6，M7，M8，M9}， CAs=C1，CAe=C7

CFm={(C1，F1)，(C2，F2)，(C3，F3)，(C4，F4)，(C5，F5)，(C6，F6)，(C7，F7)}

CFset={(C1，C2)，(C1，C3)，(C2，C4)，(C3，C5)，(C3，C6)，(C4，C7)，(C5，C7)，(C6，C7)}

FMm={((C1，C2)→M2)，((C1，C3)→M3)，((C2，C4)→M4)，((C3，C5)→M5)，((C3，C6)→M6)，((C4，C7)→M7)，((C5，C7)→M8)，((C6，C7)→M9)}

CDset={(C2，C1，)，(C4，C2，)，(C7，C4，)，(C3，C1，)，(C2，C3， )，(C5，C3，)，(C6，C3，)，(C7，C5，)，(C7，C6，)， (C5，C6，)}

2)流程結構的變化模式

定理1 D-BPMS模型中，FLMCD。

證明

a)D-BPMS中，FLM={seq，sel，syn，mex，loop}

因為{ca，cb}CAset

若seq(ca，cb)→(cb，ca，)，seq(cb，ca)→(ca，cb，)

若sel(ca，cb)→cd∧cd∈{(ca，cb，)，(ca，cb，)}

若syn(ca，cb)→(ca，cb，)

若mex(ca，cb)→(ca，cb，)

若loop(ca，cb)→(cb，ca，)∧(ca.needmsgcb.send-msg)∧((ca.needmsg-ca)cb.sendtoactivity)

b)D-BPMS模型中CD.oper∈{，，，，}

因為{ca，cb}CAset

若(cb，ca，)→seq(ca，cb)，(ca，cb，)→seq(cb，ca)

若(ca，cb，)→syn(ca，cb)

若(ca，cb，)→mex(ca，cb)

若(ca，cb，)→cd∧cd∈{(ca，cb，)，(cb，ca，)，(ca，cb，)，(ca，cb，)，(ca，cb，)}

若(ca，cb，)→{d∧cd∈{(ca，d，op) ，(d，ca，op)}}∧{e∧ed∈{(e，cb，op)，(cb，e，op)}}，op∈{，，}

綜上所述，定理得證，即D-BPMS中， FLM、CD描述流程結構的能力等價。

業務流程結構的變化模式在文獻[12]中進行了總結，如添加(add)、刪除(del)、合并(mer)、拆分(div)活動、順序—并行、并行—互斥等。D-BPMS模型中流程結構變化模式定義如下。

定義11 原子變化(ATC)

D-BPMS模型中ATCset=FLM×FLM∕{(sel，sel)，(syn，syn)，(mex，mex)，(loop，loop)}∪{add，del，mer，div}

ATC∈ATCset∧ATC(〈CA〉，〈CA〉)

定義12 復合變化CTC

D-BPMS模型中，{CAa，CAb}CAset， {M1，M2}FLM，若(M1，M2)(CAa，CAb)至少需要經過一個ATC，則CTC={∪ATC(t)|1≤ t ≤N∧ (ATC(t)∠ATC(t+1))}，則表示為(M1，M2) (CAa，CAb)CTC。其中:(M1，M2)(CAa，CAb)為(CAa，CAb)的結構由M1變為M2，∠為ATC的先后順序，為變化)。

定理2 {Ma，Mb}FLM，{CAa，CAb}CAset，Ma(CAa，CAb)∧{{ca，cb}{CAa∪CAb}∧ca≠cb→(ca，cb，)}∧Mb(CAa，CAb)∧{({ca，cb}{CAa，CAb}∧ca≠cb)→(ca，cb，)}→CTC∧(Ma，Mb)(CAa，CAb)CTC。

證明 因為在Ma時，Ma(CAa，CAb) ∧({ca，cb}∈{CAa∪CAb }∧ca≠cb)→(ca，cb，))

a)若CTC={atc1∠atc2∠atc3∠…∠atcn}

當ATC=atc1，即(Ma，M2)(CAa，CAb)atc1

因為M2∈FLM

FLMCD(定理1)

所以Ni∈M2→CD(Ni)( CD(Ni)為用CA的依賴關系表達Ni)

CD(N)∝M2 。其中:CD(N)=CD(N2)○CD(N3)○CD(N4)…○CD(Nn)，○為復合，∝為描述。

b) 當ATC依次為atc2，atc3，atc4，…，atcn，得到M2，M3，…，Mn

ATC=atcn時，Mn=Mb

因為FLMCD

Mb(CAa，CAb)∧({ca，cb}∈{CAa∪CAb}∧ca≠cb→(ca，cb，))

所以Fi∈Mn→CD(Fi)

CD(F)∝M(CD(F)=CD(F2)○CD(F3)○CD(F4)○…○CD(Fn))

CTC∧(Ma，Mb)(CAa，CAb)CTC。

綜上所述，定理2得證。

在證明了定理1和2后，以(seq，seq)，add，(seq，syn)變化模式為例，證明可以采用消息傳遞機制來設計算法實現D-BPMS模型的ATCset。

c)ATC實例的實現算法證明

(a) D-BPMS模型中(seq，seq)變化模式。如圖2所示的(seq，seq)變化。Bpn.CDset={(C4，C1，)，(C2，C4，)，(C7，C2，)，(C3，C1，)，(C3，C4，)，(C5，C3，)，(C6，C3，)，(C7，C5，)，(C7，C6，)，(C2，C5，)，(C5，C6，)}，從Bpn.CDset的依賴關系中分析變化為(seq，seq)(C2，C4))，根據變化模式利用消息傳遞機制設計算法1以實現Bpn。

算法1 (seq，seq)變化模式

輸入:BPN(T)，R，S，CDset，{R，S}BPN(T).CAset，(R，S，)

輸出:BPN(M)

if({R，S}BDD.BCAset(R，S，)){

//修改CA的屬性

D.R.sendmsg=R.sendmsg;

D.R.sendtoactivity=R.sendtoactivity;

R.sendmsg=S.sendmsg;

R.sendtoactivity=S.sendtoactivity;

S.needmsg=R.needmsg;

R.needmsg=S.sendmsg;

S.sendmsg=D.R.sendmsg;

S.sendtoactivity=D.R.sendtoactivity;

//修改BPN的連接屬性

BPN(T).FMm=BPN(T).FMm/((R，S)，M)∪{(S，R)，M};

BPN(T).CFset=BPN(T).CFset/(R，S)∪(S，R);

BPN(T).CDset=CDset;

BPN(M)=BPN(T);

}else{不可調整，退出;}

(b)D-BPMS模型中add變化模式。Bpn.CDset={(C2，C1，)，(C8，C2，)，(C4，C1，)，(C4，C8，)，(C2，C4，)，(C7，C4，)，(C3，C1，)，(C5，C3，)，(C7，C5，)，(C6，C3，)，(C7，C6，)，(C2，C3)，(C5，C6，)}，從BPN(T).CDset的依賴關系分析表明，變化模式為add(C2，C8)，根據變化模式，利用消息傳遞機制設計算法2以實現Bpn。

算法2 Add變化模式。

輸入: BPN(T)，R，S，CDset，R∈BPN(T).CAset，(R，S，)

輸出:BPN(M)

if({R，S}BDD.CAset(R，S，)){

BPN (T).Mset= BPN (T).Mset∪{Mn};

//修改CA的屬性

S.needmsg=Mn;

S.sendmsg=R.sendmsg;

S.sendtoactivity=R.sendtoactivity;

R.sendtoactivity={(Mn-S)}

//修改BPN的連接屬性

BPN (T).CFset=BPN(T).CFset∪{(R，S)};

BPN (T).FMm=BPN(T).FMm∪{(R，S)，Mn};

CC∧(R，CC)∈BPN(T).CFset→BPN(T).CFset∪{(S，CC)};

CC∧((R，CC)，M)∈BPN(T).FMm→{BPN(T).FMm∪((R，CC)，M)};

BPN(T).CFset/{(R，CC)∈BPN(T).CFset};

BPN(T).FMm/{((R，CC)，M)∈BPN(T).FMm};

(ps，CAs)∈CFset→(CAs=ps);

(pe，CAe)∈CFset→(CAe=pe);

BPN(T).CDset=CDset;

BPN(M)= BPN(T);

}else{不可調整，退出;}

(c)D-BPMS模型中(seq，syn)變化模式。Bpn.CDset={(C2，C1，)，(C7，C2，)，(C4，C1，)，(C7，C4，)，(C2，C4，)，(C3，C4，)，(C2，C1，)，(C5，C3，)，(C7，C5，)，(C6，C3，)，(C7，C6，)，(C4，C5，)，(C5，C6，)}，從Bpn.CDset的依賴關系中表明，變化模式為(seq，syn)(C2，C4)，根據變化的模式，利用消息傳遞機制設計算法3以實現Bpn。

算法3 (seq，syn)變化模式

輸入: BPN(T)，R，S，CDset，{R，S}BPN(T).CAset，(R，S，)

輸出:BPN(M)

If({R，S}BDD.CAset(R，S，)){

//修改BPN的連接屬性

BPN(T).CAset=BPN(T).CAset∪{CA0，CB0};

BPN(T).Mset=BPN(T).Mset∪{Mab0，Mab1，Mab2，Mab3};

BPN(T).CFset=BPN(T).CFset∪{(R，CA0)，(R，CB0)，(CA0，S)，(CB0，CN)}/{(R，S)};

BPN(T).FMn=BPN(T).FMn∪{((R，CA0)，Mab0)，((R，CB0)，Mab2)，((CA0，S)，Mab1)，((CB0，CB0)，Mab3)}/{((R，S)，M)};

//修改CA的屬性

R.sendmsg={Mab0，Mab2};

R.sendtoactivity={(Mab0-CA0)，(Mab2-CB0)};

S.needmsg={Mab1，Mab3};

CA0.needmsg={Mab0};CA0.sendmsg=Mab1;

CA0.sendtoactivity={(Mab1-S)}

CB0.needmsg={Mab2};CB0.sendmsg=Mab3;

CB0.sendtoactivity={(Mab3-S)};

FA∧(R，FA)∈ BPN(T).CFm→BPN(T).CFm∪{(CA0，FA)}/(R，FA);

FB∧(S，FB)∈BPN(T).CFm→{BPN(T).CFm∪{(CB0，FB)}}/(S，FB);

BPN(M)= BPN(T);

}else{不可調整，退出;}

以上算法實例證明了可以通過修改CA之間消息傳遞路徑來實現(seq，seq)，add，(seq，syn)，同樣也可以用消息傳遞機制實現其他ATC。在第4章將以流程變化實例來說明這些算法的過程。下面證明ATCset和消息傳遞機制的完備性。

3.2 ATCset和消息傳遞機制完備性證明

文獻[13]證明了YAWL流程描述語言能夠描述現有的流程結構，并具有形式化的語義。下面證明ATCset和消息傳遞機制的完備性。設文獻[13]總結的流程結構集合為NFLM。

定理3D-BPMS中，若I=NFLM，則ATCset和消息傳遞機制是完備的(I:全部流程結構的集合)。

證明

a)D-BPMS能描述YAWL的流程結構 (記為D-BPMS∝YAWL)。證明見表1的映射。

b)定理1證明了FLMCD，從而可以用FLM完成表1的映射。

表1 YAWL語法元素到D-BPMS元素的映射

YAWL的元素D-BPMS中對應的描述

conditionCA.needmsg

inputConditionCAs

outputConditionCAe

atomic taskFA

composite taskFA

multiple stance(CA.needmsg-CA)CA.sendtoactivity

multiple instance of acomposite task(CA.needmsg-CA)CA.sendtoactivity∧CA.FA= FA

AND-split task|CA.sendtoactivity|=M，|CA.needmsg|=1，{(m1-sa)，(m2-sb)}CA.sendtoactivity→(sa，sb，)(M為實際的流程分支數)

XOR-split task|CA.sendtoactivity|=1≤M，|CA.needmsg|=1，|CA.needmsg|=1，{(m1-sa)，(m2-sb)}CA.sendtoactivity→(sa，sb，)(M為實際的流程分支數)

OR-split task1≤|CA.sendtoactivity|≤M，|CA.needmsg|=1，|CA.needmsg|=1，{(m1-sa)，(m2-sb)}CA.sendtoactivity→(sa，sb，)∨(sa，sb，)(M為實際的流程分支數)

AND-join task|CA.needmsg|=N，|CA. sendtoactivity |=1，{sa，sb}CA.needmsg →(sa，sb，)(N為實際需要的消息數量)

XOR-join task|CA.needmsg|=1≤N，|CA. sendtoactivity |=1，{sa，sb}CA.needmsg →(sa，sb，)(N為實際需要的消息數量)

OR-join task1≤|CA. needmsg| ≤N，|CA. sendtoactivity|=1，{sa，sb}CA.needmsg →(sa，sb，) ∨(sa，sb，)(N為實際需要的消息數量)

c)因為YAWL能夠描述I，a)證明了D-BPMS∝YAWL，則D-BPMS也能描述I。由b)可知，FLM可以描述I，從而證明FLM是完備的，又由定義12和定理 2得ATCset也是完備的。

d){M1，M2}I∧{M1(CAa，Cab)，M2(CAa，Cab)}，由ATCset的完備性可知:CTC∧(M1，M2)(CAa，CAb)CTC，CTC={ATC1∠ATC2∠…∠ATCn}。

又因為atc∈CTC→F(atc)(F(atc)表示利用消息傳遞機制實現atc變化模式的算法)

所以F(CTC) (F(CTC)=F1(ATC1)○F1(ATC2)○…○F1(ATCn))

消息傳遞機制是完備的，能實現CTC。

綜上所述，定理得證。

在D-BPMS模型中證明了ATCset和消息傳遞機制的完備性之后，可以利用CTC對流程進行調整，但需要驗證流程變化的正確性。下面證明在D-BPMS模型中，流程變化的正確性是可驗證的。

3.3 流程變化正確性的驗證

D-BPMS中流程結構變化后需要進行正確性驗證。D-BPMS采用自由選擇擴展WF-Net驗證流程變化性的正確性，判定是否可以對流程進行這種調整。下面簡要介紹定理4中用到的關于Petri網和WF-Net (工作流網)[14]的基本概念。

Petri網定義N=(P，T，F)，其中:P是庫所;T是變遷;F是流關系; N是自由選擇網。當且僅當:

p∈P，|p|>1→((p)={p}∨(∩{(p)}=))

WF-Net定義Petri網N=(P，T，F)是WF-Net當且僅當滿足如下兩個條件:

a)存在兩個特殊位置，I表示起始庫所(source)，即I=;O表示終止庫所，即O=。

b)如果在變遷T中添加一個變遷t，F中加入(O，t)和(t，I)形成PN，則PN是強連通的。

WF-Net為擴展工作流網當且僅當加入一個新的變遷t，使t連接O和I，且t={O}，t={I}。

定理4BPN的正確性是可驗證的。

證明

a)BPN∞Petri-net(Θ表示原子映射，∞表示復合映射，{p，p1，p2}P，{t1，t2，tm}T，{tk}Token)

因為BPN的Mset，CAset，FMm可映射

m Θp，m∈BPN.Mset

cΘt，c∈BPN.CAset

smΘtk(sm表示任意消息的實例)

((c1，c2)，m)∞{c1Θt1，c2Θt2，mΘp，(t1，p)，(p，t2)}，((c1，c2)，m)∈ BPN.FMm

因為BPN的CDset可映射(定理1的證明中可知，完成下列映射，即可完成BPN.CDset的映射)

(c1，c2，)∞{c1Θt1，c2Θt2，((c1，c2)，m) ∞{mΘp，(t1，p)，(p，t2)}}，((c1，c2，))∈BPN.CDset;

(c1，c2，)∞{c1Θt1，c2Θt2，{s∧((s，c1)，m1)∈BPN.Ω∧((s，c2)，m2)∈BPN.Ω→{sΘtm，m1Θp1，m2Θp2，{(tm，p1)，(p1，t1)，(tm，p2)，(p2，t2)}}}∨{f∧((f，c1)，m3))∈BPN.Ω}∧((f，c2)，m4)∈BPN.Ω}→{fΘtf，m3Θp3，m4Θp4，{(t1，p3)，(t2，p4)，(p3，tf)，(p4，tf)}}}，((c1，c2，))∈BPN.CDset;

(c1，c2，)∞{c1Θt1，c2Θt2，{s∧((s，c1)，m1)∈BPN.Ω∧((s，c2)，m2)∈BPN.Ω→{sΘtm，m1Θp1，{(tm，p1)，(p1，t1)，(p1，t2)}}}∨{f∧((c1，f)，m3)∈BPN.Ω∧(c2，f)，m4)∈BPN.Ω}→{fΘtf，m3Θp3，{(t1，p3)，(t2，p3)，(t3，tf)}}}，((c1，c2，))∈ BPN.CDset;

所以通過以上映射BPN∞Petri-net。

b)因為BPN定義中，{ca，cb}CAset→(ca.needmsg∩cb.needmsg=)∧(ca.sendmsg∩cb.sendmsg=)，則BPN∞自由選擇Petri網(FC)。

c)因為FC存在起始點和終止點，即

{pi，po}P∧(CAsΘtas)∧(CAeΘtao)→{(pi，tas)，(tao，po)}

d) 在FC中加入tr，{(tao，tr)，(tr，tas)}，則FC是強連通的，即BPN∞由選擇WF-Net(WFCN)。

e) 在WFCN中加入tr，且tr={O}，tr={I}，則BPN∞自由選擇擴展WF-Net。用文獻[15]的化簡自由選擇擴展WF-Net的方法驗證映射后自由選擇擴展WF-Net，從而證明BPN是可驗證的。

綜上所述，定理得證。

根據定理 4，圖2中BPN映射為圖3的WNP(自由選擇擴展WF-Net)。圖3中WNP有惟一的起始點I(M1)，惟一的終止點O(M0)。WNP中加入變遷T8，(M0，T8)，(T8，M1)，則WNP是強連通的。在開始狀態，M1含有托肯，存在變遷C1、C2、C4、C7到達終止態O。WNP中不存在死的變遷，WNP是正確的。T8={O}，T8={I}，所以WNP為自由選擇擴展WF-Net。

文獻[15]給出了八條化簡規則用于自由選擇擴展WF-Net的驗證。圖4描述PWNP化簡過程，化簡結果表示從開始庫所經過一個變遷到達了終止庫所，匹配文獻[15]中定義的正確模式，從而證明流程變化是正確的。

4 D-BPMS模型應用實例分析

結合本課題的背景虛擬旅行平臺(應用D-BPMS模型設計)來討論出國旅游簽證手續辦理流程(VBP)的可變性。圖5表示VBP在調整前簽證類別包含因私簽證和因公簽證。圖5虛線框內是根據旅行社簽證辦理業務調整而添加的商務旅行簽證辦理流程(NBP)。

圖5中G2是NBP的BPN，并且具有如下關系:E1ΘCA1， AND1ΘCA2，B1ΘCA3，B2ΘCA4，AND2ΘCA5，E2ΘCA6。VBP中，CDset=VBP.CDset∪{(CA1，CB1，)，(CA2，CA1，)，(CA3，CA2，)，(CA4，CA2，)，(CA5，CA3，)，(CA6，CA3，)，(CA3，CA4，)，(CA1，CB1，)， (CA1，CB1，)}。

若(Ca，Cb，oper)∈CDset→(Ca，Cb，oper)∈BDD.CDset，則可進行這種變化調整，否則不能對VBP進行這種調整。

現在討論CDsetBDD.CDset時，用D-BPMS模型的CTC調整VBP.CTC={add(CA1，CA2)，add(CA2，CA3)，add(CA3，CA4)，add(CA4，CA5)，add(CA5，CA6)，(seq，syn)(CA3，CA4)，add(CB3，CA1)，add(CA6，CB4)，(seq，syn)(CB3，CA1)}，由定理2可知，CTC可以完成這種變化。調整的過程如下:

初始NBP=〈CAset，FAset，Mset，CAs，CAe，CFm，FMm，CFset，CDset〉，CAset={CA1}，CA1=(F，Φ，MA31，Φ，Φ)，FAset=Φ，Mset=Φ，CAs=CA1，CAe=CA1，CFm=Φ，FMm=Φ，CFset=Φ，CDset=Φ。

a)ATC=Add(CA1，CA2)后，則NBP結果為CAset={CA1，CA2}，CA1=(F，Φ，MA31，MA1，{M1-CA2})，CA2=(F，Φ，MA1，Φ，Φ)，Mset={MA1}，FMm={((CA1，CA2)，MA1)}，CFset={(CA1，CA2)}，CDset={(CA2，CA1，)}。

b)ATC依次為add(CA2，CA3)，add(CA3，CA4)，add(CA4，CA5)，add(CA5，CA6)后，則NBP結果為

CAset={CA1，CA2，CA3，CA4，CA5，CA6}，FAset={B1，B2}

CA1=(F，Φ，MA31，MA1，{M1-CA2})

CA2=(F，Φ，MA1，MA2，{MA2-CA3})

CA3=(F，Φ，MA2，MA3，{MA3-CA4})

CA4=(F，Φ，MA3，MA4，{MA4-CA5})

CA5=(F，Φ，MA4，MA5，{MA5-CA6})

CA6=(F，Φ， MA5，Φ，Φ)，CAs=CA1，CAe=CA6

Mset={MA1，MA2，MA3，MA4，MA5}，CFm={(CA3，B1)，(CA4，B2)}

FMm={((CA1，CA2)，MA1)，((CA2，CA3)，MA2)，((CA3，CA4)，MA3)，((CA4，CA5)，MA4)，((CA5，CA6)，MA5)，}

CFset={(CA1，CA2)，(CA2，CA3)，(CA3，CA4)， (CA4，CA5)， CA5，CA6)}

CDset={(CA2，CA1，)，(CA3，CA2，)，(CA4，CA3，)，(CA5，CA4，)，(CA6，CA5，)}

c)ATC=(seq，syn)(CA3，CA4)后，則NBP結果為

CAset={CA1，CA2，CA3，CA4，CA5，CA6}，FAset={B1，B2}

CA1=(F，Φ，MA31，MA1，{M1-CA2})

CA2=(F，Φ，MA1，{MA2，MA20}，{MA2-CA3，MA20-CA4})

CA3=(F，Φ，MA2，MA3，{MA3-CA5})

CA4=(F，Φ，MA20，MA4，{MA4-CA5})

CA5=(F，Φ，{MA3，MA4}，MA5，{MA5-CA6})

CA6= (F，Φ，MA5，Φ，Φ)

Mset={MA1，MA2，M20，MA3，MA4，MA5}

CAs=CA1，CAe=CA6，CFm={(CA3，B1)，(CA4，B2)}

FMm={((CA1，CA2)，MA1)，((CA2，CA3)，MA2)

((CA3，CA5)，MA3)，((CA4，CA5)，MA4)，((CA2，CA4)，MA20)，((CA5，CA6)，MA5)，}

CFset={(CA1，CA2)，(CA2，CA3)，(CA3，CA5)，(CA2，CA4)，(CA4，CA5)，(CA5，CA6)}

CDset={(CA2，CA1，)，(CA3，CA2，)，(CA5，CA3，)，(CA5，CA4，)，(CA6，CA5，)，(CA4，CA2，)，(CA3，CA4，)}

d)ATC依次為add(CB3，CA1)，add(CA6，CB4).(seq，syn)(CB3，CA1)后，則VBP結果為

CAset=(VBP.CAset∪NBP.CAset)∧(CB1.sendmsg=

CB1.sendmsg∪{MA31})∧(CB1.sendtoactivity=

CB1.sendtoactivity∪{MA31-CA1})∧(CB4.needmsg=CB4.needmsg∪

{MA32})∧(CA6=(F，Φ，MA6，MA32，{MA32-CB4}))

FAset=VBP.FAset∪NBP.FAset

Mset=VBP.Mset∪NBP.Mset∪{MA31，MA32}

CAs=VBP.CAs，CAe=VBP.CAe

CFm=VBP. CFm∪NBP.CFm

FMm=VBP.FMm∪NBP.FMm∪{((CB1，CA1)，MA31)，((CA6，CB4)，MA32)}

CFset=VBP.CFm∪NBP.CFet∪{(CB1，CA1)，(CA6，CB4)}

CDset=VBP.CDset∪NBP.CDset∪{(CA1.CB1，)，(CB4，CA6，)，(CA1，CB1，)，(CA1，CB2，)}

上述實例展示了應用D-BPMS提供的方案解決NBP的添加問題。由定理4得VBP∞VPTON，并用文獻[15]提出的化簡方法證明VPTON是正確的，從而證明在VBP添加NBP是正確的。圖6為VBP∞VPTON((a)為VPTON;(b)(c)是化簡過程的中間狀態，在此基礎上一直應用化簡規則，可以得到開始庫所經一個變遷到終止庫所的結果，從而驗證VPTON是正確的)。

5 結束語

本文提出的業務流程管理系統模型(D-BPMS)能夠支持業務人員調整業務流程的結構。D-BPMS流程邏輯層根據業務之間的依賴關系利用消息傳遞機制調整流程結構。D-BPMS在業務流程的調整階段需要設計好CA之間的依賴關系。業務專家通過流程邏輯層提供的方法修改流程中業務活動的依賴關系來直接調整流程，而不需要IT專家修改代碼和重新部署BPMS。D-BPMS模型為了支持流程結構的變化需要業務邏輯層和數據層的支持，因此下一步的工作是重點研究業務邏輯層和數據層的實現機制。

參考文獻:

[1] FERRARA A. Web services:a process algebra approach[C]//Proc of International Conference on Service Oriented Computing.New York:ACM Press，2004:242-251.

[2]ROSEMANN M， VAN DER ALAST W M P. A configurable reference modeling language[J]. Information Systems， 2007， 32(1):1-23.

[3]KAMOUN F. A roadmap towards the convergence of business process management and service oriented architecture[M]. New York:ACM Press，2007.

[4]JABLONSKI S， FAERBER M， BERNHARD V. Deriving biological applications from domain specific process models[C]//Proc of Conference on Information and Knowledge Management. Lisbon， Portugal:ACM Press， 2007:23-30.

[5]PAUTASSO C， HEINIS T， ALONSO G. Autonomic resource provisioning for software business process [J]. Information and Software Technolgy， 2007，49(1): 65-80.

[7]JABOLNSKI S， LAY R， MEILER C， et al. Data logistics as a means of integration in healthcare applications[C]//Proc of Symposium on Applied Computing. Santa Fe， New Mexico:ACM Press，2005:236-241.

[8]MOTAHARINEZHAD H R， MARTENS A， CURBERA F， et al. Semi-automated adaptation of service interactions[C]//Proc of International World Wide Web Conference. 2007:993-1002.

[9]JABLONSKI S， BERNHARD V. A conceptual modeling and execution framework for process based scientific applications[C]//Proc of Conference on Information and Knowledge Management. Lisbon， Portugal:ACM Press， 2007:23-30.

[10]GIOVANNI R， KERNLAND M E， GHIZZIOH R. LS/ABPM:an agent-powered suite for goal-oriented autonomic BPM[C]//Proc of International Conference on Autonomous Agents. 2008:1701-1702.

[11]JENG J J， CHANG H， CHUNG J Y. BPMM:a grid-based architectural framework for business process meta management[C]//Proc of Symposium on Applications and the Internet (SAINT’03). 2003:84-91.

[12]張靜. 支持業務流程變化的軟件系統構建方法研究[D].濟南:山東大學，2007.

[13]ASLST W M P van der， HOFSTEDE A H M ter. YAWL:yet another workflow language[J]. Information Systems， 2005，30(1):245-273.

[14]ASLST W M P van der. Verification of workflows nets[C]//Proc of Application and Theory of Petri nets， Lecture Notes in Computer Science， volumn 1248. Berlin:Springer-Verlag，1997:107-226.

[15]趙俊峰，謝冰，張路，等. 一種支持領域特性的Web服務組裝算法[J]. 計算機學報，2005，28(4):731-738.

[15]李建強，范玉順.基于Petri網化簡方法的工作流模型驗證[J]. 信息與控制，2001，30(6):492-497.