丁明， 張書玲， 張琛

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

?

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

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

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

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

業(yè)務(wù)流程; 確定有限自動機; 模型檢測; 線性時序邏輯

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

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

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

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

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

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

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

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

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

此處以圖1所示的簡單流程為例，說明業(yè)務(wù)流程的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 業(yè)務(wù)流程的自動機模型

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

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

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

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

通過以下轉(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，φ，η，α，β)，對應(yīng)的帶約束條件的確定有限自動機M可表示為一個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，每個狀態(tài)與業(yè)務(wù)流程中的一個主體相對應(yīng);

③ 約束條件集合R=C;

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

⑤ 交互動作集合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，每個終止?fàn)顟B(tài)與業(yè)務(wù)流程中的一個終止節(jié)點相對應(yīng).

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

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

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

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

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

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

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

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

輸入:業(yè)務(wù)流程的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: //內(nèi)部動作為布爾型，初始值false，表示動作未執(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: //生成進程說明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)部動作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 實例分析

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

3.1 員工休假審批流程定義

使用業(yè)務(wù)流程建模與標(biāo)注(business process model and notation， BPMN)標(biāo)準(zhǔn)規(guī)范描述的員工休假審批業(yè)務(wù)流程如圖3所示. 休假申請單提交審批后，若休假天數(shù)小于等于1 d，由部門領(lǐng)導(dǎo)審批后即可提交人力部歸檔;若休假天數(shù)大于1 d小于等于3 d，部門領(lǐng)導(dǎo)批準(zhǔn)后，還需人力部領(lǐng)導(dǎo)批準(zhǔn)后才可送人力部歸檔;大于3 d的休假申請，需經(jīng)部門領(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 流程的自動機模型

根據(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}).

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

3.3 CDFA模型的Promela描述

根據(jù)算法2定義的轉(zhuǎn)換方法，休假審批流程的CDFA模型對應(yīng)的Promela描述是一個由進程、消息通道、變量和全局對象組成的有限狀態(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 驗證性質(zhì)

根據(jù)員工休假審批流程的需求定義可知:部門領(lǐng)導(dǎo)具有小于等于1 d的休假審批權(quán)，人力部領(lǐng)導(dǎo)具有大于1 d,小于等于3 d的休假審批權(quán)，公司總經(jīng)理具有3 d以上假期的審批權(quán).驗證需求選取休假天數(shù)為3 d以內(nèi)，根據(jù)需求定義，無需公司總經(jīng)理進行審批.對應(yīng)的驗證性質(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)

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

3.5 驗證結(jié)果

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

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

4 結(jié) 論

通過信息化的技術(shù)手段實現(xiàn)繁瑣復(fù)雜的業(yè)務(wù)流程自動化是保證企業(yè)靈活運行，提高工作效率的關(guān)鍵，而對復(fù)雜的業(yè)務(wù)流程進行驗證、測試是一項具有挑戰(zhàn)性的工作. 文中采用CDFA描述業(yè)務(wù)流程設(shè)計模型，使用LTL表示需求，通過模型檢測工具Spin對流程設(shè)計與需求的一致性進行驗證. 將其應(yīng)用于業(yè)務(wù)流程管理實施中，對提高流程設(shè)計質(zhì)量、提升開發(fā)效率具有重要意義，為業(yè)務(wù)流程正確地運行提供了有效地支持;同時，為下一步從CDFA模型中抽象出測試用例，實現(xiàn)測試腳本的自動生成，提供了依據(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] 雷麗暉，段振華.一種基于擴展有限自動機驗證組合Web服務(wù)的方法[J].軟件學(xué)報，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].小型微型計算機系統(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] 林惠民，張文輝.模型檢測:理論、方法與應(yīng)用[J].電子學(xué)報，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

國家自然科學(xué)基金資助項目(61502365,61272117);中央高校基本科研業(yè)務(wù)費專項資金項目(K5051303005)

丁明(1982—)，男，博士生，E-mail:dingmingdm@126.com;張書玲(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