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

3162 Journal of Software 软件学报 Vol.31, No.10, October 2020

则其时间将进一步增加.而本文方法只需获取所有的完整简单路径(如 Travel Book System 中只含有 384 条),并
对核协调映射即可生成修正协同业务过程,避免文献[13−15]中方法使用过程模型挖掘算法(如α算法等)、案例
差异检测等步骤,从而缩短了修正时间;
(2) 由于本文方法能够事先保证修正协同业务过程中含有修正前协同业务过程中所有的完整轨迹,且未引
入隐藏轨迹,这使得本文方法无须进行有效性确认,即有效性确认耗费时间为 0ms.而文献[13−15]中方法的有效
性确认所耗费的时间均较高.例如,针对 Travel Book System,文献[13]和文献[14,15]中方法进行有效性确认耗费
的时间分别为 20 900ms 和 59 696ms.分析发现,这是由于选取的协同业务过程和对应修正协同业务过程中均含
有较多的简单轨迹和完整轨迹所致.可以预见,若对更加复杂的协同业务过程进行有效性确认,则其所耗费的时
间将进一步增加;
(3) 从修正耗费总时间来看,相较文献[13]和文献[14,15]中的方法,本文方法的修正效率有极大的提高,分
别提高 14 倍和 42 倍.
综上分析,可以得出如下结论:相比文献[13−15]中所提出的正确性修正方法,在考虑协同业务过程实际特
征的情况下,由于本文方法能够事先确保修正协同业务过程中含有修正前协同业务过程中所有完整的轨迹,且
未引入隐藏轨迹,从而使得本文方法可以对协同业务过程进行更加有效的修正,并且能够极大地缩短修正所耗
费的时间.
6 相关工作

目前,针对协同业务过程的正确性分析方法可分为两类:正确性检测方法和正确性修正方法.下面对这两类
方法中的一些典型文献进行介绍和分析.
6.1 正确性检测方法

国内外研究者针对协同业务过程的正确性检测方法开展了大量的研究.归纳起来,这些方法可分为 3 类:基
于 Petri 网的检测方法、基于进程代数的检测方法及基于自动机的检测方法.
以传统的组织内业务过程建模方法为基础,文献[9]较早地在国际上提出了 IOWF(inter-organizational
workflow)用于建模跨组织业务过程.针对构建跨组织业务过程提出合理性概念用来定义其正确性,并基于 Petri
网的可达图提出跨组织业务过程正确性检测方法.之后,国内外研究者以此为基础开展了大量的研究.如文献
[10]针对跨部门业务过程协同呈现出越来越复杂的特点,对 WF-net 扩展资源和消息等要素以建模参与部门的
业务过程,继而使用库所熔合技术将资源库所和消息库所加以熔合从而得到跨部门协调业务过程模型.针对构
建跨部门业务过程,基于合理性定义其正确性并提出验证方法.跨组织工作流网 IWF-nets(inter-organizational
workflow nets)可以有效地建模协同业务过程间基于消息的协作.为了确保协同业务实施的正确性,文献[26]引
入了兼容性和弱兼容性的概念,并针对 IWF-nets 的网结构提出了用于判定兼容性或弱兼容性的充要条件.针对
公共管理呈现出交互的特征,为确保其正确实施,文献[27]首先使用 BPMN(business process modeling notation)
对其进行描述,之后将其 BPMN 模型转换成基于 Petri 网的模型,并采用 Petri 网的展开技术(unfolding-based
technique)对相关性质(如死锁等)进行验证.为了有效地验证协同业务过程的行为正确性,文献[28]首先利用
BPMN 建模协同业务过程,然后将每个参与组织的流程转换为一类高级 Petri网 ECATNets(recursive ECATNets),
最后基于库所熔合技术将其组合得到以 ECATNets 来描述的模型.由于该模型的语义被解释为条件重写逻辑,
进而可以利用 Maude LTL 模型检测器对协同业务过程的行为正确性性质进行验证.
基于 Pi 演算,文献[16]较早地提出一种利用进程代数建模跨组织业务过程方法.即利用 Pi 演算的并发算子,
将跨组织业务过程建模为一组自治且并发执行的组织内子流程的组合,子流程建模为组织内本地流程定义和
组织间控制约束的组合,并利用工具 MWB(mobile workbench)验证抽象正确性.为了检测协同业务过程能否正
确地协调,文献[29]提出了一种针对多个业务过程组合验证的概念框架.它将 BPMN 建模的协同业务过程转换
以时间通信顺序进程 CSP+T(communicating sequential processes+time)表示进程,之后采用时序逻辑公式定义
期望正确性性质,并利用模型检测方法在工具 FDR2(failures-divergences refinement)上自动验证正确性性质是