面向數據的工作流的驗證方法

朱永華，趙 琳，高洪皓，沈 熠

（上海大學 計算機科學與信息工程學院，上海200444）

0 引 言

目前，大多數工作流分析方法采用時間依賴圖呈現工作流模型［1］，或用Petri網建模［2］等。基于控制流的檢驗方法僅能驗證活動執行的時序關系，不能滿足商業流程中包含數據流動情況的驗證，因此，必須同時考慮控制與數據。文獻 ［3，4］提及參與工作流的數據，卻沒有考慮錯誤診斷問題。另一方面，雖然有提出了前提條件與后置條件間的數據約束，但對于約束的實現沒有給出明確的算法［6］。

基于控制流，本文在模型中添加數據流動的前提條件與后置條件、數據取值區間，進而判定活動的執行狀態，達到對工作流進行驗證目的。通過實例展示研究問題，基于XPDL框 架 與CTL （computation tree logic），用 建 模 工具TWE對實例所涉及的工作流進行建模，并添加約束條件與活動屬性；將建模完成后保存的.xpdl格式文件，用Shark加載并檢驗工作流正確性，若工作流的描述不符合XPDL語法格式，則無法載入，若加載成功但約束條件錯誤，則在錯誤位置標識死鎖，從而達到驗證工作流的目的。

1 動機與實例

通過一個大型歌唱比賽的工作流模型實例，給出工作流上的活動與數據框架。

首先，發布比賽信息；其次，參賽者報名 （讀取參賽者數與報名費），活動舉辦方獲得廣告商贊助 （讀取贊助費）；接著，進行比賽宣傳 （讀取宣傳費）；進而，活動方準備比賽事項，包括邀請主持人與評審 （讀取評審與主持人費），準備場地與器材 （讀取場地與器材費），準備場地與其它 （讀取獎品及其它費）；之后，進行初賽，復賽 （確定決賽名額）；最后，售決賽觀眾門票 （讀取觀眾人數與票價），邀請電視臺 （讀取邀請電視臺費）并進行決賽。

在圖1中，數據流由12個活動 （圓角矩形描述），8個控制節點 （菱形描述），1 個開始節點 （細線條圓形描述）與1個終止節點 （粗線條圓形描述），以及遷移 （有向箭頭描述）組成。其中，控制節點內為 “＋”符號的表示該控制節點為AND 的并發操作，為 “x”符號的表示該控制節點為XOR 抑或操作。AND 型控制節點分為兩種：ANDsplit與AND－join，其中前者表示有單入度多出度，ANDjoin表示有多入度單出度。同樣，XOR 型控制節點也分為XOR－split與XOR－join，詳見定義1。

本文涉及的變量取值范圍／固定值及變量的含義見表1，其中RegFee、SN、Spon、FT、Atten 為產生資金的變量，Propa、RaH、VaI、PriaO、FT 為消耗資金的變量。

表1 例子中的數據

2 工作流與檢驗性質

2.1 工作流［7］

定義1 一個工作流圖是一個元組P＝ （N；E），其中：①N 是 一 系 列 節 點，包 括XOR－split、AND－split、XOR－join、AND－join、活動、以及唯一的開始與終止節點。②EN×N 是一系列決定了優先順序的有向弧。

XPDL工作流圖是一個有向圖，流程流動方向由節點和遷移決定。其中，在工作流規范中，工作流管理聯盟（workflow management coalition，WFMC）提 出 了XPDL作為標準的工作流建模語言，詳細介紹請參見文獻 ［9］。

2.2 獲取數據

遷移上的約束條件決定了數據在活動間的流動與傳遞。為了簡化處理，本文統一將待賦值的變量的類型定義為浮點型。雖然變量值是一個范圍，而實際進行處理時，需要變量模擬具體值以便于運算。因此，本節通過以下兩種方法，根據變量取指范圍計算實際值。

（1）手動輸入法

以決賽觀眾人數為例，已知變量Atten 的取值區間為300～500，由上述方法，可以得出變量Atten的取值空間為｛300，350，400，450，500｝，用TWS工具對工作流進行驗證的過程中，若采用手動賦值的方式，可將Atten取值空間的每個值賦給Atten。

同理，若采用手動賦值的方式，可計算出每一個變量的取值空間，將該空間的某一值作為變量的實際值。

（2）隨機獲取法

隨機獲取法的基本思想為：首先新建一個能夠獲取隨機數的包應用，將待獲取數據的活動的類型框中ID 項設置為包應用的名稱；接著在活動的類型框中通過新建實參設置數據的取值區間與待賦值變量的名稱，詳見3.1。

因此，用以上兩種方法驗證數據流能否正確執行的抽象算法如下：

2.3 CTL公式

本文的檢驗性質采用CTL進行描述，CTL是描述系統約束的有效方法，詳細定義請參見文獻 ［5，8］。定義2 CTL公式可以遞歸定義如下：

（1）命題常量｛true，false｝和原子命題變元r是CTL公式；

（2）如果p，q是CTL 公式， p、p∨q、p∧q、p→q、AXp、EXp、AFp、EFp、AGp、EGp、A ［pUq］和E［pUq］等也是CTL公式。

在CTL公式中，有兩種成對出現的時態運算符，分別為：A （對于所有路徑）或E （對于一些路徑），以及G（always或Global）、X（neXt）、F（Finally）、或U（Until）。比如：當且僅當從狀態s開始存在一些路徑，滿足p狀態一直有效直到q狀態，則E（pUq）在狀態s是有效的。

2.4 約束條件／CTL公式

在數據流中，能否執行成功主要由活動的約束條件決定。若活動的前提條件不滿足，活動就無法得到執行；若后置條件不滿足，活動就無法正常結束。

將實例大型歌唱比賽的工作流進行分析，得到關于工作流中的每個活動的約束條件，以及活動與約束條件的CTL公式，見表2。

表2 活動的約束條件與CTL公式

例如對于活動 “宣傳”來說，其前置條件為：Spon＞1000000，后置條件為：Propa＞150000，在該活動狀態滿足的CTL公式為：AX（PostP→E［PostP U Pre］），表示對于所有 （本例只有一條）可達的滿足PostP 的活動，存在從 “宣傳”開始的路徑，直到滿足Pre的活動前，路徑中的活動滿足PostP。

要保證工作流能夠正確執行，必須在控制流正確的基礎上保證約束也是正確的。如果工作流不能在約束條件下順利執行，可以通過修改約束條件或者重新布局控制流加以修改，因為約束條件不滿足并不意味著約束條件一定錯誤［2］。

3 建模與驗證過程

本節將介紹工作流的數據賦值和驗證工作。實現變量被賦值，在活動有約束條件下，用CTL 公式描述數據在工作流上的時序關系的基礎上，通過Shark工具驗證變量的值是否滿足預期的約束條件。

3.1 TWE建模

為了實現乘法、生成隨機數的目的，本文建立兩個包應用并對包應用設置形參，分別為：Multiplication與RandomNoGene。RandomNoGene包應用的部分實現代碼如下：

其中min為變量取值范圍的上界，max 為變量取值范圍的下界，result為生成的數值。

圖2中除了信息發布、贊助、宣傳、決賽這4 項活動外，其余活動即為任務應用類型的活動，該類活動的類型框中ID 應選擇相應的包應用名稱，并為活動設置實參與擴展屬性。以活動 “邀請裁判與主持人”為例，該活動類型框中的ID 選擇RandomNoGene包應用后，為包應用新建3個實參，且實參的模式應與形參一一對應，效果如圖3所示。在擴展屬性框，根據需要設置活動的擴展屬性，Name＝"VariableToProcess＿VIEW"，Value＝"RevaHost"。

圖2 采用TWE建模的工作流

圖3 活動IraH 設置參數

對于 “參賽者報名”、 “售觀眾門票”兩項活動來說，由于這兩項活動類型框中的ID 已經選擇了multiplication包應用，故不能同時選擇RandomNoGene包應用，因此，在這兩項活動之前加上隨機生成參賽者數與隨機產生觀眾人數的活動。效果如圖2所示，方法同上。可以在TWE中設置活動的運行方式為Automatic或Manual。

3.2 TWS驗證［10］

建模完成后，用Shark工具將.xpdl格式的文件加載到包管理中并實例化流程，驗證工作流模型的正確性。對于運用了包應用的活動來說，會按照在TWE 中設置的運行方式執行，而對于沒有運用包應用的活動來說必須手動執行。在執行活動的過程中，可以觀察到變量被自動賦值，效果如圖4 所示。顏色為黃色的活動代表工作流執行到該活動。

3.3 變量獲取數據方式比較

上述實驗過程中，數據為自動獲取，由于數據的取值范圍已提前設定好，所以只要約束條件滿足，工作流一定可以正確執行。如果選擇在某活動處手動輸入數據的方式，而輸入的數據不在變量取值范圍之內，或者不滿足約束條件，就會引起后繼活動無法開始，造成工作流無法正確執行。

4 結束語

本文研究了在約束條件下如何判斷數據流能否被正確執行，其中變量的賦值包括如下兩種方式：第一種方式為通過計算的方式求出變量取值空間，進行驗證時手動輸入取值空間的數據；第二種方式為在建模過程中設置成變量隨機獲取數值，因此當對數據流進行驗證時，變量可自動獲取數值。實驗結果表明，基于這樣的方法可以高效地對基于數據的工作流進行驗證。作為本文的進一步工作，工作流的數據驗證將對包括循環的數據流進行深入研究。

圖4 執行活動效果

［1］Ma Yinglong，Zhang Xiaolan，Ke Lu.A graph distance based metric for data oriented workflow retrieval with variable time constraints［J］.Expert Systems with Applications，2014，41（4）：1377－1388.

［2］FU Zuowei，YUE Xiaobo.Research on petri net－based extended workflow model［J］.Computer Applications and Software，2013，30 （9）：173－175（in Chinese）.［傅作為，樂曉波.基于Petri網的擴展工作流模型研究 ［J］.計算機應用與軟件，2013，30 （9）：173－175.］

［3］Sidorova N，Stahl C，Trcka N.Soundness verification for conceptual workflow nets with data：Early detection of errors with the most precision possible ［J］.Information Systems，2011，36 （7）：1026－1043.

［4］TrˇCka N，Aalst WM，Sidorova N.Data－flow anti－patterns：Discovering data－flow errors in workflows ［G］.LNCS 5565：Advanced Information Systems Engineering，2009：425－439.

［5］Christel Baier，Joost－Pieter Katoen.Principles of model checking ［M］.The MIT Press，2008：121－168.

［6］Diana Borrego，Rik Eshuis.Diagnosing correctness of semantic workflow models［J］.Data ＆Knowledge Engineering，2013，87：167－184.

［7］Rik Eshuis，Akhil Kumar.An integer programming based approach for verification and diagnosis of workflows［J］.Data ＆Knowledge Engineering，2010，69 （8）：816－835.

［8］ZENG Hongwei.Verification and testing technology for Web application ［D］Shanghai：Shanghai University，2008 （in Chinese）. ［曾紅衛.Web應用的驗證與測試方法研究 ［D］.上海：上海大學，2008.］

［9］TC00－1003，The workflow management coalition specification［S］.

［10］Together Workflow Server V.5.2－1－20130204－2300－TAB－2.4－1User Manual［S］.