業務流程的形式化設計與驗證

丁明， 張書玲， 張琛

(1.西北大學 信息科學與技術學院， 陜西， 西安 710127;2.中航工業西安航空計算技術研究所，陜西， 西安 710119;3.西安電子科技大學 計算機學院， 陜西， 西安 710071)

?

業務流程的形式化設計與驗證

丁明1，2， 張書玲1， 張琛3

(1.西北大學 信息科學與技術學院， 陜西， 西安 710127;2.中航工業西安航空計算技術研究所，陜西， 西安 710119;3.西安電子科技大學 計算機學院， 陜西， 西安 710071)

針對如何保證業務流程設計模型與業務需求的一致性問題，在研究有限自動機模型的基礎上，提出了一種業務流程的自動機模型構建和驗證方法.采用擴展的帶約束條件的確定有限自動機對業務流程設計模型進行形式化描述，使用線性時序邏輯表示業務需求，分別給出業務流程設計模型到自動機模型和自動機模型到Promela描述的轉換算法，并通過模型檢測技術，使用Spin工具驗證設計模型是否滿足需求性質.若不滿足性質，則能夠獲得反例執行的路徑.實例分析表明，該方法可用于業務流程設計的正確性驗證.

業務流程; 確定有限自動機; 模型檢測; 線性時序邏輯

業務流程由存在于企業價值鏈條上的一系列活動及其之間的關系構成，是企業提高效率和增加效益的重要手段. 為了增強業務流程的可靠性，保證設計結果的正確性，避免未經過有效驗證的流程設計被開發、測試、甚至交付使用，造成返工修改，浪費大量的人力和物力，可應用形式化方法進行模型驗證，確保流程設計與需求的一致性.

業務流程模型可以使用不同的形式化方法描述和驗證. 目前常見的方法包括:文獻[1]中提出了一種語義業務流程的驗證方法，可驗證流程中活動之間以及活動與工作流底層結構的一致性. 文獻[2]中提出了一種驗證流程執行的自動推理方法，通過遍歷業務流程活動之間的相互關系，生成多個子句集，然后使用路徑搜索判斷其可達性. 文獻[1-2]的方法對順序、合取、析取三類邏輯關系的流程活動進行了建模和驗證，不適合于復雜流程的循環、嵌套等結構. 文獻[3]中設計了一個描述和分析業務流程的半自動化框架，實現過程應用行為時序邏輯描述語言表達行為條件，使用Petri網描述中間語義. 文獻[4]中提出了應用Petri網對業務流程自下而上和自上而下的建模方法，并對流程的弱終止性進行了分析驗證. 文獻[3-4]中提出的方法均使用Petri網對業務流程進行建模，Petri網具有直觀的圖形化表示、精確的語義、強大的表達能力和基于狀態而不是基于事件等優點. 但是，其相應具有更高的空間復雜度. 若為了降低復雜度，限制Petri網有界，則其表達能力不會超過有限自動機[5]. 文獻[6]中提出了一種業務流程建模和合規性驗證的方法，通過將業務流程執行語言表達的業務流程轉化為Pi演算模型，進而轉化為有限自動機模型進行合規性驗證. 文獻[7]中提出了一種支持多業務協作的業務流程形式化驗證方法，采用Pi演算形式化描述業務流程的執行語義，進而轉化為代碼輸入模型檢測器， 判斷流程是否滿足給定準則. 文獻[6-7]采用了Pi演算進行業務流程建模和驗證，作為一種理論成熟的進程代數方法，它使用基于文本的進程表達式描述系統，具有形式簡單、表達能力強等優點. 但其應用存在方法抽象、圖形表達能力差等缺點. 文獻[8]中通過建立流程的有向有環圖模型，提出了一種圖形歸約和圖形展開相結合的工作流過程模型局部和過程邏輯錯誤驗證方法. 文獻[9]提出了一種通過使用一組化簡規則和允許結構沖突的方法，逐步縮減工作流圖，驗證流程是否包含死鎖和同步沖突. 文獻[8-9]采用圖形縮減技術驗證工作流過程模型的正確性，具有表達形式簡單、直觀等優點，但對于復雜應用的業務流程模型支持存在不足，不適用于驗證循環和嵌套的重疊結構.

模型檢測是一種自動驗證有窮狀態系統的形式化驗證技術，可驗證設計模型是否滿足于業務需求，從而保證設計的正確性[10]. 確定有限自動機(deterministic finite automata， DFA)是一類能夠根據給定函數實現確定的狀態遷移的自動機. 為了準確表達業務流程中各活動的輸入、輸出、相互關系和作用，本文采用帶約束條件的確定有限自動機(conditioned deterministic finite automata， CDFA)作為描述業務流程的形式化模型. 并且，基于自動機的驗證技術相對成熟，為本文研究工作奠定了基礎.

1 業務流程建模

1.1 業務流程

Michael Hammer與James Champy給出了業務流程的經典定義:定義某一組活動為一個業務流程，這組活動有一個或多個輸入，輸出一個或多個結果，這些結果對客戶來說是一種增值[11]. 典型的業務流程包括:輸入資源，按一定規則執行的活動，活動之間的相互關系和作用(即結構)，輸出結果，顧客，流程創造的價值，表示方式如下.

定義1(業務流程) 業務流程用一個14元組表示，

P=(O，Ao，At，A，C，t，N，s，E，H，φ，η，α，β)，

式中:O為業務流程在交互過程中所有參與主體的集合;Ao為主體執行的不會引發遷移的活動，可為空，表示為εv;At為主體執行的會引起遷移的活動，可為空，表示為εx;A為交互過程中所有活動的集合，A=Ao∪At;C為遷移約束條件的集合，可為空，表示為εc;t為主體之間交互的遷移函數，O×(At×C)→O;N為被調用操作的集合，可為空，表示為εn;s為開始節點;E為終止節點的集合;H為后繼流程的集合，可為空，表示為εh;φ為從At到O的一個函數關系，φ(at)∈O，at∈At，表示活動at的發送主體;η為從At到O的一個函數關系，η(at)∈O，at∈At，表示活動at的接受主體;α為從Ao到O的一個函數關系，α(ao)∈O，ao∈Ao， 表示活動ao所對應的主體;β為從E到H的一個函數關系，β(h)∈E，h∈H，表示后繼流程h對應的終止節點，β(εh)=?.

此處以圖1所示的簡單流程為例，說明業務流程的14元組定義過程. 圖1所示流程的14元組定義如下.

P=({start_node， A， B， C， D， end_node}，

{action A， action B， action C， action D}，

{start，pass1， pass2，pass3，end}，

{action A，action B， action C， action D，

start， pass1， pass2， pass3， end}，

{condition=true， condition=false}，

{t(start_node，start)=A，

t(A，[condition=true]pass1)=B，

t(A，[condition=false]pass1)=C，

t(B， pass2)=D， t(C，pass3)=D，

t(D， end)=end_node}，

{εn}， {start_node}， {end_node}，

{εh}， {φ(start)=start_node， φ(pass1)=A，

φ(pass2)=B， φ(pass3)=C，

φ(end)=D}， η(start)=A，

{η(pass1)=B， η(pass1)=C， η(pass2)=D，

η(pass3)=D， η(end)=end_node}，

{α(action A)=A， α(action B)=B，

α(action C)=C， α(action D)=D}， {?}).

1.2 業務流程的自動機模型

CDFA是擴展的帶約束條件的確定有限自動機，用以形式化描述業務流程. CDFA的狀態對應表達業務流程中各活動的主體，狀態遷移描述了業務流程主體之間的交互. 遷移用二元組標注，包括所發生的事件和事件發生的約束條件. 狀態遷移表示對象接受或者發送滿足約束條件的消息，按給定的轉移函數從一個狀態轉移到另一狀態. CDFA 可以準確表達業務流程中各活動的輸入、輸出、相互關系以及活動間的遷移. 以下給出了CDFA的9元組定義.

定義2(CDFA) 帶約束條件的確定有限自動機M是一個9元組，

M=(Q， R， V， X， Σ， δ， λ， q0， F)，

式中:Q為狀態非空的有窮集合，?q∈Q，q稱為自動機M的一個狀態;R為動作的約束條件集合，可為空，表示為ε;V為狀態內部動作的集合;X為交互動作的集合;Σ為輸入字母表，輸入字符串都是Σ上的字符串，Σ={(r，x)| r∈R，x∈X};δ表示狀態轉移函數，Q×Σ→Q;λ是從V到Q的一個函數關系，λ(v)∈Q，v∈V，表示內部動作v所對應的狀態;q0表示M的初始狀態，q0∈Q;F表示M的終止狀態集合，F?Q.

通過以下轉換規則構造業務流程CDFA模型.

定義3 業務流程的CFDA模型構造算法.

令業務流程P=(O，Ao，At，A，C，t，N，s，E，H，φ，η，α，β)，對應的帶約束條件的確定有限自動機M可表示為一個9元組

M=(Q，R，V，X，Σ，δ，λ，q0，F).

算法1 構造業務流程的CDFA模型.

輸入:業務流程的14元組描述.

輸出:業務流程的CDFA模型.

① 創建初始狀態q0=s;

② 狀態集合Q=O，每個狀態與業務流程中的一個主體相對應;

③ 約束條件集合R=C;

④ 狀態內部動作集合V=Ao;

⑤ 交互動作集合X=At;

⑥V到Q的函數關系λ定義為λ(v)∈Q，?v∈V，λ(v)=α(v);

⑦ 輸入字母表Σ={(r，x)|r∈R，x∈X}={(c，at)|c∈C，at∈At};

⑧ 狀態轉移函數δ(q，(r，x))∈Q，?q∈Q，δ(q，(r，x))=t(q，(r，x));

⑨ 終止狀態集合F=E，每個終止狀態與業務流程中的一個終止節點相對應.

2 業務流程驗證

通過模型檢測技術，驗證業務流程設計模型與業務需求性質之間的一致性. 模型檢測[12-14]是一種針對系統屬性驗證的形式化方法，已被廣泛應用于軟/硬件、通信、安全等方面. 模型檢測用狀態遷移系統描述系統的行為，能夠對有窮狀態系統的各類復雜的時序性質進行驗證，當判斷某性質不被滿足時能夠提供反例，以便定位設計錯誤.

2.1 業務流程驗證方法

本文使用由貝爾實驗室開發的模型檢測工具Spin[15](simple Promela interpreter)進行一致性驗證，工具通過Promela語言描述系統模型，采用線性時序邏輯[16](linear-time temporal logic， LTL)定義待驗證的性質. 驗證過程如圖2所示，首先采用14元組定義業務流程;其次根據定義3的構造算法將業務流程轉換為帶約束條件的確定有限自動機模型，并使用Promela語言描述;然后定義業務需求待驗證性質的LTL公式;最后將Promela描述的模型與LTL定義的需求性質輸入驗證工具Spin. Spin對兩者的一致性進行模擬校驗，如發現違背性質的任何反例，輸出驗證結果為業務流程設計不滿足需求;如未發現反例，說明流程設計與需求一致.

2.2 業務流程自動機模型到Promela描述的轉換

Promela是一種類C程序語言的抽象語言，用于描述通信協議或分布式系統，可對有限狀態系統進行形式化建模. Promela描述的模型是一個有限轉換系統，由進程、消息通道、變量和全局對象組成，進程之間相互通信，每個進程都可看作是擴展的有限自動機.

業務流程的CDFA模型向Promela描述進行轉換的算法實現如下:

算法2 CDFA模型到Promela描述轉換算法.

輸入:業務流程的CDFA模型.

輸出:CDFA模型的Promela描述.

1: //生成mytype類型說明.

2: for inti=1 to Ubound(AUTOMATA.Transitions)

3:{ Promela.mytype[i]=AUTOMATA. Transitions[i];}

4://生成chan msg 通道說明定義.

5:for inti=1 to Ubound (AUTOMATA.States)

6:{if (AUTOMATA.States)[i].is End State==false)

Promela.Newchanmsg(AUTOMATA.States[i]);}

7: //內部動作為布爾型，初始值false，表示動作未執行.

8: for inti=1 to Ubound (AUTOMATA.Actions)

9:{ Promela.New Bool Variable(AUTOMATA.Actions[i]);}

10: //將所有約束條件定義為相應的變量.

11: for inti=1 to Ubound (AUTOMATA.Conditions)

12:{ Promela.New Variable(AUTOMATA.Conditions[i]);}

13: //生成進程說明protype.

14: for intj=1 to Ubound (AUTOMATA.States)

15: {Promela.protype[j].Name=AUTOMATA.States[j]. Name;

16:for inth=1 to Ubound(AUTOMATA.Transfer FuntionS)

17: //生成接收消息.

18:{ if (AUTOMATA.Transfer FuntionS[h]. Result== AUTOMATA.States[j])

19:{ Promela.protype[j].AddRecevieMsg(

AUTOMATA.Transfer FuntionS[h].Argument_

State，AUTOMATA.Transfer FuntionS[h].

Argument_Transition); }

20: //生成發送消息并添加發送消息的條件.

21:if (AUTOMATA.Transfer FuntionS[h].

Argument_State==AUTOMATA.States[j])

22:{ Promela.protype[j].Add Send Msg(AUTOMATA.

Transfer FuntionS[h].Argument_Condition，

AUTOMATA.Transfer FuntionS[h].Argument_

State，AUTOMATA. TransferFuntionS[h].

Argument_Transition; } }

23: //生成內部動作action.

24: for inth=1 to Ubound(AUTOMATA. Action FuntionS)

25:{ if(AUTOMATA. Action FuntionS[h]. Result==

AUTOMATA. States[j])

26: { Promela.protype[j].Set Variables True

(AUTOMATA. Action FuntionS[h]. Argument) } }.

3 實例分析

本節以簡化的員工休假審批流程為實例，說明業務流程設計與業務需求的一致性驗證過程.

3.1 員工休假審批流程定義

使用業務流程建模與標注(business process model and notation， BPMN)標準規范描述的員工休假審批業務流程如圖3所示. 休假申請單提交審批后，若休假天數小于等于1 d，由部門領導審批后即可提交人力部歸檔;若休假天數大于1 d小于等于3 d，部門領導批準后，還需人力部領導批準后才可送人力部歸檔;大于3 d的休假申請，需經部門領導、人力部領導批準后，送公司總經理批準后方可送人力部歸檔;最后人力部歸檔，流程結束.

圖3所述流程的14元組定義的部分信息如下:

P=({start_node，…，end_node}，

{writeapply， examine， archive}，

{start， submit， agree， disagree， end}，

{writeapply，…， disagree， end}，

{leavedays<=1，2，…， 3

{t(start_node， start)=applicant，…，

t(superior_leaders，[leavedays<=1]agree)=

hr_staff，…，

t(hr_staff， end)=end_node}，{εn}，

{start_node}， {end_ node}， {εh}，

{φ(submit)=applicant，…， φ(end)=

end_ node}，

{η(submit)=superior_leaders，…，η(disagree)=

applicant}，

α(writeapply)=applicant，…， α(archive)=

hr_staff}， {?}).

3.2 流程的自動機模型

根據算法1構造方法，CDFA模型的部分內容如下:

M=({start_node，applicant，…，hr_staff，

end_node}，

{leavedays<=1，2，…，3

{writeapply，examine， archive}，

{start， submit， agree， disagree， end}，

{(leavedays<=1，agree)， …，

(3< leavedays， agree)}，

{δ(start_node，start)=applicant，…，

δ(superior_leaders，[leavedays<=1]agree)=

hr_staff， …，

δ(hr_staff， end)=end_node}，

{λ(writeapply)=applicant，…，

λ(archive)=hr_staff}，

{start_node}， {end_node}).

其對應的CDFA自動機模型如圖4所示.

3.3 CDFA模型的Promela描述

根據算法2定義的轉換方法，休假審批流程的CDFA模型對應的Promela描述是一個由進程、消息通道、變量和全局對象組成的有限狀態遷移系統，部分片段如下所示.

mtype={start，submit， agree， disagree，end};

chan start_node_chan=[2] of {mtype};……

int leavedays;

bool endflag=false;…….

active proctype start_node()

{start_node_chan!start;}……

active proctype hr_staff ()

{ if :: superior_leaders？agree ->

{ if :: (leavedays<=1)-> hr_staff_chan!end fi; }

:: hr_leaders_chan？agree ->

{ if :: (leavedays>1&&leavedays<=3)->

hr_ staff_chan!end fi; }

:: company_leaders _chan？agree->

{if :: (leavedays>3)-> hr_staff_chan!end fi; } fi; }

active proctype end_node ()

{if :: hr_staff_chan？end -> endflag=true fi; }

3.4 驗證性質

根據員工休假審批流程的需求定義可知:部門領導具有小于等于1 d的休假審批權，人力部領導具有大于1 d,小于等于3 d的休假審批權，公司總經理具有3 d以上假期的審批權.驗證需求選取休假天數為3 d以內，根據需求定義，無需公司總經理進行審批.對應的驗證性質定義為與需求相反的性質，表示為:若休假天數小于3 d并流程辦結已發生，則公司總經理審核同意. 即，如q和s成立則t成立，q表示休假天數小于3 d;s表示流程已辦結;t表示公司總經理審核同意.性質的LTL公式描述為

□((q && s)->□(t)).

(1)

通過驗證，如果CDFA模型不滿足相反的性質，并給出反例路徑，則說明業務流程設計滿足需求，存在可達路徑;如果滿足相反的性質，則說明設計與需求不一致.

3.5 驗證結果

將員工休假審批流程的CDFA模型的Promela描述與待驗證業務需求性質的LTL公式輸入Spin，性質(1)的驗證結果為:設計模型不滿足待驗證性質.如圖6所示.

反例路徑為:queue1(start_node_ chan)->queue2(applicant_chan)->queue3(superior_ leaders_chan)->queue4(hr_heads_chan)->queue5(hr_staff_chan).驗證結果表明:申請人提交小于3 d的休假申請，經部門領導審核同意、人力部領導審核同意、人力部歸檔后完成審批，設計模型滿足“公司總經理無需對小于3 d的員工休假進行審批”的需求.

4 結 論

通過信息化的技術手段實現繁瑣復雜的業務流程自動化是保證企業靈活運行，提高工作效率的關鍵，而對復雜的業務流程進行驗證、測試是一項具有挑戰性的工作. 文中采用CDFA描述業務流程設計模型，使用LTL表示需求，通過模型檢測工具Spin對流程設計與需求的一致性進行驗證. 將其應用于業務流程管理實施中，對提高流程設計質量、提升開發效率具有重要意義，為業務流程正確地運行提供了有效地支持;同時，為下一步從CDFA模型中抽象出測試用例，實現測試腳本的自動生成，提供了依據.

[1] Weber Ingo， Hoffmann Jorg， Mendling Jan. Semantic business process validation[C]∥Proceedings of the 3rd International Workshop on Semantic Business Process Management. Tenerife， Spain: CEUR-WS.org， 2009:22-36.

[2] Qiu Xiaoping， Zheng Jiacheng， Tang Yongchuan， et al. Executive validation analysis of workflow process[C]∥Proceedings of the 5th World Congress on Intelligent Control and Automation. Hangzhou， China: IEEE Press， 2004:2702-2705.

[3] Masalagiu C， Chin W N， Andrei S， et al. A rigorous methodology for specification and Turin verification of business processes[J]. Formal Aspects of Computing， 2009，21(5):495-510.

[4] Van Hee K M， Sidorova N， van der Werf J M. Business process modeling using Petri nets[J]. Transactions on Petri Nets and Other Models of Concurrency VII， 2013,LNCS 7480 :116-161.

[5] 雷麗暉，段振華.一種基于擴展有限自動機驗證組合Web服務的方法[J].軟件學報，2007，18(12):2980-2990.

Lei Lihui， Duan Zhenhua. An extended deterministic finite automata based method for the verification of composite web services[J]. Journal of Software， 2007，18(12):2980-2990. (in Chinese)

[6] Liu Y， Muller S， Xu K. A static compliance checking framework for business process models[J]. IBM Systems Journal， 2006，46(2):335-361.

[7] Yuan M， Huang Z， Li X， et al. Towards a formal verification approach for business process coordination[C]∥Proceedings of 2010 IEEE Eighth International Conference on Web Services. Miami， USA: IEEE Computer Society， 2010:362-368.

[8] 宋寶燕，王菊英，于戈.基于圖形展開及圖形歸約的過程模型驗證方法[J].小型微型計算機系統，2005，26(6):1073-1078.

Song Baoyan， Wang Juying， Yu Ge. Verification method for process model based on graph-spreading and graph-reduction[J]. Mini-Micro Systems， 2005，26(6):1073-1078. (in Chinese)

[9] Wasim Sadiq， Maria E orlowska. Analyzing process models using graph reduction techniques[J]. Information Systems， 2000，25(2):117-134.

[10] Groefsema H， Bucur D. A survey of formal business process verification: from soundness to variability[C]∥Proceedings of International Symposium on Business Modeling and Software Design (BMSD). Noordwijkerhout， the Netherlands: Springer， 2013:198-203.

[11] Michael Hammer， James Champy. Reengineering the corporation: a manifesto for business revolution (collins business essentials)[M]. New York: Harper Collins， 2006.

[12] Jean-Pierre Queille， Joseph Sifakis. Specification and verification of concurrent systems in CESAR[C]∥International Symposium on Programming: 5th Colloquium. Turin， Italy: Spinger， 1982:337-351.

[13] Edmund M， Clarke E， Allen Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic[J]. 25 Years of Model Checking， 2008, LNCS 5000 :196-215.

[14] 林惠民，張文輝.模型檢測:理論、方法與應用[J].電子學報，2002，30(12):1907-1912.

Lin Huimin， Zhang Wenhui. Model checking: theories， techniques and applications[J]. Chinese Journal of Electronics， 2002，30(12):1907-1912. (in Chinese)

[15] Holzmann J. The model checker spin[J]. IEEE Transactions on Software Engineering， 1997，23(5):279-294.

[16] Pnueli Amir. The temporal logic of programs[C]∥Proceedings of the 18th Annual Symposium on Foundations of Computer Science. Providence， USA: IEEE Computer Society， 1977:46-77.

(責任編輯：劉雨)

Formal Design and Verification of Business Processes

DING Ming1，2， ZHANG Shu-ling1， ZHANG Chen3

(1.School of Information and Technology， Northwest University， Xi’an， Shaanxi 710127， China; 2.Xi’an Aeronautics Computing Technique Research Institute， AVIC， Xi’an， Shaanxi 710119， China; 3.School of Computer Science and Technology， Xidian University， Xi’an， Shaanxi 710071， China)

To ensure the consistency of business process design models and business requirements, based on the researches on finite automata model, a quantitative method was proposed in this paper to deal with the construction and verification of business process models. First, the extended conditioned deterministic finite automata were used to describe business process design models and linear temporal logic was used to represent business requirements. Furthermore, the algorithms for transforming the business process design models into automata models and the automata model into Promela were presented. Finally, based on the model checking method, the consistency of the design models and properties were verified with the Spin, if the system models could not satisfy the property, a counter-example and the execution path could be found. Experimental results show that the proposed method is useful in ensuring the correctness of business process design.

business process; deterministic finite automata; model checking; linear temporal logic

2014-09-16

國家自然科學基金資助項目(61502365,61272117);中央高?；究蒲袠I務費專項資金項目(K5051303005)

丁明(1982—)，男，博士生，E-mail:dingmingdm@126.com;張書玲(1957—)，男，教授，博士生導師，E-mail:zh_zhshul@163.com.

TP 311

A

1001-0645(2016)11-1147-07

10.15918/j.tbit1001-0645.2016.11.010