[發明專利]基于Pi演算的分布式流程驗證系統及方法

無效

• 申請號: 201010609285.0
• 申請日: 2010-12-28
• 公開（公告）號: CN102043681A
• 公開（公告）日: 2011-05-04
• 發明（設計）人: 郭小群;侯紅;丁劍潔
• 申請（專利權）人: 西北大學
• 主分類號: G06F11/00
• 分類號: G06F11/00
• 代理公司: 西安恒泰知識產權代理事務所 61216
• 代理人: 李鄭建

技術領域

本發明屬于工作流和計算機技術領域，具體涉及一種驗證用BPEL語言描述的流程是否正確的方法，特別是一種基于Pi演算的分布式流程驗證系統及方法，該方法能夠驗證當多個流程并發推進時是否會有死鎖發生，并給出死鎖發生原因。

背景技術

隨著經濟的全球化，業務模式和組織形式的多樣化，流程出現了分布式、跨組織、多任務協作等特點，對流程管理提出了靈活性和移動性等新的需求。目前開發分布式流程的主要語言是BPEL，一個新的流程被開發出來后，為了保證流程在實際運行中的正確性，流程在部署之前必須被驗證，但由于業務模式的分布式、跨組織、多任務協作的特點，使得流程的驗證變得很困難。

目前關于流程的驗證研究很多，比較流行的是基于Petri網的驗證方法。Petri網有精確的定義，可對工作流及工作流系統進行定性和定量分析，這使得Petri網成為主要的建模技術之一。在國外，Aalst等對Petri網工作流模型進行了深入的研究。在國內，范玉順，suyou?li，西北大學軟件工程研究所等也做了很多有益的工作。Petri網具有豐富的分析技術可以幫助判斷過程設計的正確性，但Petri網由于無法表達移動性，不能驗證分布式、多任務協作流程。

Pi演算理論因其適合于描述移動性而日益引起人們的重視，目前很多人嘗試用Pi演算驗證分布式工作流，但這些驗證都停留于手工階段，關于如何用計算機協助人們驗證用BPEL語言描述的流程是否會產生死鎖的方法目前還沒有。

發明內容

針對上述現有技術存在的缺陷或不足，本發明的目的在于，提供一種基于Pi演算的分布式流程驗證系統及方法，本發明克服了目前用Pi演算驗證分布式工作流程中驗證都停留于手工階段的缺陷或不足，在本發明的驗證系統中運用驗證方法，可以驗證用BPEL語言描述的分布式流程是否存在死鎖，并精確定位死鎖位置，找出或者發現由于流程設計的不恰當，當并發協作的流程在推進時在什么地方會出現死鎖，并重新設計流程，從而保證在把流程部署到真實環境之后，流程運行的正確性。

為了實現上述任務，本發明采取如下的技術解決方案：

一種基于Pi演算的分布式流程驗證系統，其特征在于，所述的驗證系統至少包括如下模塊：

BPEL語言編輯模塊，用來開發被驗證的BPEL流程；

BPEL語言到Pi演算的轉換模塊，用來將被開發出來的BPEL流程轉換為Pi演算；

Pi演算編輯模塊，用來對轉換后的Pi演算進行改寫；

Pi演算驗證模塊，用來對生成的Pi演算公式進行驗證：把轉換后的每個Pi演算公式當作一個進程，然后將所有進程共同推進，通過進程間的通信判斷是否有流程死鎖發生；

死鎖原因顯示模塊，用來顯示解釋死鎖狀態的文本文件；

所述BPEL語言編輯模塊、BPEL語言到Pi演算的轉換模塊、Pi演算編輯模塊、Pi演算驗證模塊和死鎖原因顯示模塊依次相連接，在Pi演算驗證模塊中，通過各模塊互相之間的進程通信來判斷分布式流程中是否存在死鎖，并在死鎖原因顯示模塊中通過顯示解釋死鎖狀態的文本文件來定位死鎖位置。

進一步的，所述流程死鎖有如下特征：

a、在流程推進中，流程已經無法和其他流程通信，但還至少有一個流程不能最終到達中止狀態；

b、在流程推進中，雖然流程之間還可以通訊，但有多于一個的流程卻不斷重復回到某一中間狀態。

一種利用基于Pi演算的分布式流程驗證系統的方法，其特征在于，包括如下步驟：

步驟1，BPEL語言編輯模塊用BPEL語言描述將要部署的流程；

步驟2，BPEL語言到Pi演算的轉換模塊對用BPEL語言描述的流程進行轉換，得到若干個Pi演算流程；

步驟3，Pi演算編輯模塊對得到的Pi演算流程進行改寫；

步驟4，Pi演算驗證模塊采用Pi演算的規約理論進行死鎖檢查；

所述的流程死鎖有如下特征：在流程推進中，流程已經無法和其他流程通信，但還至少有一個流程不能最終到達中止狀態；或者，在流程推進中，雖然流程之間換可以通訊，但卻不斷重復回到某一中間狀態。

步驟5，死鎖原因顯示模塊用文本文件解釋死鎖狀態，定位死鎖位置。

進一步的，所述步驟2的轉換過程具體包括如下步驟：

步驟201：讀入整個BPEL文件；

步驟202：把BPEL文件中process標簽對應的過程名作為一個Pi演算進程名；