丁明， 張書(shū)玲， 張琛

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

?

業(yè)務(wù)流程的形式化設(shè)計(jì)與驗(yàn)證

丁明1，2， 張書(shū)玲1， 張琛3

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

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

業(yè)務(wù)流程; 確定有限自動(dòng)機(jī); 模型檢測(cè); 線性時(shí)序邏輯

業(yè)務(wù)流程由存在于企業(yè)價(jià)值鏈條上的一系列活動(dòng)及其之間的關(guān)系構(gòu)成，是企業(yè)提高效率和增加效益的重要手段. 為了增強(qiáng)業(yè)務(wù)流程的可靠性，保證設(shè)計(jì)結(jié)果的正確性，避免未經(jīng)過(guò)有效驗(yàn)證的流程設(shè)計(jì)被開(kāi)發(fā)、測(cè)試、甚至交付使用，造成返工修改，浪費(fèi)大量的人力和物力，可應(yīng)用形式化方法進(jìn)行模型驗(yàn)證，確保流程設(shè)計(jì)與需求的一致性.

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

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

1 業(yè)務(wù)流程建模

1.1 業(yè)務(wù)流程

Michael Hammer與James Champy給出了業(yè)務(wù)流程的經(jīng)典定義:定義某一組活動(dòng)為一個(gè)業(yè)務(wù)流程，這組活動(dòng)有一個(gè)或多個(gè)輸入，輸出一個(gè)或多個(gè)結(jié)果，這些結(jié)果對(duì)客戶來(lái)說(shuō)是一種增值[11]. 典型的業(yè)務(wù)流程包括:輸入資源，按一定規(guī)則執(zhí)行的活動(dòng)，活動(dòng)之間的相互關(guān)系和作用(即結(jié)構(gòu))，輸出結(jié)果，顧客，流程創(chuàng)造的價(jià)值，表示方式如下.

定義1(業(yè)務(wù)流程) 業(yè)務(wù)流程用一個(gè)14元組表示，

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

式中:O為業(yè)務(wù)流程在交互過(guò)程中所有參與主體的集合;Ao為主體執(zhí)行的不會(huì)引發(fā)遷移的活動(dòng)，可為空，表示為εv;At為主體執(zhí)行的會(huì)引起遷移的活動(dòng)，可為空，表示為εx;A為交互過(guò)程中所有活動(dòng)的集合，A=Ao∪At;C為遷移約束條件的集合，可為空，表示為εc;t為主體之間交互的遷移函數(shù)，O×(At×C)→O;N為被調(diào)用操作的集合，可為空，表示為εn;s為開(kāi)始節(jié)點(diǎn);E為終止節(jié)點(diǎn)的集合;H為后繼流程的集合，可為空，表示為εh;φ為從At到O的一個(gè)函數(shù)關(guān)系，φ(at)∈O，at∈At，表示活動(dòng)at的發(fā)送主體;η為從At到O的一個(gè)函數(shù)關(guān)系，η(at)∈O，at∈At，表示活動(dòng)at的接受主體;α為從Ao到O的一個(gè)函數(shù)關(guān)系，α(ao)∈O，ao∈Ao， 表示活動(dòng)ao所對(duì)應(yīng)的主體;β為從E到H的一個(gè)函數(shù)關(guān)系，β(h)∈E，h∈H，表示后繼流程h對(duì)應(yīng)的終止節(jié)點(diǎn)，β(εh)=?.

此處以圖1所示的簡(jiǎn)單流程為例，說(shuō)明業(yè)務(wù)流程的14元組定義過(guò)程. 圖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 業(yè)務(wù)流程的自動(dòng)機(jī)模型

CDFA是擴(kuò)展的帶約束條件的確定有限自動(dòng)機(jī)，用以形式化描述業(yè)務(wù)流程. CDFA的狀態(tài)對(duì)應(yīng)表達(dá)業(yè)務(wù)流程中各活動(dòng)的主體，狀態(tài)遷移描述了業(yè)務(wù)流程主體之間的交互. 遷移用二元組標(biāo)注，包括所發(fā)生的事件和事件發(fā)生的約束條件. 狀態(tài)遷移表示對(duì)象接受或者發(fā)送滿足約束條件的消息，按給定的轉(zhuǎn)移函數(shù)從一個(gè)狀態(tài)轉(zhuǎn)移到另一狀態(tài). CDFA 可以準(zhǔn)確表達(dá)業(yè)務(wù)流程中各活動(dòng)的輸入、輸出、相互關(guān)系以及活動(dòng)間的遷移. 以下給出了CDFA的9元組定義.

定義2(CDFA) 帶約束條件的確定有限自動(dòng)機(jī)M是一個(gè)9元組，

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

式中:Q為狀態(tài)非空的有窮集合，?q∈Q，q稱為自動(dòng)機(jī)M的一個(gè)狀態(tài);R為動(dòng)作的約束條件集合，可為空，表示為ε;V為狀態(tài)內(nèi)部動(dòng)作的集合;X為交互動(dòng)作的集合;Σ為輸入字母表，輸入字符串都是Σ上的字符串，Σ={(r，x)| r∈R，x∈X};δ表示狀態(tài)轉(zhuǎn)移函數(shù)，Q×Σ→Q;λ是從V到Q的一個(gè)函數(shù)關(guān)系，λ(v)∈Q，v∈V，表示內(nèi)部動(dòng)作v所對(duì)應(yīng)的狀態(tài);q0表示M的初始狀態(tài)，q0∈Q;F表示M的終止?fàn)顟B(tài)集合，F(xiàn)?Q.

通過(guò)以下轉(zhuǎn)換規(guī)則構(gòu)造業(yè)務(wù)流程CDFA模型.

定義3 業(yè)務(wù)流程的CFDA模型構(gòu)造算法.

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

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

算法1 構(gòu)造業(yè)務(wù)流程的CDFA模型.

輸入:業(yè)務(wù)流程的14元組描述.

輸出:業(yè)務(wù)流程的CDFA模型.

① 創(chuàng)建初始狀態(tài)q0=s;

② 狀態(tài)集合Q=O，每個(gè)狀態(tài)與業(yè)務(wù)流程中的一個(gè)主體相對(duì)應(yīng);

③ 約束條件集合R=C;

④ 狀態(tài)內(nèi)部動(dòng)作集合V=Ao;

⑤ 交互動(dòng)作集合X=At;

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

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

⑧ 狀態(tài)轉(zhuǎn)移函數(shù)δ(q，(r，x))∈Q，?q∈Q，δ(q，(r，x))=t(q，(r，x));

⑨ 終止?fàn)顟B(tài)集合F=E，每個(gè)終止?fàn)顟B(tài)與業(yè)務(wù)流程中的一個(gè)終止節(jié)點(diǎn)相對(duì)應(yīng).

2 業(yè)務(wù)流程驗(yàn)證

通過(guò)模型檢測(cè)技術(shù)，驗(yàn)證業(yè)務(wù)流程設(shè)計(jì)模型與業(yè)務(wù)需求性質(zhì)之間的一致性. 模型檢測(cè)[12-14]是一種針對(duì)系統(tǒng)屬性驗(yàn)證的形式化方法，已被廣泛應(yīng)用于軟/硬件、通信、安全等方面. 模型檢測(cè)用狀態(tài)遷移系統(tǒng)描述系統(tǒng)的行為，能夠?qū)τ懈F狀態(tài)系統(tǒng)的各類復(fù)雜的時(shí)序性質(zhì)進(jìn)行驗(yàn)證，當(dāng)判斷某性質(zhì)不被滿足時(shí)能夠提供反例，以便定位設(shè)計(jì)錯(cuò)誤.

2.1 業(yè)務(wù)流程驗(yàn)證方法

本文使用由貝爾實(shí)驗(yàn)室開(kāi)發(fā)的模型檢測(cè)工具Spin[15](simple Promela interpreter)進(jìn)行一致性驗(yàn)證，工具通過(guò)Promela語(yǔ)言描述系統(tǒng)模型，采用線性時(shí)序邏輯[16](linear-time temporal logic， LTL)定義待驗(yàn)證的性質(zhì). 驗(yàn)證過(guò)程如圖2所示，首先采用14元組定義業(yè)務(wù)流程;其次根據(jù)定義3的構(gòu)造算法將業(yè)務(wù)流程轉(zhuǎn)換為帶約束條件的確定有限自動(dòng)機(jī)模型，并使用Promela語(yǔ)言描述;然后定義業(yè)務(wù)需求待驗(yàn)證性質(zhì)的LTL公式;最后將Promela描述的模型與LTL定義的需求性質(zhì)輸入驗(yàn)證工具Spin. Spin對(duì)兩者的一致性進(jìn)行模擬校驗(yàn)，如發(fā)現(xiàn)違背性質(zhì)的任何反例，輸出驗(yàn)證結(jié)果為業(yè)務(wù)流程設(shè)計(jì)不滿足需求;如未發(fā)現(xiàn)反例，說(shuō)明流程設(shè)計(jì)與需求一致.

2.2 業(yè)務(wù)流程自動(dòng)機(jī)模型到Promela描述的轉(zhuǎn)換

Promela是一種類C程序語(yǔ)言的抽象語(yǔ)言，用于描述通信協(xié)議或分布式系統(tǒng)，可對(duì)有限狀態(tài)系統(tǒng)進(jìn)行形式化建模. Promela描述的模型是一個(gè)有限轉(zhuǎn)換系統(tǒng)，由進(jìn)程、消息通道、變量和全局對(duì)象組成，進(jìn)程之間相互通信，每個(gè)進(jìn)程都可看作是擴(kuò)展的有限自動(dòng)機(jī).

業(yè)務(wù)流程的CDFA模型向Promela描述進(jìn)行轉(zhuǎn)換的算法實(shí)現(xiàn)如下:

算法2 CDFA模型到Promela描述轉(zhuǎn)換算法.

輸入:業(yè)務(wù)流程的CDFA模型.

輸出:CDFA模型的Promela描述.

1: //生成mytype類型說(shuō)明.

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

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

4://生成chan msg 通道說(shuō)明定義.

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

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

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

7: //內(nèi)部動(dòng)作為布爾型，初始值false，表示動(dòng)作未執(zhí)行.

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

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

10: //將所有約束條件定義為相應(yīng)的變量.

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

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

13: //生成進(jìn)程說(shuō)明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: //生成發(fā)送消息并添加發(fā)送消息的條件.

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: //生成內(nèi)部動(dòng)作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 實(shí)例分析

本節(jié)以簡(jiǎn)化的員工休假審批流程為實(shí)例，說(shuō)明業(yè)務(wù)流程設(shè)計(jì)與業(yè)務(wù)需求的一致性驗(yàn)證過(guò)程.

3.1 員工休假審批流程定義

使用業(yè)務(wù)流程建模與標(biāo)注(business process model and notation， BPMN)標(biāo)準(zhǔn)規(guī)范描述的員工休假審批業(yè)務(wù)流程如圖3所示. 休假申請(qǐng)單提交審批后，若休假天數(shù)小于等于1 d，由部門(mén)領(lǐng)導(dǎo)審批后即可提交人力部歸檔;若休假天數(shù)大于1 d小于等于3 d，部門(mén)領(lǐng)導(dǎo)批準(zhǔn)后，還需人力部領(lǐng)導(dǎo)批準(zhǔn)后才可送人力部歸檔;大于3 d的休假申請(qǐng)，需經(jīng)部門(mén)領(lǐng)導(dǎo)、人力部領(lǐng)導(dǎo)批準(zhǔn)后，送公司總經(jīng)理批準(zhǔn)后方可送人力部歸檔;最后人力部歸檔，流程結(jié)束.

圖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 流程的自動(dòng)機(jī)模型

根據(jù)算法1構(gòu)造方法，CDFA模型的部分內(nèi)容如下:

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}).

其對(duì)應(yīng)的CDFA自動(dòng)機(jī)模型如圖4所示.

3.3 CDFA模型的Promela描述

根據(jù)算法2定義的轉(zhuǎn)換方法，休假審批流程的CDFA模型對(duì)應(yīng)的Promela描述是一個(gè)由進(jìn)程、消息通道、變量和全局對(duì)象組成的有限狀態(tài)遷移系統(tǒng)，部分片段如下所示.

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 驗(yàn)證性質(zhì)

根據(jù)員工休假審批流程的需求定義可知:部門(mén)領(lǐng)導(dǎo)具有小于等于1 d的休假審批權(quán)，人力部領(lǐng)導(dǎo)具有大于1 d,小于等于3 d的休假審批權(quán)，公司總經(jīng)理具有3 d以上假期的審批權(quán).驗(yàn)證需求選取休假天數(shù)為3 d以內(nèi)，根據(jù)需求定義，無(wú)需公司總經(jīng)理進(jìn)行審批.對(duì)應(yīng)的驗(yàn)證性質(zhì)定義為與需求相反的性質(zhì)，表示為:若休假天數(shù)小于3 d并流程辦結(jié)已發(fā)生，則公司總經(jīng)理審核同意. 即，如q和s成立則t成立，q表示休假天數(shù)小于3 d;s表示流程已辦結(jié);t表示公司總經(jīng)理審核同意.性質(zhì)的LTL公式描述為

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

(1)

通過(guò)驗(yàn)證，如果CDFA模型不滿足相反的性質(zhì)，并給出反例路徑，則說(shuō)明業(yè)務(wù)流程設(shè)計(jì)滿足需求，存在可達(dá)路徑;如果滿足相反的性質(zhì)，則說(shuō)明設(shè)計(jì)與需求不一致.

3.5 驗(yàn)證結(jié)果

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

反例路徑為:queue1(start_node_ chan)->queue2(applicant_chan)->queue3(superior_ leaders_chan)->queue4(hr_heads_chan)->queue5(hr_staff_chan).驗(yàn)證結(jié)果表明:申請(qǐng)人提交小于3 d的休假申請(qǐng)，經(jīng)部門(mén)領(lǐng)導(dǎo)審核同意、人力部領(lǐng)導(dǎo)審核同意、人力部歸檔后完成審批，設(shè)計(jì)模型滿足“公司總經(jīng)理無(wú)需對(duì)小于3 d的員工休假進(jìn)行審批”的需求.

4 結(jié) 論

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

[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] 雷麗暉，段振華.一種基于擴(kuò)展有限自動(dòng)機(jī)驗(yàn)證組合Web服務(wù)的方法[J].軟件學(xué)報(bào)，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] 宋寶燕，王菊英，于戈.基于圖形展開(kāi)及圖形歸約的過(guò)程模型驗(yàn)證方法[J].小型微型計(jì)算機(jī)系統(tǒng)，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] 林惠民，張文輝.模型檢測(cè):理論、方法與應(yīng)用[J].電子學(xué)報(bào)，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.

(責(zé)任編輯：劉雨)

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

國(guó)家自然科學(xué)基金資助項(xiàng)目(61502365,61272117);中央高?；究蒲袠I(yè)務(wù)費(fèi)專項(xiàng)資金項(xiàng)目(K5051303005)

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

TP 311

A

1001-0645(2016)11-1147-07

10.15918/j.tbit1001-0645.2016.11.010