工作流模式的π演算形式化

摘要:為了實現工作流管理功能，必須將業務過程從現實世界中抽象出來，并用一種形式化方法對其進行描述#65377;工作流模式是工作流建模的基本構造單元#65377;π演算是一種移動進程代數，可用于對并發和動態變化的系統進行建模#65377;首先提出以π演算作為工作流形式化的基礎，然后利用π演算對工作流模式進行詳細的描述#65377;

關鍵詞:π演算;ECA規則;工作流模式

中圖分類號:TP311

文獻標識碼:A

1引言

π演算(π-calculus)是Robin Milner提出的以進程間的移動通信為研究重點的并發理論，它是對CCS (Calculus of Communication System) 的發展[1，2]#65377;π演算是系統交互行為建模的理論基礎，適合描述動態系統#65377;在工作流建模階段使用π演算有助于清楚地描述工作流;而在模型建立后，則可利用π演算來推演系統的行為，同時驗證模型的正確性，如發現系統行為不完整#65380;死鎖#65380;缺少同步等;另外，π演算作為一種強大和成熟的形式化方法，π演算有支持其正確性驗證和相關應用的工具，所以π演算自然地成為工作流過程建模的理想工具，例如，文[3，4] 使用π演算對工作流進行了初步的形式化#65377;

工作流模式(workflow patterns)是工作流建模的基本構造單元，從控制流的角度系統地描述了過程定義語言需要滿足的業務需求，與特定的工作流語言無關#65377;本文著眼于對工作流過程建模中反復出現的模式即工作流模式進行π演算形式化#65377;

2π演算

在π演算中，進程是并發運行實體的單位，并以名字來統一定義通道名以及在通道中傳送的消息，每個進程都有若干與其他進程聯系的通道， 數據結構在這里被封裝為與特定通道相關的進程，外部進程通過這些通道來操作相關結構#65377;其基本計算實體為名字和進程，進程之間的通信是通過傳遞名字來完成#65377; 由于π演算不但可以傳遞CCS 中的變量和值等，還可以傳遞通道名，并且將這幾種實體都統稱為名字而不再作區分，這使得π演算具有了建立新通道的能力#65377;

π演算有幾種不同的符號表示[1，2，5，6]，下面介紹π演算的基本語法可由以下BNF范式給出:π演算中最簡單的實體是名字，名字的語法定義是標識符#65377;上述

π演算語法定義中，x是單個名字，與x互為對偶名字(Co-names)，進程通過對偶名字進行交互#65377;P是π演算中另一實體進程的語法定義，而M是π演算中“和“(summations)的語法定義，用以表達選擇關系#65377;π的語法給出進程能夠執行的四種動作，稱為前綴#65377;進程通過執行這些動作而進行演化#65377;π演算形式化π演算語法的形式語義運用約簡關系和變遷關系定義，下面運用自然語言給出它的直觀定義#65377;

(1)0表示非活動進程，即不做任何工作的進程#65377;

(2)前綴π.P表示具有π表示的單一行為能力，該能力執行后，執行進程P#65377;

輸出前綴.p表示通過名字x輸出名字y，然后執行進程P#65377;

輸入前綴x(z).p表示通過名字x輸入名字，并用輸入的名字替換進程P中z， 然后執行替換后的進程P#65377;

啞前綴τ.P 表示做啞動作τ然后執行P，一般來說，τ用于表示進程外部不可見的內部動作#65377;匹配前綴[x=y]π.P 表示當x 和y 是同一名字時，執行π.P，否則不做任何工作#65377;

(3)“和“M1+M2表示選擇執行進程M1#65380;M2中的一個#65377;

(4) 組裝P1|P2表示并行執行P1和P2 #65377;

(5) 限制vzP表示名字z是P的局部名字，P在名字z上的外部動作被禁止，但P通過名字z的內部通信是允許的#65377;

(6) 復制! P表示無限多個P的組裝#65377;

3π演算形式化工作流模式

3.1工作流模式簡介

為了提供基本的工作流建模并評價工作流語言的描述能力， W.M.P. van der Aalst等借鑒設計模式的思想，對工作流模式[7，8]進行了收集和研究#65377;工作流模式指在過程建模中反復出現的模式，與特定的工作流語言無關#65377;

工作流模式分為6 類，共包含20個模式，具體分類如表1所示#65377;

3.2工作流模式的π演算形式化方法

用π演算形式化工作流時，將活動模型化為進程(process)，讓每一個活動對應一個獨立的進程，每一個進程有前置條件和后置條件#65377;進程P是進程Q的前置條件表示P完成后，Q才能開始;進程P是進程Q的后置條件表示Q完成后，Q要給P發送消息#65377;對進程定義時使用事件-條件-動作(Event-Condition -Action，簡稱ECA)規則，ECA規則#65377;描述了觸發活動的事件和內部條件，實際上也描述了執行活動的執行依賴關系#65377;ECA規則中的事件和條件對應進程的前置條件，事件模型化為π演算中的輸入前綴，條件模型化為π演算中的匹配前綴;ECA規則中的動作分成兩種:分別對應進程的內部動作和進程的后置條件#65377;顯然，如果一個進程定義時沒有事件部分(即輸入前綴)，則這個進程表示一個開始活動;如果一個進程定義時沒有后置條件，則這個進程表示一個最后的活動#65377;因此，定義一個基本活動可用如下π演算形式:

其中，輸入前綴x對應ECA規則中的事件，匹配前綴[a=b]對應ECA規則中的條件，τ..0對應ECA規則中的動作#65377;

下面使用上述方法形式化表1中模式:

順序模式的解決辦法 對這種模式進行π演算形式化時，我們把一個活動模型化為進程A，另一個活動模型化為進程B，進程A和進程B通過通道b進行通信，如圖1#65377;由上文介紹的π演算形式化工作流模式的基本思想，可得到如下的π演算形式化表示:A=τA..0表1工作流模式分類表其中，進程B在完成內部動作τB后，激發后續進程B′#65377; 圖1順序模式并行分支模式的解決辦法:這種模式進行π演算形式化時，我們把一個活動模型化為進程A，另外兩個活動模型化為進程B和進程C，進程并行分支為進程B和進程C，進程A和進程B通過通道b進行通信，進程A和進程C通過通道c進行通信，如圖2#65377;由上文介紹的π演算形式化工作流模式的基本思想，可得到如下的π演算形式化表示:

其中，進程B在完成內部動作τB后，激發后續進程B′;進程C在完成內部動作τC后，激發后續進程C′#65377;

并行分支模式同步模式的解決辦法:對這種模式進行π演算形式化時，我們把一個活動模型化為進程B，另外兩個活動模型化為進程C和進程D，進程B和進程C同步為進程D，進程B和進程D通過通道d1進行通信，進程C和進程D通過通道d2進行通信，如圖3#65377;由上文介紹的π演算形式化工作流模式的基本思想，可得到如下的π演算形式化表示: 其中，進程D在完成內部動作τD后，激發后續進程D′#65377;

圖3同步模式互斥模式的解決辦法 類似于并行分支模式的解決辦法，可得到如下的π演算形式化表示:簡單匯聚模式的解決辦法 類似于同步模式的解決辦法，可得到如下的π演算形式化表示:關于其它模式的π演算形式化可類似得到，由于篇幅原因，不再贅述#65377;

4總結

本文利用π演算對工作流模式進行了詳細的描述，這種方法是完全形式化的，具有較強的語義表達能力#65377;基于工作流模式分析是從控制流的角度出發，所以本文的分析結果也只是說明這種模型描述過程控制流的能力，通過使用數據和環境變量等方式，整個工作流管理系統能滿足更廣泛的需求#65377;另外需要說明的是，工作流模式所描述的業務需求雖然較廣泛和全面#65377;但是，并不能完全涵蓋實際應用的所有場景#65377;

注：本文中所涉及到的圖表、注解、公式等內容請以PDF格式閱讀原文。