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

無效

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

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

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

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

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

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

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

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

2.如權利要求1所述的基于Pi演算的分布式流程驗證系統，其特征在于，所述流程死鎖有如下特征：

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

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

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

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

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

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

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

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

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

4.如權利要求3所述的方法，其特征在于，所述步驟2的轉換過程具體包括如下步驟：

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

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

步驟203：掃描整個BPEL文件，找出并列的活動標簽及處理機制標簽，把每一個活動標簽名及處理機制標簽名作為一個Pi演算進程名，所有這些進程及一個接收進程的并發作為process標簽名對應的進程所定義的內容；

步驟204：判斷步驟203中的活動標簽是否是結構化的活動，如果是，則掃描結構化活動之間的文本，轉入步驟206進行轉換，否則轉入步驟205，直到過程的并發全部變為基本活動；

步驟205：把每一個基本活動當作一個Pi演算進程，給出每一個基本活動的Pi演算描述；

步驟206：提取結構化活動之間并列的標簽名，轉入步驟203，把每一個活動標簽名及處理機制標簽名作為一個Pi演算進程名。

5.如權利要求3所述的方法，其特征在于，所述步驟3的Pi演算編輯模塊對得到的Pi演算流程進行改寫，是指對經過BPEL語言到Pi演算的轉換模塊而得到的Pi演算公式中的進程名及通道名進行改寫，即把BPEL語言中用的描述活動、過程、消息等短語改寫為大寫或小寫的英文字母，并采用注釋的形式記錄下來。

6.如權利要求3所述的方法，其特征在于，所述步驟4的?Pi演算驗證模塊采用Pi演算的規約理論進行死鎖檢查具體包括如下步驟：

步驟401：把每一個Pi演算公式看作一個單獨的進程；

步驟402：判斷這些進程是否能歸約，如果能，轉入步驟404；否則轉入步驟403；

步驟403：判斷所有進程是否到達中止狀態，如果有沒有到達中止狀態的，則死鎖發生，記錄下當前所有進程的狀態，以及之前進程的狀態；否則無死鎖發生，正常終止；

步驟404：如果能夠規約，判斷是否有多于一個進程到達的狀態是以前到達過的某個中間狀態，如果是，則死鎖發生，記錄下當前所有進程的狀態，以及之前進程的狀態；否則轉入步驟405；

步驟405：按Pi演算的規約規則進行規約，并轉回步驟402，直到有死鎖發生或正常終止。