結合Petri網與進程代數的業務過程協同模型研究

笪建+程耀坤+莫啟

摘要：業務過程協同允許組織之間彼此進行通信、交互與協作以完成特定業務目標。為了完整地描述出一個參與組織的協同，提出進程標號遷移系統PLTS（Process Labeled Transition System），對單個參與組織的模型視圖和通信行為視圖序列進行集成，進而使整個跨組織業務過程協同可以通過各個參與組織的PLTS并行組合而成。該建模方法充分結合了Petri網與CCS各自的優勢，避免了單一運用Petri網與進程代數建模業務過程時面臨的問題，有效支持了業務過程協同的形式驗證。同時為了避免模型狀態空間過大而無法進行有效驗證的問題，提出了6條約簡規則，并證明了這些規則是滿足協同正確性的充分條件，從而使行為驗證方式由模型推導變為代數推導。

關鍵詞：

Petri網；進程代數；跨組織業務過程； 進程標號遷移系統； 約簡

DOIDOI：10.11907/rjdk.172661

中圖分類號：TP301

文獻標識碼：A 文章編號：1672-7800（2017）012-0049-04

Abstract：Business processes collaboration enable organizations to communication， interact and cooperate with each other to achieve their business goals. To the whole cross-organization business process collaboration can be composed of the PLTS of every organization， this method combines the advantages of both Petri Net and CCS， avoiding the issues which occurs by applying petri net and process algebra respectively， which can effectively support collaboration business process formal verification， at the same time， to avoid the state space too big to verify， six rules is proposed and prove that the six rules can guarantee collaboration correctness， so that the mode of behavior verification from the model-based reasoning to algebraic reasoning.

Key Words：Petri Net；process algebra；cross-organization business； process labeled transaction system； reduction

0 引言

隨著經濟全球化與企業信息化的發展，企業經營模式也發生了很大變化，各個企業的業務活動已從獨立模式發展為跨企業多目標合作的協同模式[1]。在現代環境下，沒有一個企業是孤立存在的，企業僅作為參與者參與到業務協作中。在協作過程中，它們彼此交互，完成一定的業務功能[2]。一個業務過程是指用來規劃企業的業務元素。在不同的組織業務過程中，通常會聯系多個業務過程單元，組織邊界被跨越，在電子商務環境下的跨組織信息系統中，業務功能和制造活動之間的流關系得到了廣泛關注[3]。

1 相關研究

對于業務過程，研究者們提出了很多建模與分析方法。如文獻[4]提出了嚴格的語義形式化方法，它的優點是能夠精確地描述和分析業務過程，Petri網與進程代數主要關注了建模和分析業務過程協同；文獻[5]提出，Petri網是一種比較好的業務過程建模語言，因為Petri網有直觀的圖形化表示、嚴格的形式語義、形式化的分析技術，可以清晰描述實例的控制流執行狀態，可用跨組織業務過程建模；文獻[6]提出，進程代數是一種很好的描述和分析并發系統的模型，進程代數具有的顯式交互機制及組合特性最適合對通信、交互特征的跨組織業務過程進行建模，可以采用其中的歸約表示由進程間相互作用形成的動態演化。

在業務過程協同方面， 文獻[7]提出利用Petri網與進程代數進行建模與分析業務過程協同，得到了學術和工業界的廣泛關注。在跨組織業務過程協同領域，對業務過程協同模型進行約簡的文獻并不多見。在文獻[8]中，為了解決動態跨組織工作流協同問題，提出一種基于視圖的方法對跨組織業務過程進行建模，并針對模型中的順序結構、選擇結構及并行結構提出了約簡方法；文獻[9]結合跨組織工作流建模與對象網之間的相似性，提出一種基于公共視圖與對象Petri網的建模方法，并假定該網是自由選擇網的基礎，提出幾種簡單的約簡方法；文獻[10]針對跨組織應急聯動系統的特性，在Petri網模型基礎上進行擴展，提出了OTRM-Net，用于建模任務協同模式和應急處置流程，并對模型的約簡進行了簡單討論。

綜上分析，針對模型約簡存在的主要問題，本文提出進程標號遷移系統，對單個參與組織的模型視圖和通信行為視圖序列進行集成，進而使整個跨組織業務過程協同可以通過各個參與組織的進程標號遷移系統并行組合而成。同時為了避免模型的狀態空間過大而無法驗證的問題以及減少驗證代價，在考慮通信異步的基礎上提出了6條約簡規則，并證明這些規則是滿足協同正確性的充分條件，從而將業務過程的驗證由模型推導轉變為代數推導。

2 進程標號遷移系統及約簡

2.1 進程標號遷移系統

基于Petri網與CCS分別對業務過程模型視圖和通信行為視圖進行建模。對于一個模型視圖，存在一個通信行為視圖序列與之對應，該通信行為視圖序列受模型視圖內部狀態的約束。為了完整描述出一個參與組織的協同，本文借鑒進程代數中標號遷移系統LTS（Labeled Transition System）的思想，引入進程標號遷移系統PLTS（Process Labeled Transition System），對單個參與組織的模型視圖和通信行為視圖序列進行集成。

定義1（進程標號遷移系統） BPV=（IV，PV，ftp）為一個業務過程模型視圖，其進程標號遷移系統形式化定義為一個四元組PLTS=（R（M0），E，P，φ），其中：

（1）R（M0）是模型視圖的可達狀態集，稱為頂點集；M0是模型視圖的初始狀態，稱為根節點。

從定義1可以看出，進程標號遷移系統與標號遷移系統的區別在于：在LTS中，狀態用進程表示，而在PLTS中，狀態用內部視圖中的標識表示；在LTS中，遷移關系用動作表示，而在PLTS中，遷移用通信行為進程和τ表示。

通過PLTS，可以完整地描述出單個參與組織的協同，進而使整個跨組織業務過程協同可以通過各個參與組織的PLTS＼+0并行組合而成。其中，PLTS＼+0表示某個模型視圖初始狀態所生成的進程標號遷移系統。

2.2 約簡規則

模型建立的目的是為了更加準確、直觀、自然地描述所要分析的系統，而驗證則是以建立的模型為基礎對系統進行定性和定量分析，以判斷系統是否滿足既定目標，以對其進行改進。對于跨組織業務過程協同中的某類復雜系統（如聯合制造、供應鏈及電子商務等），其中單個參與組織內部的結構及所實現的業務邏輯復雜難懂，組織之間的交互關系錯綜復雜，跨組織業務過程協同的直接組合往往會使模型的狀態空間過大而無法快速實現對該類復雜系統的驗證。

在跨組織業務過程協同過程中，如果業務過程模型內部視圖不能夠正確終止，則協同必然會失敗。因此，在本文中假定參與協同的業務過程內部視圖都滿足文獻[7]中定義的合理性，并用合理性定義業務過程的正確性，進而使跨組織業務過程協同的驗證變為組織之間交互關系的驗證，即進程標號遷移系統之間交互關系的驗證。

文獻[8]中的研究結果表明，在協同過程中，一個參與組織的內部結構所擁有的弧集及狀態集遠遠大于組織用于協同而開放的接口數，對這些弧集和狀態集進行約簡，能夠極大地減少復雜系統的驗證代價，提高驗證效率。

綜上述，約簡規則應以進程標號遷移為基礎，結合異步消息通信對模型視圖中所擁有的弧集及狀態集進行化簡，只保留體現交互行為的通信行為視圖及必要的內部行為，以達到減少模型狀態空間的目的。由于在PLTS中只存在3種基本類型的結構：順序、選擇及循環，因而約簡規則也從這3方面進行定義。

定義2（協同正確性） 對于參與協同的每一個業務過程，在給定初始標識的情況下，通過交互，使每一個業務過程都能正確結束，即滿足合理性。

定義3（約簡規則） 對于跨組織業務過程模型內部視圖中的任意兩個變遷t＼+1，t＼+2，t＼+1＼+·∩＼+·t＼+2=P，則約簡t＼+1和t＼+2為t后滿足：＼+·t=＼+·t＼+1+＼+·t＼+2-P，t＼+·=t＼+＼{1·＼}+t＼+＼{2·＼}-P。

約簡規則1：令α為某個通信變遷所生成的通信行為視圖，τ為某個瞬時變遷對應的行為，則τ；α可以約簡為α，記為τ；α≈α。其中；表示兩個進程的順序執行，≈表示協同正確性互模擬。

證明：不妨設τ映射的瞬時變遷為a，進程α所映射的通信變遷為t。根據條件可知，約簡后只存在通信變遷為t。根據約簡前滿足協同正確性及定義1可知，瞬時變遷a能夠被執行，則＼+·a都有Token；又因為瞬時變遷a和通信變遷t是順序執行，并滿足瞬時變遷a執行之后通信變遷t能夠執行，可知在執行瞬時變遷a后＼+·t都有Token。因為是順序執行，設瞬時變遷a和通信變遷t之間的庫所集為P，根據定義3可知，約簡后＼+·t＼+＼{post＼}=＼+·a+＼+·t-P。分兩種情況進行討論：

（1）如果P=，則可以推出合并后運行到該階段時，＼+·a+＼+·t都有Token，而＼+·a+＼+·t=＼+·a+＼+·t-P，這等于t被觸發的＼+·t＼+＼{post＼}，因此約簡后通信變遷t能夠被觸發。根據約簡前滿足協同正確性及定義1可知，通信變遷t能夠執行完成。

（2）如果P≠，則可以推出合并后通信變遷t能夠被觸發，必須滿足＼+·a+＼+·t-P都有Token，而＼+·t=＼+·e+a＼+·∩t＼+·，即t的前集由兩部分組成，一部分為外部提供的Token，另一部分為a提供的Token。由＼+·t =＼+·e+P可知，＼+·e=＼+·t-P，則可以推出合并后運行到該階段時，＼+·e+＼+·a都有Token，而這等于t被觸發的＼+·t＼+＼{post＼}，因此約簡后通信變遷t能夠被觸發。根據約簡前滿足協同正確性及定義1可知，通信變遷t能夠執行完成。

不管在哪種情況下，通信變遷t都能夠執行完成，在執行完成后內部其它與a和t存在約束關系的變遷也都能夠被觸發。根據約簡前滿足協同正確性及定義1可知，與之存在消息依賴關系的組織都可以執行完成，從而推導出約簡后的組織和協同組織都可以正確地執行完畢，滿足協同正確性。

τ；τ≈τ和τ.τ≈τ可以看作規則1的特例。

約簡規則2：令α為某個通信變遷生成的通信行為視圖，τ為某個瞬時變遷對應的行為，則α；τ可以約簡為α，記為α；τ≈α。

證明過程與規則1類似，略。

約簡規則3：令α、β為兩個通信變遷生成的通信行為視圖，τ為某個瞬時變遷對應的行為，則α+τ；β可以約簡為α+β，記為α+τ；β≈α+β。其中，+表示兩個進程的選擇執行。

證明： （1）如果左邊的α進程對應的變遷t能夠被觸發，根據約簡前滿足協同正確性，可以推出約簡后也滿足協同正確性。

（2）如果選擇右邊的分支執行，因為τ和進程β是順序執行的，根據規則1可知，約簡后也滿足協同正確性。

約簡規則4 ：令α、β為兩個通信變遷生成的通信行為視圖，τ為某個瞬時變遷對應的行為，則α+β；τ可以約簡為α+β，記為α+β；τ≈α+β。其中，+表示兩個進程的選擇執行。

證明過程與規則3類似，略。

規則3和規則4考慮了異步通信對協同正確性的影響，它沒有聲稱α+τ≈α，是因為其可能因異步通信而導致協同的不正確性，見命題1。

命題1：用α替換α+τ可能導致業務過程不滿足協同正確性。

證明：設協同環境為R，α+τ所在的組織為org。當org執行到狀態M時，可以選擇一個活動執行，分兩種情況討論：①當選擇內部活動執行時，因為org和環境R能夠正確協同，在R中必存在一個不依賴于該選擇階段的內部活動，即R′→τP，其中，R′為R執行到該階段時所處的狀態；②當選擇通信活動執行時，推出R中必存在相關的消息依賴活動。假如通信活動的執行由外部活動rs發送消息而觸發，即R′→rsQ。因為內部活動和通信活動的執行是互斥的，則推出R′→τP和R′→rsQ發生也是互斥的，即R′=τ.P+rs.Q，進而替換后的org與R在該階段一次可能的交互為：α|（τ.P+rs.Q）→τα|P。由定義1可知，由于α得不到rs發送的消息而阻塞，導致org發生死鎖，進而引起業務過程協同的失敗，即不滿足協同正確性。

約簡規則5：令α、β為兩個通信變遷生成的通信行為視圖，P為復合進程，τ為某個瞬時變遷對應的行為，則P=（α；β；τ）；P可以約簡為（α；β）；P，記為P≈（α；β）；P。

證明：從進程P的執行順序看，在一次執行過程中，β進程所映射的通信變遷t和τ映射的瞬時變遷a是順序執行的關系，同時根據合理性定義，進程P的循環次數必須是確定的。因而根據規則1，約簡后滿足協同正確性。

約簡規則6：令α、β為兩個通信變遷生成的通信行為視圖，P為復合進程，τ為某個瞬時變遷對應的行為，則P=（α；τ；β）；P可以約簡為（α；β）；P，記為P≈（α；β）；P。

證明過程與規則5類似，略。

相對于進程代數中的等價理論，約簡規則1～6能夠放寬驗證條件。如α+τ.β和α+β并不弱等價，但是基于規則3，約簡后滿足協同正確性。

定義4（模型推導） 給定一個業務過程模型，為了找到一個與之等價并具有較小狀態空間的業務過程模型，需要首先構造一個可能的業務過程模型，然后根據各自的業務過程模型視圖分別構建可達圖，找到互模擬關系，并進行行為比較，這種方法稱為模型推導。

從定義4可以看出，模型推導需要首先嘗試找到一個可能的、具有較小狀態空間的業務過程模型，然后分別構建各自的可達圖，從可達圖上找出互模擬關系進行判定。該方式工作量大并具有相當大的隨意性，不利于數學推導，也不利于計算機輔助工具的設計與開發。同時，由于基于互模擬關系驗證等價的條件過于苛刻，不能有效地支持狀態空間的約簡。

定義5（代數推導） 對于一個給定的業務過程模型，利用規則1～6、命題1及CCS中的等價理論可以直接推導生成與該業務過程模型等價并具有較小狀態空間的業務過程模型，這種方法稱為代數推導。

從定義5可以看出，與模型推導相比，代數推導不需要首先構造出一個可能與之行為等價的，并具有較少狀態空間的業務過程模型，只需要利用規則1～6、命題1及CCS中的等價關系進行推導判定，提高了驗證效率。同時代數在推導過程中是基于規則1～6的，相對于進程代數中的互模擬關系，弱化了驗證條件，能夠支持具有更小狀態空間的業務過程模型生成。

3 結語

本文針對跨組織業務過程協同進行研究，為了充分反映出跨組織業務過程協同中表現出來的自治、異步及安全保護等特性，引入進程標號遷移系統PLTS對單個參與組織的模型視圖和通信行為視圖序列進行集成。為了減少驗證代價，提出6條約簡規則，并證明了滿足這6條規則的替換是協同正確的，從而將業務過程行為驗證由模型推導轉變成代數推導。未來工作將主要針對以下2個方面問題進行研究：①原型系統實現；②如何對生成的行為進程進行一致性驗證。

參考文獻：

[1] 盧亞輝，明仲，張力.業務過程協同模式的研究[J].計算機集成制造系統，2011，17（8）：1570-1579.

[2] M L ROSA， A TER HOFSTEDE， P WOHED， et al.Managing process model complexity via concrete syntax modifications[J]. IEEE Transactions on Industrial Informatics， 2011，7（2）：255-265.

[3] M L ROSA， P WOHED， J MENDLING， et al.Managing process model complexity via abstract syntax modifications[J]. IEEE Trans. Ind. Informat， 2011，7（4）：614-629.

[4] S LI， L XU， X WANG， et al.Integration of hybrid wireless networks in cloud services oriented enterprise information systems[J].Enterprise Inform，Syst，2012，6（2）：165-187.

[5] K WANG， X BAI， J LI，et al.A service-based framework for pharmacogenomics data integration[J]. Enterprise Inform. Syst， 2010，4（3）：225-245.

[6] L XU.Enterprise systems： state-of-the-art and future trends[J].IEEE Trans. Ind. Informat， 2011，7（4）：630-640.

[7] M ZDRAVKOVI， H PANETTO， M TRAJANOVIC，et al.An approach for formalizing the supply chain operations[J].Enterprise Inform. Syst， 2011，5（4）：401-421.

[8] J GUO， L XU， Z GONG，et al.Semantic inference on heterogeneous e-marketplace activities[J].IEEE Trans. Syst.， Man， Cybern.—Part A： Syst. Humans， 2012，42（2）：316-330.

[9] J GUO.Collaboration role in semantic integration for electronic marketplace[J].Int. J. Electron. Bus， 2010，8（6）：528-549.

[10] VAN DER AALST WMP. Modeling and analyzing interorganizational workflows[C].Proceedings of the 1st International Conference on Application of Concurrency to System Design（CSD'98）， Fukushima. Washington， DC， USA： IEEE Computer Society， 1998：262-272.

（責任編輯：黃 健）