丁明， 张书玲， 张琛

(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);中央高校基本科研业务费专项资金项目(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