Page 187 - 《软件学报》2020年第10期

莫启 等:协同业务过程的建模及正确性修正 3163

否满足.为实现面向 Web 服务的流程无缝集成,文献[30]提出了一种基于递归组合代数的 Web 服务交互流程建
模和验证方法.首先利用递归组合代数建模 Web 服务流程交互,并将其转换为递归组合交互图,之后利用递归组
合规约语言来描述需求,并通过递归组合交互图自动地验证需求是否满足与否.
为了使得多个基于 Web 服务的业务过程的组合符合用户定义适配需求,文献[31]提出一种描述及验证多业
务过程间行为适配的方法.它采用 LTS 描述业务过程及适配器,进而将业务过程与适配器组合来检测其是否相
容以判断多业务过程的组合是否符合用户定义适配的需求.互操作是业务协同正确实施须具备的先决条件,为
确保每个参与组织的互操作是否符合规定的需求,文献[32]首先使用 BPMN 来描述协同业务过程,之后将其
BPMN 模型转换成模型检测工具 UPPAAL 中的时间自动机网络(timed automata network,简称 TAN),并采用时序
逻辑 TCTL(time computation tree logic)描述互操作需求,从而实现互操作自动检测.特别地,BPMN 模型中每个
参与组织业务过程在 TAN 中对应一个时间自动机(timed automata,简称 TA),这些 TA 并发组合构成了 TAN,即
协同业务过程.在后续工作中,为了更加有效地存储和描述互操作需求,文献[33]首先提出了一种领域描述语言
用来描述互操作需求,继而将描述需求自动转换为时序逻辑 TCTL,并采用 TAN 建模协同业务过程.通过
UPPAAL 实现互操作需求的自动验证.
上面提出的正确性检测方法通常具有检测过程自动化,不需要人工干预,且在检测失败时能够给出诊断信
息,便于业务设计人员发现并修正错误.但其不足是,若协同业务过程中存在多处不正确,则需要经过多次检测,
且在每次检测后都需要对协同业务过程重新调整.这种设计、验证、分析及纠错的过程使得协同业务过程的正
确性分析变得复杂且耗时.

6.2 正确性修正方法
相比正确性检测方法,针对业务过程正确性修正方法是较新的课题,相关研究工作较少.文献[11,12]针对以
Artifact 为中心的业务过程提出一种正确性保持的设计方法.它首先采用 Petri 网建模以 Artifact 为中心的业务
过程,之后以合规性和弱合理定义其正确性,最后将业务过程与正确性合成以自动构建具有正确性的业务过程.
文献[34]采用开放工作流网 oWFN(open workflow nets)建模跨组织环境下的业务过程,利用 CTL 公式定义期望
正确性性质,根据以 CTL 公式定义性质对业务过程内部结构进行修改来构建跨组织环境下具有正确性的业务
过程.然而,上面提出的正确性修正方法均面向组织内的单个业务过程.由于协同业务过程具有自治性、分布性
及涉及多个业务过程间的同步或异步交互,因此上面提出的方法不适用于跨组织环境下的协同业务过程.
近年来,面向轨迹的业务过程修正方法引起一些学者的关注.文献[14]首次在国际上提出此类方法.首先利
用已有的一致性检测来发现过程模型与轨迹间差异,并将体现这些差异的轨迹从原轨迹中分离出来,以子轨迹
来加以表示.针对这些子轨迹,构建其对应子结构并将其添加至原业务过程中,从而完成业务过程的修正.随后,
文献[15]对文献[14]的工作进行了一些改进,即针对一致性检测中发现的循环结构,构建其对应的子过程并将其
添加至修正模型中.文献[35]提出的修正方法沿用了文献[14,15]的思路.针对工作流模型,首先利用监控矩阵刻
画实际工作流模型足迹,通过比较工作流模型的轨迹与足迹间的差异,提出 4 种用于修正的工作流模型算法.我
们课题组最近的工作 [13] 是结合 Petri 网和过程挖掘的相关理论,提出一种针对协同业务过程的修正方法.该方法
首先获取部分正确协同业务过程中所有完整的轨迹,之后利用α算法从这些完整的轨迹构建相容协同业务过
程,最后通过设置协同业务过程与业务过程间的任务执行同步关系以协调业务过程的正确运行.然而,利用上述
方法建立的修正业务过程仍是集中式的,也存在修正前协同业务过程中完整轨迹可能会丢失和修正协同业务
过程中可能会引入隐藏轨迹等问题.相较而言,本文方法构建的协同业务过程是完全分布式的(即不存在中心流
程),它的执行能够正确终止且与修正前协同业务过程中含有的所有完整轨迹相一致.
面向 Web 服务流程的自动组合方法也是与协同业务过程正确性修正比较相关的工作.文献[36]首先裁剪合
理性定义正确性(即相容性),针对部分相容 Web 服务流程采用 Petri 网建模每个服务的流程,然后将其进行组合
并分析其相容性.若分析结果部分相容,则产生适配器将来协调服务流程,使之前部分相容的服务流程转换为完
整相容,且未改变原有服务流程的内部结构.为了应对服务流程间存在时序约束及消息匹配问题,文献[37]首先
采用 Petri 网建模每个服务的流程,然后根据消息匹配情况及时序约束构建适配器,从而使得所有服务的流程与