业务协同中组织需求的建模与一致性验证

笪 建，莫 启，程耀坤,张 毅，李 彤

(1.云南大学 软件学院，云南 昆明 650091；2.云南大学 云南省软件工程重点实验室，云南 昆明 650091；3.淮安开放大学 信息工程系，江苏，淮安 223001;4.江苏联合职业技术学院淮安分院 现代教育技术中心 223001)

0 引言

随着全球经济化的发展和企业信息化程度的不断提高，企业的经营模式发生了重大变化，企业的业务活动已从企业内单目标为导向的独立发展模式发展成为跨企业多目标合作的协同模式[1]。在现代商业环境下，没有一个企业是孤立的[2-3]。企业作为参与者参与到协作中，在协作过程中，它们彼此进行交互以完成特定业务功能。近年来，随着互联网成为主流的计算平台，尤其是面向服务计算(Service-Oriented Computing, SOC)的快速兴起，使得不同组织业务过程间的交互成为可能，如企业信息系统[4]、电子商务[5]等。为实现共同的商业目标，每个组织的业务过程通常需要跨越组织边界，同其他组织的业务过程进行交互和协作，以形成相对稳定的过程视图。学术界和工业界称这种存在复杂交互和协作关系的业务过程为协同业务过程[6]。为确保协同业务过程实施的正确性，在设计阶段对协同业务过程进行建模与验证是当前业务过程管理(Business Process Management, BPM)领域研究的热点。

针对协同业务过程，已有研究工作大多围绕如何构建支持个性化特征的协同业务过程开展，如文献[7-8]，并以此为基础对相关性质(如弱合理性等)进行验证，如文献[9]。而事实上，衡量协同业务过程质量的因素除了模型本身无歧义、一致性和无错误等性质外，更重要的是其能否充分满足参与组织需求。一些研究者注意到了上述问题，并基于目标模型提出了业务过程需求一致性验证方法，如文献[10]，但这些方法仅针对单个业务流程。协同业务过程中含有多个参与组织流程，这些流程间相互通信合作，共同推进全局流程演进[11]。由于上述方法没有考虑多流程间协作的情形，很难应用于跨组织环境下的需求一致性验证。解决协同业务过程需求一致性问题面临以下挑战：①如何准确地描述跨组织环境下的需求；②如何形式化建模支持需求分析的协同业务过程；③如何验证协同业务过程与需求保持一致。

本文借鉴经典需求工程中目标模型[12]的思想，并基于模型检测技术提出一种验证协同业务过程与参与组织需求一致性的方法。该方法将参与组织需求以类似目标模型方式构建，并将其和协同业务过程分别转化为以线性时序逻辑公式(Linear Temporal Logic, LTL)描述性质和可形式验证的模型，借助模型检测技术实现需求一致性自动验证。

本文主要贡献如下：

(1)借鉴经典需求工程中目标模型思想，提出了需求依赖图(Requirement Dependence Graph, RDG)来显式刻画参与组织需求间依赖关系，通过分析协同业务过程特性[11]给出跨组织环境下原子需求定义。

(2)采用Petri网建模参与组织业务过程，引入并发操作符提供一种通过组合参与组织业务过程构建协同业务过程的方法。提出需求产生式用来刻画需求随任务执行产生规则。在明确需求产生规则前提下，以任务执行为驱动提出了协同业务过程执行语义，以支持需求一致性验证。

(3)基于模型检测技术提出需求一致性验证框架。从迹等价[13]角度证明了协同业务过程与转换生成NuSMV规约间在参与组织需求层面具有一致检测结果，并给出将参与组织需求自动转换成LTL公式的算法。以此为基础借助NuSMV实现了参与组织需求自动验证。

(4)结果表明，相对已有工作，本文方法不仅可直接应用于建模跨组织需求和支持需求分析过程模型，还可更加有效地刻画参与组织需求和验证需求一致性。

1 相关研究

目前国内外研究者就协同业务过程建模与验证开展了一系列相关工作。

在协同业务过程建模方面，文献[14]将Petri网和Pi演算交叉应用，提出一种协同业务过程的建模方法以支持协同业务过程具有面向流程组合的特性。为了保护参与组织内部流程信息，文献[8]首先提出一组元结构，然后针对每种元结构提出各自的约简规则，得到参与组织的公共视图，将公共视图进行组合从而得到跨组织协同的信息流网结构，即协同业务过程。文献[15]基于Petri网提出一种多视角的跨组织业务过程建模方法。该方法从内部视角定义私有过程，进而通过抽取规则集生成公共过程，将公共过程组合生成协作过程。文献[16]引入了过程视图概念，过程视图由投影规则(如灰盒投影、白盒投影等)从私有过程中生成，它隐藏了私有业务过程中无关的信息，仅暴露相关协作信息，可视为私有过程的外部映像。进而通过将过程视图组合得到协同业务过程。然而，这些研究工作关注的重点是如何构建支持个性化特征[11](如面向流程组合、隐私等)的协同业务过程模型，没有讨论协同业务过程验证。

在协同业务过程形式验证中，文献[7]较早在国际上提出了跨组织工作流网(Inter-Organizational WorkFlow, IOWF)用于建模跨组织工作流，并基于传统的合理性定义了IOWF的正确性。在此基础上，国内外研究者开展了相关研究。文献[17]采用Petri网和Pi演算分别对协同业务过程的本地控制流及控制流间交互协议进行建模，并基于Petri网可达图建立了本地控制流和交互协议间的关联关系；然后，定义了协同业务过程逻辑结构的正确性，进而提出了逻辑结构正确性验证方法。为了避免形式验证中状态空间爆炸问题，文献[9]提出一种协同业务过程模型，即利用面向交互的Petri网(Interaction-Oriented Petri Nets, IOPN)用于描述参与组织间业务协同；然后，引入IOPN弱合理性概念用来定义IOPN的逻辑结构正确性，并基于不变量分解方法将一个弱合理的无回路IOPN分解为一组顺序图用于验证其逻辑结构正确性。文献[6]针对跨部门业务协同呈现出的复杂特性，对WF-net扩展资源和消息等要素来建模参与部门的业务流程，然后使用库所融合技术将资源库所和消息库所融合以得到跨部门协调业务过程模型。以传统合理性为基础定义了协调业务过程模型正确性标准，并基于可达图给出协同业务过程正确性分析方法。为了有效地存储和描述互操作需求，文献[18]首先提出一种领域描述语言用来描述互操作需求，继而将描述需求自动转换为时间计算树逻辑(Time Computation Tree Logic, TCTL)，并采用时间自动机网络(Timed Automata Network, TAN)建模协同业务过程。通过UPPAAL实现互操作需求的自动验证。然而，以上工作重点关注协同业务过程逻辑结构正确性或互操作方面需求，并未考虑参与组织共性及个性需求这一重要因素。

为此，国内外研究者提出了一些关于需求形式验证的方法。为支持用户需求意图表达，文献[19]提出一种基于目标感知的可配置业务流程分析方法。该方法将用户需求与业务过程进行融合，进而通过增加配置操作将用目标工作流网(Goal WF-net, GWF-net)表达的业务过程转化为符合用户个性化需求的流程模型。为确保业务过程满足用户特定需求，文献[10]提出一种目标模型与过程模型一致性验证方法。该方法采用目标模型对用户需求进行建模，PZN(Z+Petri Net)模型用于刻画业务过程，继而基于PZN模型活动路径来验证是否满足目标模型。尽管文献[10]和文献[19]对用户需求与业务过程模型一致性问题进行了讨论，但这些工作仅局限于组织内单个业务过程，未涉及业务过程间协作，不适用于跨组织环境下需求一致性验证。考虑到目标能够良好地反映参与组织需求意图，文献[20]基于面向目标业务过程提出一种分布式的协同业务过程监控与管理方法。该方法通过实时收集业务过程中任务执行的相关目标信息实现挖掘分析。尽管文献[20]阐述了利用目标进行协同业务过程建模、分析及监控的重要性，但对于如何验证协同业务过程与需求的一致性没有进行讨论。

2 组织需求和协同业务过程建模

本章对参与组织需求和协同业务过程的建模方法进行详细阐述。

2.1 需求依赖图RDG

传统目标模型能够良好地描述需求间存在的例化和分解关系[12]。通过扩展目标模型，本文提出需求依赖图RDG来描述参与组织期望需求。在RDG中，根据构建参与组织需求的需要，增加Pre依赖来表达需求间存在的时序关系，同时添加XOR依赖来进一步表示现实中需求间存在的互斥关系。在RDG中，需求可分为原子需求和组合需求两类，原子需求是建模参与组织需求的最小粒度，而组合需求通常可分解为一组原子需求集合。

特别地，RDG中需求之间存在的依赖关系可从垂直和水平两个角度区分：①从垂直视角，需求之间的依赖关系可分为与分解关系和或分解关系，用于将高层次需求(即概念需求)逐层细化成低层次需求(其中最底层需求是消息，表示实际交互行为)，为参与组织提供一种逐层细化其意图方法，降低建模复杂性；②从水平视角，需求之间的依赖关系可分为前驱关系和互斥关系，分别用于描述协同业务过程中交互发生的先后关系和互斥关系。例如，在京东或苏宁网购中，店主通常要求客户先付款后发货。如果缺少前驱关系Pre，则参与组织就不能表达出这种诉求。同时，客户在支付过程中只能使用一种支付方式(如支付宝、微信及网银等)，因此利用互斥关系就能够描述出客户支付方式互斥需求。RDG的形式定义如下。

定义1RDG是一个3元组G=(V,E,φ)，其中：

(1)V为节点有限集合，表示参与组织需求集合。

(2)E:V×V为节点间存在有向边集。

(3)标注函数φ:E×{AND,OR,XOR,Pre}用来标识有向边类型，这些类型包括与分解关系(AND)、或分解关系(OR)、异或分解关系(XOR)和前驱关系(Pre)。

定义1中，RDG中每个节点表示一个需求。原子需求在V中映射为叶子节点(原子需求定义参见定义3)，而组合需求对应非叶子节点，它由原子需求或低层次组合需求通过分解关系构成；节点间有向边表示需求间存在依赖关系；边上的标记为依赖关系类型。为了方便表述需求间依赖关系，若需求R由{R1,…,Rn}通过AND分解组成，则记为R=R1&…&Rn，表示当R1,…,Rn全部完成时R才能完成；若需求R由{R1,…,Rn}通过OR分解组成，则记为R=R1‖…‖Rn，表示当R1,…,Rn中有一个或多个完成时R才能完成；若需求Ri，Rj满足Pre关系，则记为Ri→Rj，表示当Rj完成时Ri已经完成；若需求Ri，Rj满足XOR关系，则记为Ri⊗Rj，表示Ri和Rj间是异或关系，即两者只能取其一。

进一步以G为基础，参与组织需求良构性定义如下。

定义2参与组织需求良构性。当且仅当R对应的需求依赖图G=(V,E,φ)满足如下条件，称参与组织需求R具有良构性：

(1)存在唯一根需求root，满足对于∀v∈V，(v,root)∉V。

(2)对于∀vi∈V，若ei1=(vi,vi1),…,ein=(vi,vin)∈E且φ(eij)∈{AND,OR}，则φ(ei1)=…=φ(ein)。

(3)若∃e=(vi,vj)∈E且φ(e)=Pre，则∃v∈V，ei=(v,vi)，ej=(v,vj)∈E，使得φ(ei)=φ(ej)=AND。

(4)若∃e=(vi,vj)∈E且φ(e)=XOR，则∃v∈V，ei=(v,vi)，ej=(v,vj)∈E，使得φ(ei)=φ(ej)=OR。

(5)G不存在环结构。

定义2中，条件(2)要求每次分解类型必须相同；条件(3)要求前驱关系只能指定由与分解得到的同一层次上不同需求执行先后关系；条件(4)要求互斥关系只能指定由与分解得到的同一层次上不同需求执行互斥关系；条件(5)要求G中不存在环结构，避免出现循环分解和循环前驱。

其中：条件(2)和条件(5)与经典需求模型保持一致[12]；条件(3)和条件(4)是受到文献[21]启发提出，即文献[21]认为在实际建模中约束关系(即Pre关系和XOR关系)主要定义在同一层次。同时，也方便后文将以RDG描述需求转换为LTL公式。在实际应用中，约束关系也可能分布在RDG中的不同层次，这将在下一步工作中详细讨论。

在实际应用中，参与组织需求通常由协同业务过程执行情况确定。以参与组织内部任务执行为驱动，协同业务过程行为在参与组织间表现为消息传递[11]。此外，跨组织环境下消息传递具有异步特性，使得在协作中产生多种消息状态。一条消息及其在某个时刻所处状态是参与组织观察协同业务过程执行情况的最小粒度。为此本文将消息及其状态进行组合来表示原子需求。

由于原子需求中涉及消息状态，本文通过对任务与消息交互过程进行分析，将消息状态进行统一抽象，如图1所示。

对于任意消息(message)，开始时其处于未生成状态(inactive)；在任务task(任务定义参见定义2)执行完成并发送消息message后(消息生成由任务内部执行确定，任务执行在本文中认为是原子的，故产生状态没有显示列出)，其处于投递状态(delivered)；之后若message没有被接收则将处于等待接收状态(pending)；一旦message被接收则将处于接收状态(received)。

本文默认协同业务过程执行处于一个足够良好的通信环境中，即若一个参与组织发生一条消息，则请求该消息的组织一定可以在规定时间内被接受，不存在消息有效性时长问题。这种假设在协同业务过程的形式验证中是合理的[22]。

在明确消息状态的前提下，将原子需求定义如下。

定义3原子需求是2元组atomic=(msg,state)，其中：

(1)msg为消息。

(2)state∈{inactive,delivered,pending,received}为消息所处状态。

在实际应用中，参与组织的需求由组织间协商得到，进而可采用RDG进行描述。特别地，需求获取是一个循环迭代的过程，如何迭代求精获取需求可参考文献[23]。限于篇幅，本文后续讨论中的需求均指经反复协商得到的最终需求。

在跨组织环境下，参与组织需求可能有天然的不一致性，通常可分为需求冗余和需求冲突两类[24]。前者是指存在一个需求，该需求可由其他需求推出，对这种需求进行分析没有必要，而后者则是指针对两种需求，协同业务过程无法同时满足，导致对其分析是徒劳的。文献[24]对如何消除这两类需求不一致性进行了较为详细的讨论。限于篇幅，本文后续讨论中的需求均指无冗余和无冲突的需求。此外，文献[23]也认为需求不一致性并不限于需求冗余和需求冲突两类。由于本文主要关注需求定义及需求与模型一致性分析，如何进一步消除需求间存在的不一致性将在进一步的工作中详细讨论。

2.2 协同业务过程

业务过程是参与组织流程信息的本地定义，由该组织自治管理。业务过程由参与组织任务集和建立其上的控制流组成，是构建协同业务过程的基础。

任务是组织为完成特定业务目标开展的业务活动，其形式定义如下。

(1)name是任务名字，唯一标识组织内一个任务。

(2)org是任务所属的组织。

(3)MsgRec是任务执行前需接收的消息集合。

(4)MsgSend是任务执行完成后发送消息集合。

对于任意任务task，task.MsgRec为task接收消息集合；task.MsgSend为task发送消息集合。

本文采用Petri网对业务过程控制流进行建模。进一步地，将以Petri网建模控制流中每个变迁关联一个任务从而得到业务过程。有关Petri网详细内容参见文献[25]。业务过程形式定义如下。

定义5业务过程是一个三元组BP=(Tasks,Flow,f)，其中：

(1)Tasks是有限任务集，对于∀task∈Tasks，task是符合定义4的任务。

(2)Flow为控制流，它是一个基本Petri网Flow=(P,T;F,M0,i,o)，其中：P是有限库所集；T是有限变迁集；F⊆(P×T)∪(T×P)是流关系；M0是初始标识，满足∀p∈P，p≠i：M0(p)=0且M0(i)=1；i和o是两个特殊库所，分别表示开始库所和终止库所。

在平时的教学中，我们要培养勤于思考的良好习惯，对人对事都要有自己的见解。譬如，在指导学生写一篇关于“门”的话题作文时，我们可引导他们进行思维发散。可写有形的门，如家门、校门、城门等；也可写无形的门，如科学之门、心灵之门等；可写门内的世界，也可写门外的世界；可写开门的意义，也可写关门的意义；可从身边的小事引发对“门”的感受与收获，可以由“门”联系历史事实去发表看法，也可以由“门”的自然属性阐发哲理。我们还可以引导学生大胆指点教材，激扬文字，增加自信。教师不妨开几节欣赏课，采用逆向教学，让学生开怀评点教材中的不足之处，或主题，或构思，或语言，或逻辑，每人讲那么一两点，并敢于对名家名篇“开刀”。

(3)f:T→Tasks是变迁映射函数，表示每个变迁关联一个任务。

以业务过程为基础可定义协同业务过程。由于进程代数能够自然地以模块的方式构建复杂的交互并发系统[26]，借鉴其思想，本文引入并发操作符的概念，并发操作符提供一种通过组合参与组织业务过程构建协同业务过程方法。

定义6协同业务过程。设参与协同的业务过程为BP1,…,BPn，由这n个业务过程构成的协同业务过程记为CBP=BP1‖…‖BPn。

定义6只是将多个业务流程在形式上列为并发关系，其间存在协作关系，可按实际场景定义。本文仅考虑业务过程中存在的异步消息通信关系(参见定义10)。实际中，业务过程中可能还存在同步等情形，即一个协作实现需要多个任务同时参与完成，这将在后续工作中进行详细讨论。

本文引入格局的概念来表示协同业务过程状态，它由每个参与组织运行状态及协作中产生消息组成，其形式定义如下。

(2)MS为消息状态，即c中当前含有消息集合。

对于任意格局r，r[i]为格局中业务过程BPi的运行状态，r.MS为r当前含有消息集。

可对格局运行状态或消息进行替换，格局运行状态替换和格局信息替换定义如下。

定义协同业务过程语法规则之后，对协同业务过程执行语义进行讨论。

本质上，协同业务过程执行语义刻画由任务执行引起的格局转换的过程。为支持需求一致性验证，执行语义中还需考虑参与组织需求。结合图1所示的消息状态抽象和任务定义，本文引入需求产生式概念来刻画参与组织需求随任务执行产生规则。需求产生式如表1所示。

表1 需求产生式

表中：规则R1是指若存在需求r=(msg,inactive)，在任务task执行完成并发送消息msg后则产生需求r′=(msg,delivered)；规则R3和规则R4可按类似规则R1方式解释；规则R2是指若存在需求r=(msg,delivered)，在任务task执行完成，且未接收消息msg后则产生需求r′=(msg,pending)。

在明确需求产生规则之后，结合任务定义和格局可定义协同业务过程执行语义。

(1)S为有穷格局集合。

(2)s0为初始格局。

(3){task,R}中R为任务task关联原子需求集合，表示在task完成后所达到的需求。

1)·task⊆r[i]∧task.MsgRec⊆r.MS，表示若task可以执行，则其使能且需要接收的消息均满足；

2)s=r[M′/M]i∧s=r[MS′/MS]，表示若task执行完成后，格局r中BPi的运行状态以及消息状态分别更新为M′=(M-·task)∪task·和MS′=(MS-task.MsgRec)∪task.MsgSend；

3)∀msg∈task.MsgRec∪task.MsgSend，若∃μ∈Δ且μ.msg=msg，按需求产生式更新后为μ′，则μ′∈R且Δ=(Δ-μ)∪{μ′}。

由于协同业务过程执行语义采用LTS描述，故可将其转换为其他模型检测工具可以识别的规约(如SMV、Promela等)进行形式分析，从而判别出协同业务过程是否与期望需求一致。

3 基于模型检测的需求一致性检测

为了实现需求一致性自动检测，本文采用模型验证技术，其基本思想是：将待验证的系统表示为一个状态迁移模型M，需验证的性质用时序逻辑公式φ表示，进而就可以将“系统是否满足所期望的性质”转化为“M是否满足公式，即M|=φ”。目前，较为著名的模型验证工具有NuSMV、SPIN和FDR等。考虑到NuSMV开源、具有开放式架构和以SMV语言描述模型的行为可解释为Kripke结构(KS)等特点。故本文选用NuSMV作为需求一致性自动验证工具。

图2所示为基于NuSMV的参与组织需求一致性自动检测框架，具体检测步骤如下：

步骤1将协同业务过程转换为SM，之后将SM转换为SMV规约。

步骤2采用DRDL描述参与组织需求，并将其转换为LTL公式。

步骤3将SMV规约和LTL公式分别作为NuSMV的模型和性质输入，验证结果将表明协同业务过程是否满足给定的参与组织需求。

如果验证结果得到了验证需求的反例，则说明协同业务过程与期望需求不一致，根据反例信息可以找到协同业务过程中存在的问题并进行调整；如果验证结果没有反例出现，则说明协同业务过程满足期望性质。特别地，由于使用模型检测工具NuSMV，使得需求一致性验证过程可自动完成，不需要人工干预。

分析图2所示的一致性验证框架可知，生成协同业务过程执行语义和采用RDG描述参与组织需求在前文进行详细阐述。因此，为实现需求一致性自动检测，需要重点解决将执行语义模型转换为NuSMV输入语言和将RDG描述参与组织需求转换为LTL公式这两个问题。下面对这两个问题进行详细讨论。

3.1 执行语义到Kripke结构转换

由于NuSMV的输入语言是基于有限状态自动机的形式语言，其行为解释为Kripke结构。将执行语义模型转换为NuSMV输入语言的关键在于实现执行语义模型到Kripke结构的转换。下面先给出Kripke结构的定义。

定义11Kripke结构[27]。设AP为非空原子命题集合，Kripke结构形式化定义为4元组KS=(S,S0,R,L)，其中：

(1)S为有限状态集合。

(2)S0⊆S为初始状态集合。

(3)R⊆S×S为状态迁移关系集合。

(4)L:S→2AP为标记函数，用于实现状态到AP幂集映射，表示返回在该状态成立的原子命题集合。

(2)Sk0={s0}。

(4)对于∀r，s∈S，L(r)={⊥}，L(s)={⊥}且L((r,a,s))={a}。

通过对LTS到KS转换过程进行分析，可得到转换唯一性定理。

证毕。

定理1的结论确保了SM与KS间存在一对一映射关系。以此为基础，并通过对转换过程进行归纳，得出定理2。

证明采用数学归纳法证明。

(2)当n=k-1时，对SM第k-1次(记为SMk-1)转换生成的Kripke结构为KSk-1，满足trace(SMk-1)≈trace(KSk-1)，其中函数trace(S)用来标识S的迹。

证毕。

根据定理2，对于任意以RDG描述需求R具有如下重要结论。

定理3设SM为协同业务过程执行语义模型，由其生成Kripke结构为KS。需求R在SM和KS上具有相同满足结果。

证明由定理2结论可知：SM和KS具有相同迹语义，则由文献[28]结论可知，SM和KS满足相同的时序逻辑规范，即对于任意LTL公式φ，公式φ在SM和KS具有相同验证结果。又因为需求R在本文中采用线性时序逻辑公式LTL描述(参见3.2节),可推导出，需求R在SM和KS上具有相同满足结果。

证毕。

基于定理3结论，对于任意以RDG描述参与组织需求R，有如下推论。

推论1设SM为协同业务过程生成语义模型，SL是根据定义9生成Kripke结构对应的SMV语言，需求R在SM满足结果和SL上检测结果一致。

证明基于KS，NuSMV输入语言，即SMV语言中，状态变量初始值用init()语句定义；对于∀r∈R(R为KS中状态迁移关系集合)，r在SMV语言中可由next-case语句进行精确地刻画。因此，由KS生成的SMV语言与KS间具有相同反应式，即具有相同迹。而定理2结论又表明SM与KS之间是迹等价，从而可知：由KS生成的SMV语言与SM是迹等价的。结合定理3结论可推出：在R由LTL公式描述情况下，需求R在SM满足结果和SL上检测结果一致。

证毕。

在确保转换正确前提下，根据定义10得到执行语义模型到SMV语言转换规则如表2所示。

表2 执行语义模型SM到SMV语言转换规则

续表2

3.2 需求到LTL公式转换

将参与组织需求转换成LTL公式分两步进行：①提出将参与组织需求中的需求依赖关系转换为LTL公式规则集；②在上一步的基础上，提出将参与组织需求转换成LTL公式算法。

通过分析DRG中4种需求间的依赖关系，给出4条转换规则用于将需求依赖关系统一转换为LTL公式。◇为LTL中存在算子，有关LTL的详细内容参见文献[24]。

规则1若R=R1&…&Rn，则用LTL公式表示为◇R1∧…∧◇Rn。

规则2若R=R1‖…‖Rn，则用LTL公式表示为◇R1∨…∨◇Rn。

规则3若R=Ri⊗Rj，则用LTL公式表示为◇Ri→◇Rj。

规则4若Ri→Rj，则用LTL公式表示为◇(Ri∪Rj)。

设R为采用RDG描述参与组织需求，且具有良构性。下面给出算法1来自动生成需求R对应的LTL公式集合。算法1首先调用算法2生成相关节点对应的LTL公式，然后按照规则3和规则4生成互斥关系和前驱关系对应的LTL公式。

算法1 Generate LTL formula for R

Input:Requirement R=(V,E,φ);

Output:LTL formula set LS for R;

1. generate LTL formula rootLtl for root requirement root by algorithm 2 and add it to LS;

2. for each XOR R=Ri⊗Rjin R do

3. generate LTL formula liand ljfor Ri, Rj, respectively;

4. and add ◇li→◇ljto LS;

5. end for

6. for each precursor R=Ri→Rjin R do

7. generate LTL formula liand ljfor Ri, Rj, respectively;

9. end for

10. return LS;

算法2根据规则1和规则2生成需求R中任意节点v对应的LTL公式，其时间复杂度为O(V)，其中V为需求R中节点数。

算法2 Generate LTL formula for given vertex v

Input:Requirement R=(V,E,φ);

Output:LTL formula for vertex v;

1. generate decomposition relation DR={v} and add DR to list list;

2. put v into queue Q;

3. while Q.size > 0 then

4. elem=Q.poll;

5. obtain decomposition type type by elem;

6. if type=AND then

7. get children children={c1,…,cn} of elem;

8. replace elem by children in DR where DR contains elem;

9. for each c in children do

10. if c is not leaf then

11. add c to Q;

12. end if

13. end for

14. else

15. obtain DR where DR contains elem;

16. construct set {c1}∪(DR-elem),…,{cn}∪(DR-elem);

17. delete DR in list;

18. and add each element in set to list;

19. end if

20. end while

21. ltl=null;

22. for each elem={e1,…,en} in list do

23. tempLtl=e1∧…∧en;

24. ltl=ltl∨tempLtl;

25. end for

26. return ltl;

根据3.1节和3.2节讨论方法，可将协同业务过程和参与组织需求分别转换为表达能力等价的SMV规约和以LTL公式表示的性质。将转换生成SMV规约和LTL公式分别作为NuSMV的模型和性质输入，NuSMV(其集成了基于LTL公式的模型检测引擎)将自动完成需求一致性检测。根据NuSMV检测结果，可以判断协同业务过程是否与需求一致。若存在不一致，则根据反例信息可以找到协同业务过程中存在的问题并予以修正。

4 实例分析

4.1 实例说明

为说明本文所提方法在建模和分析时的有效性，本节以协同制造中一个简化的采购订单(记为PO)为例对其进行建模，并与属于该方法内的典型文献[11]进行对比分析。该采购订单中包含1个零售商、1个制造商和1个产品送货商，其交互过程如图3所示。首先，零售商与制造商就订购产品价格进行反复协商(步骤1)，在价格达成一致后零售商向制造商提交订单(步骤2)；其次，制造商在收到该订购请求后向送货商发送运输请求(步骤3)，送货商在收到运输请求后确定运输费用并通知制造商(步骤4)。在收到运费请求后制造商先向零售商请求支付订购产品(步骤5)，接着在零售商支付完成后(步骤6)向送货商付费(步骤7)；最后，送货商在收到制造商付费消息后将订购产品送至零售商(步骤8)。

4.2 采购订单建模

采购订单PO建模可按如下两步进行：

(1)建模采购订单PO对应协同业务过程

通过分析图3中PO的交互过程，采用Petri网建模零售商、制造商和送货商各自的业务过程控制流分别如图4a～图4c所示，其中每个变迁标识(如r1等)为其对应任务标识。

进一步分析，可得到PO中每个参与组织控制流中涉及任务信息如表3所示。

表3 采购订单中任务信息

续表3

将零售商、制造商和送货商对应的业务过程根据定义6并发组合得到采购订单的协同业务过程。根据定义10生成PO执行语义如图5a所示，继而根据定义12将其转换为KS如图5b所示。

图5中，每个任务完成后所达到的需求如表4所示。

表4 任务需求关联表

(2)建模参与组织需求

参与组织需求可由参与组织间协商得到，其隐含意图是能够实现参与组织间的价值交换[26]，例如零售商支付，而制造商提供产品就是一类典型价值交换过程。基于该原则，PO中参与组织需求R采用RDG描述如图6a所示，其中需求Order表示若制造商提供订购产品(rr7)，则零售商支付(rr6)，且零售商在制造商提供订购产品之前完成支付(rr6→rr7)；需求ShipGoods表示若送货商运送订购产品至零售商(rr7)，则制造商支付运费(rm9)，且制造商在送货商运送订购产品之前完成支付(rm9→rr7)。需要说明是，图6a仅仅描述参与组织间存在一类共性需求，需求R可根据实际情况做进一步细化。

根据算法1将图6a所示需求R转换为LTL公式，如性质1～性质3所示。

性质1(◇payOrder=delivered∧◇orderGoods=received∧◇payshipGoodes=delivered)。

性质2(◇(payOrder=delivered∪orderGoods=received))。

性质3(◇(payshipGoodes=delivered∪orderGoods=received))。

4.3 方法评价

为评价本文方法的有效性，选择此类方法中具有代表性的工作[10]。文献[10]提出的需求一致性验证方法针对单个业务过程，不能直接应用于跨组织环境下需求一致性验证。但在求得协同业务过程执行语义和明确参与组织需求前提下，文献[10]方法也可用于协同业务过程需求一致性验证。因此，以PO为对象，对本文方法和文献[10]方法的有效性进行定性评价。

有效性是指针对任意结构的协同业务过程，本文方法和文献[10]方法能否识别出PO满足既定需求。由于协同业务过程的执行语义以LTS刻画，本质上，LTS是一个有向图，故对于任意LTS而言，迁移集间只存在顺序和循环两种关系。因此，针对PO首先构建有环结构协同业务过程，记为LCBP，即PO中存在零售商和制造商间就订购产品价格进行反复协商交互；然后构建无环结构协同业务过程，记为NLCBP，即将PO中零售商和制造商间就订购产品价格进行反复协商交互移除。同时，为了评价能否识别既定需求，先以图6a所示需求R作为目标需求进行评价。由于PO满足需求R，故记此时需求为CR；然后同时将图6a中需求shipGoods注入一个外部需求re=(r,delivered)，得到需求记为ER，如图6b所示，和如图5b KS中节点P1617关联外部需求re=(r,delivered)，表示PO在执行至P1617时，同时满足需求(payshipGoodes,delivered)和re=(r,delivered)，即rm9={(payshipGoodes,delivered),(r,delivered)}，记此时采购订单对应协同业务过程为ELCBP，且无环情形下采购订单对应协同业务过程记为ENLCBP。

使用本文方法和文献[10]方法在LCBP、NLCBP检测需求CR和在ELCBP、ENLCBP上检测需求ER，检测结果分别如表5和表6所示。表5和表6中，√表示检测结果为True，×表示检测结果为False，∅表示不支持检测。

表5 两种方法CR检测结果

由表5可以看出：针对LCBP，文献[10]方法检测结果为∅。其原因在于：文献[10]方法采用任务系列匹配方式，即在检测之前需要求取所有的任务执行系列，由于LCBP中存在环结构，这将导致需求一致性无法判定。而本文方法检测结果为√，表示能够成功检测出LCBP满足需求CR。其原因在于：本文方法采用模型检测技术，该技术可有效处理过程模型中含有环结构情形。其思想是将以LTL公式描述的需求转换为Büchi自动机，过程模型以有限状态机刻画，通过判定Büchi自动机与有限状态机的积(也为自动机)中是否存在强连通组件来判断需求是否满足[28]。针对NLCBP，本文方法和文献[10]方法均能够成功检测出NLCBP满足需求CR。

表6 两种方法ECR检测结果

由表6可以看出：针对ELCBP，文献[10]方法检测结果为∅，其原因在表5分析中进行阐述。而本文方法检测结果为√，表示能够成功检测出LCBP满足需求CR。针对NLCBP，文献[10]方法检测结果为×，而本文方法检测结果为√。其原因在于：文献[10]方法采用任务系列匹配方式实现需求一致性检测，需求以任务计划[29]形式描述，故仅能检测出需求(payshipGoodes,delivered)，(r,delivered)存在次序关系情形，无法检测出上述需求同时发生情形。而本文方法采用LTL公式(◇payOrder=delivered∧◇orderGoods=received∧◇payshipGoodes=delivered∧◇r=delivered)描述需求ER，可方便地表述出需求(payshipGoodes,delivered)和(r,delivered)间次序满足和同时满足情形，因此检测结果为√。

综上所述，在需求描述方面，由于本文方法采用LTL公式表示需求，较文献[10]方法中任务计划描述能力更强，即所有用任务计划描述需求均转换成LTL公式[29]。此外，跨组织环境下需求间通常存在次序满足和同时满足情形，采用LTL公式均可直观描述。在需求一致性检测方面，文献[10]方法无法处理过程模型中存在环结构情形，而本文方法能够有效应对此类情况，适用性更强。因此可得出如下结论：相较文献[10]方法，本文方法一方面可直接应用于建模跨组织需求和支持需求分析过程模型；另一方面可更加有效地刻画参与组织需求和进行需求一致性验证。

5 结束语

参与组织需求是协同业务过程形式验证中需要考虑的一个重要方面。本文基于模型检测技术提出一种验证参与组织共性及个性需求方法。该方法一方面将协同业务过程转换成语义等价SMV语言，从理论上确保验证结果一致性；另一方面，提出将由RDG描述的参与组织需求转换成LTL公式算法。进而借助符号模型检测工具NuSMV实现在协同业务过程上自动检测参与组织需求满足问题。由于协同业务过程规模通常较为复杂，使用模型检测技术验证参与组织需求一致性可能面临的状态空间爆炸问题。为此，未来将从以下3个方面开展研究：①在考虑确保检测结果一致前提下，如何采用抽象、分解等方法来提高需求一致性形式验证效率；②本文将RDG中约束关系(即Pre关系和XOR关系)限定在同一分解层次，在实际应用中，约束关系也可能分布在不同层次，未来工作将放松这一限制，使得本文提出的方法更具普适性；③在跨组织环境下，不同参与组织的需求可能有天然的不一致性，如何消除这种不一致将在未来工作中进行详细讨论。