基于流程抽象的协同业务过程符合性验证

莫 启，向吉祥，汪煜祺，代 飞，许小龙，齐连永

(1.云南大学 软件学院，云南 昆明 650091；2.云南大学 云南省软件工程重点实验室, 云南 昆明 650091；3.西南林业大学 大数据与智能工程学院，云南 昆明 650091；4.南京信息工程大学 计算机与软件学院，江苏 南京 210044；5.曲阜师范大学 信息科学与工程学院，山东 曲阜 273165)

0 引言

随着企业信息化程度不断提高，企业经营模式发生了重大转变，从独立经营模式发展成为跨企业合作模式[1]。作为一类跨组织的业务过程，协同业务过程[2]在企业协作中扮演着重要角色。当前协同业务过程被广泛应用于各种行业中，如医疗[3]，电子商务[4]和物联网[5]。为确保这些行业应用在实际中良好地实施，协同业务过程在设计阶段通常需要满足如下3类重要性质：

(1)正确性[6]为完成既定业务目标，协同业务过程应能够正确地执行完成，且在执行过程中未出现死锁、活锁和未指定消息接收等。

(2)一致性[7]协同业务过程的执行应与事先确定的规约一致。规约通常指编排，即从全局视角定义业务过程间交互，由参与组织协商确定[7]。

(3)符合性[8-9]协同业务过程面向特定行业，其执行需与应用领域的特性相符。应用领域特性是指领域约束，通常来自管理、风险及审计符合性等相关方面[8-9]。例如，在信贷业务过程中，每次贷款完成前需经过相关职能部门的贷款审查，从而保证贷款操作透明合理。

事实上，上述3类性质均可在设计阶段通过运用形式验证技术予以确保。例如，若需要判断协同业务过程与规约间的一致性，则可利用行为等价理论(如迹等价等)进行判定[7]。由于当前验证协同业务过程正确性及一致性的相关研究较为成熟，本文关注如何验证协同业务过程与领域约束的符合性。

目前，国内外研究者围绕如何验证协同业务过程符合性做了大量工作，但是这些研究工作的关注重点仍是符合性验证中符合性管理框架设计、符合性语言设计及协同业务过程可视化建模等方面[9-10]，并未涉及业务过程中内部流程细节(包括本地活动及由这些活动形成控制流)处理，这将导致如下3个方面问题：①建立的协同业务过程是具有协同功效的全局模型(即由业务过程直接组合形成)，因此将参与组织的内部流程信息完全暴露给其他组织，与隐私保护原则相违背[2]；②从外部环境观察，协同业务过程行为表现为业务过程间活动交互，全局模型中内部流程细节可能会导致符合性误判；③由于是在全局模型上验证领域约束是否相符，导致其验证效率低下。

为此，基于流程抽象(即将业务过程中内部流程细节抽象掉，只保留外部可见部分)，本文提出一种协同业务过程行为符合性验证方法。该方法隐藏所有参与组织的业务过程中内部流程细节，能够有效地避免暴露组织内部流程信息、确保符合性验证结果的正确性及提高形式验证效率。本文的主要贡献如下：

(1)基于流程抽象提出一种协同业务过程行为符合性验证方法。即先基于弱轨迹等价[11]将业务过程中含有的内部流程细节全部移除，得到抽象业务过程，并将其并发组合得到抽象协同业务过程；之后采用线性时序逻辑(Linear time Temporal Logic，LTL)描述领域约束；最后借助模型检测技术自动地验证抽象协同业务过程与领域约束是否相符。

(2)理论上证明了给定领域约束在协同业务过程和抽象协同业务过程上的验证结果一致。这可避免暴露组织内部流程信息、确保符合性验证结果的正确性及提高形式验证效率。

(3)采用实际协同业务过程集阐述本文提出方法的有效性，并对所提方法的分析效率进行定量评价。

1 方法概览

本文关注验证协同业务过程与领域约束间的符合性，提出的方法框架如图1所示，具体包含如下两个阶段：

(1)建模阶段 首先利用标号迁移系统[8]，参与组织建模各自的业务过程，然后并发组合形成协同业务过程；之后为了确定期望的领域约束，参与组织间进行协商并利用符合性语言(Compliance Request Language, CRL)[19]描述。特别地，直接采用命题逻辑或时序逻辑定义领域约束易于出错且复杂，而符合性语言能够以模式方式描述领域约束，对于参与组织易于使用。

(2)分析阶段 首先抽象业务过程中内部流程细节，得到抽象业务过程；然后并发组合这些抽象业务过程以建立抽象协同业务过程。上述操作为本文所提方法的核心。之后将符合性语言描述的领域约束映射为以LTL公式表示的性质，其中具体映射规则由符合性语言CRL规定。最后将抽象协同业务过程转换为PAT(process analysis toolkit)[注]http://pat.comp.nus.edu.sg/。中以CSP#(communicating sequential programs)[12]描述进程，并将产生的CSP#进程规约和以LTL公式表示的领域约束作为模型检测器PAT的输入，根据检测结果能够有效地判断协同业务过程是否满足期望的领域约束。

具体符合性检测由PAT自动完成，不需要人工干预。更重要的是，对协同业务过程进行符合性验证可转换为对抽象协同业务过程验证(它们的验证结果一致)，从而可避免暴露内部流程信息且提高符合性验证效率(抽象协同业务过程状态空间极大地压缩)。同时，由于屏蔽了内部流程细节对符合性验证的影响，可避免误判。

2 协同业务过程及领域约束建模

根据图1所示框架，参与组织首先需对协同业务过程及领域约束进行建模，下面进行详细阐述。

2.1 协同业务过程建模

沿用项目组前期工作[13]，在对业务过程建模时，本文也采用标号迁移系统对其进行描述，然后将业务过程并发组合，以构建协同业务过程。

本质上，一个参与组织的内部业务逻辑(即外部环境不可见部分)与其外部环境(即其他参与组织的业务过程)的交互[2,14]可以利用一个业务过程进行描述，其形式定义如下。

定义1业务过程[13]。 业务过程是一个迁移系统N=(S,s0,ψ,γ,Δ)，其中：

(1)S为有穷状态集合；

(2)s0∈S是初始状态；

(3)ψ⊆S是终止状态集；

(4)γ=γl∪γi是活动集，γl和γi分别为本地活动和交互活动集。特别地，γi=γs∪γr，其中：γs和γr分别为异步发送和接收活动集合；

(5)Δ⊆S×γ×S是刻画活动间控制流的迁移关系。

为了方便，将一条迁移(p,a,q)∈Δ记为p[a>q。另外，∀a∈γs，其形如!m，m是其关联发送消息。类似地，∀a∈γr，其形如?m，m是其关联接收消息。

利用文献[13]中提出的并发算子，多个业务过程可组合构建为一个协同业务过程。

协同业务过程的状态表示为格局，其形式定义如下。

特别地，将N的初始格局表示为c0=，其中：∀i∈[1，…，n]；s0i为Ni的初始状态；M=NIL表示N在执行前不存在消息；N的终止格局表示为ce=，其中：∀i∈[1，…，n]，sei为Ni的一个终止状态；M=NIL表示N在执行后产生的消息均被接收。

为了对格局中的状态和消息进行重置，定义函数如下：

协同业务过程的执行由其点火规则确定，形式定义如下。

(1)若a∈γl，则c[a>c′，当且仅当si[a>sj∧c′=c[si←sj]；

(2)若a=!m，则c[a>c′，当且仅当si[a>si′∧M′=M+ {m}∧c′=c[M←M′]∧c′=c[si←sj]；

(3)若a=?m，则c[a>c′，当且仅当si[a>sj∧M(m)≠0∧M′(m)=M(m) - {m}∧c′=c[si←sj]。

基于点火规则，协同业务过程行为可形式化为路径。

定义7轨迹[13]。 给定路径r=c0[a1>c1…cn-1[an>cn…，则其迹可定义为a0∧a1…an-1∧an∧…。

特别地，若将a0∧a1…an-1∧an∧…中本地活动全部移除，则得到r交互迹，记为χ(a0∧a1…an-1∧an∧…)。本文交互迹主要用于避免本地活动对符合性验证造成影响。另外，若格局c1能够通过执行迹σ迁移至格局c2，则记为c1[σ>c2。

定义8路径一致。给定两条有穷路径ru=cu0[a1>cu1…cu(n-1)[an>cun和rv=cv0[b1>cv1…cv(n-1)[bn>cvn，ru和rv一致，记为ru=rv，当且仅当ru和rv的交互轨迹相同。

在实际应用中，协同业务过程进行符合性验证前需满足正确性[8]。故本文后续讨论中均默认协同业务过程是正确的。目前，为了验证协同业务过程的正确性，研究者提出多种标准，其中应用最为广泛的是合理性[6]及其变体(如弱合理[15]等)。由于合理性主要用于定义组织内业务过程正确性且较为严格[15]，本文利用弱合理性定义协同业务过程正确性。

定义9弱合理。给定协同业务过程N=(S,s0,ψ,γ, Δ)，则N是弱合理的，当且仅当对于从s0可达的任意格局c，存在轨迹σ和一个终止格局ce∈ψ，使得c[σ]>ce。

定义9本质上要求从初始格局可达的任意格局都能够到达终止格局，一方面，它可以确保每个业务流程都能达到终止状态，并避免协同业务过程中可能存在的死锁和活锁等情形；另一方面，终止格局要求每个业务流程的消息队列为空，从而确保可以合理地接收协同中生成的所有消息。

2.2 领域约束建模

协同业务过程通常面向特定行业，其执行受到应用领域内的相关特征(如行业规范、制度规范及法律法规等)约束[8-9]。归纳起来，领域约束大致可分为必选领域约束和可选领域约束两类[16]。前者指协同业务过程在执行时必须满足的领域约束；而后者则是指协同业务过程在执行时可选的领域约束，不要求必须满足。例如，在投稿业务过程中，若作者投稿被拒，则编辑部(或会务组)应向作者返回退稿理由，这可视为一个必选领域约束；而在在线购买中，客户在购买商品之后，可以自愿地添加该商品评论，这就可视为一个可选领域约束。

按形式基础，现有的研究中通常采用命题逻辑或时序逻辑描述领域约束[8-9]。相比命题逻辑，时序逻辑中添加一些额外时序操作符(如终将时态算子◇等)，表达能力更加强大。因此，本文采用LTL来描述领域约束。

用来描述领域约束的LTL公式是定义在交互迹上的一个表达式。

定义10领域约束。 领域约束是一个LTL公式，采用BNF定义如下：

∅::=1 |a(a∈AP) | ∅1∧∅2| ┑∅ | ○∅ | ∅1∪∅2。

其中：AP为原子领域约束(即表示为交互活动)集合；以LTL公式表示领域约束用来断言协同业务过程中的交互迹所满足的性质。对于任意交互迹σ，σ满足LTL公式∅解释如下：

σ|=1；

σ|=a⟺a0=a(a0为σ中第一个活动)；

σ|=∅1∧∅2⟺σ|=∅1∧σ|=∅2；

σ|=┐∅⟺┐(σ|=∅)；

σ|=○∅⟺σ1|=∅;

σ|=∅1∪∅2⟺∃i≥0:σi|=∅2∧∀j∈[0,i-1]:σj|=∅1。

其中：终将时态算子◇和总是时态算子□可由上述时态算子推出，即◇∅≜1∪∅；□φ≜┐◇┐∅。

特别地，本文中仅考虑涉及协同业务过程行为的领域约束，而包含其他要素(如资源、数据等)的领域约束将在下一步工作中讨论。从外部视角观察，协同业务过程的行为表现为活动间交互。因此，本文将原子领域约束定义为一个交互活动。更重要的是，基于交互迹定义领域约束可以避免符合性验证中的误判。例如，若存在某条轨迹σ=a0∧a1∧a2，其中：a0是本地活动，而a1和a2是交互活动。从外部视角观察，由于a0不可见，故领域约束∅1=a1及∅2=a1∪a2满足，即验证结果均为true。但是，若直接利用σ进行验证，则∅1及∅2的验证结果均为false。由于消息迹将σ中的本地活动a0移除，验证结果与观察到的验证结果一致。

实际中的领域约束通常采用符合性语言[8-9]描述。本质上，符合性语言是由一些常见模式(如存在模式、次序模式等，用自然语言描述)转换成时序逻辑公式的映射组成。目前，这方面研究工作较为成熟。为了避免重复工作，本文利用文献[9]中的符合性语言CRL来描述领域约束。例如，对于网店店主不允许客户添加商品评论这类存在性领域需求，则可用CRL中isAbsent模式描述，映射LTL公式为□┐(comment)。有关CRL的详细内容可以参考文献[9]。

基于领域约束定义，下面定义领域约束在协同业务过程上的满足性。

定义11领域约束满足。 给定协同业务过程N，称N满足以LTL公式∅表示领域约束，记为N|=∅，当且仅当对于N中任意路径对应的交互迹σ，N|=∅成立。

需说明的是：在跨组织环境下，领域约束通常通过参与组织之间的协商得到，并且它们的获取是一个循环迭代的过程。在文献[9]中描述了如何迭代改进获得领域约束。另一方面，参与组织通过协商建立的领域约束之间可能存在自然的不一致性，归纳起来可以分为领域约束冗余和领域约束冲突两类[17]。前者是指一个领域约束的存在，可以从其他领域约束中推导得出，因此不必分析该领域约束；后者是指存在两个领域约束，而协同业务过程不能同时满足这两个领域约束，因此对其进行分析是徒劳的。文献[17]在相关的LTL理论的基础上详细研究了如何消除这两种类型的不一致。限于篇幅，本文后续讨论中的领域约束均指无冗余和无冲突领域约束。

3 符合性验证

在参与组织定义业务过程及利用CRL描述领域约束之后，下面讨论符合性验证。如图1所示框架，符合性验证的核心是将业务过程抽象为抽象业务过程及构建抽象协同业务过程。

本质上，抽象业务过程对应组织的公共过程，它从单个组织视角描述其与外部环境的交互及交互次序[2,14]。相比抽象业务过程，符合定义1的业务过程中还含有外部环境不可见的业务逻辑，即本地任务及由这些任务形成的控制流。因此，可以通过将业务过程中本地活动及相关控制流移除后形成抽象业务过程。下面先定义隐藏操作，用于将业务过程中本地活动置为外部不可见活动。

定义12隐藏[13]。 给定业务过程N=(S,s0,ψ,γ,Δ)，则对N进行隐藏后得到的隐藏业务过程为Nh=(Sh,sh0,ψh,γh,Δh)，其中：

(1)Sh=S；

(2)sh0=s0；

(3)ψh=ψ；

(4)γh⊆{τ}∪γ；

(5)∀(p,a,q)∈Δ，若a∈γi，则(p,a,q)∈Δh，否则τ-迁移关系(p,τ,q)∈Δh。

由定义12可以看出，隐藏主要是为了重置BP中的状态转移关系，即如果状态转移关系在N中是交互活动，它将在重置的状态迁移关系中保持不变。同时，将N中本地活动设置为外部不可见活动τ，形成τ-迁移关系。

在获得隐藏业务过程之后，还需将其中所有τ-迁移关系全部移除。目前，研究人员已经提出了多种行为最小化技术[11]，如轨迹最小化，分支最小化和互模拟最小化等。由于本文的重点是协同业务过程路径和域约束的一致性，弱轨迹等效性[11]被用于最小化隐藏业务流程。具体的最小化过程见算法1。

算法1生成抽象业务过程。

输入: 隐藏业务过程N=(S, s0, ψ, γ, Δ);

输出: 抽象业务过程Na=(Sa, sa0, ψa, γa, Δa)。

1. S0=τ-closure({s0});

2. 置S0为未访问，并将其添加至Q;

3. whileQ≠φthen

4. 取Q中未访问的状态Su;

5. forN中每一个交互活动ado

6. Sv=τ-closure(tran(Su, a));

7. if Sv∉Q then

8. 置Sv为未访问，并将其添加至Q;

9. 把(Su, a, Sv)加入Δa;

10. else

11. 把(Su, a, Sv)加入Δa;

12. end if

13. end for

14. end while

15. 把S0作为初始状态sa0;

16. 把包含ψ的状态Se加入ψa;

17. 把Sa和γa分别设为Q和γ;

18. return Na;

算法1中，给定业务过程N中状态集D∈S,函数τ-closure(D)定义从D中任意状态出发，通过标记为τ的路径到达的状态集；而函数tran(D,a)定义从D中任意状态出发，经过活动a转换到达的状态集。

经算法1构建抽象业务过程也符合定义1中业务过程定义。因此，可利用并发操作符将抽象业务过程集组合，得到抽象协同业务过程。

由于模型验证技术不需要在检测过程中进行人工干预，并且可以提供反例信息以在验证失败时纠正错误，在构建完成抽象协同业务过程后，本文利用模型检测技术对其进行符合性验证。目前，较为著名的模型验证工具有NuSMV[注]http://nusmv.fbk.eu/。、PAT及SPIN[注]http://spinroot.com/spin/whatispin.html。等。PAT具有用户友好界面、内置高效LTL检测器，以及可方便地将LTS转换为PAT输入语言CSP#等特点，因此本文采用PAT作为符合性自动验证工具。

由于CSP#能够良好地以文本方式描述LTS，且为避免在符合性验证前，显式地构建协同业务过程状态空间从而实现On-the-fly验证，本文提出如表1所示的映射规则，用于将协同业务过程映射为CSP#进程。其核心思想是将协作中产生的每条消息映射为整形变量，每个业务过程映射为CSP#进程及协同业务过程映射为所有业务过程进程并发组合，以模拟协同业务过程点火规则的执行。

表1 协同业务过程到CSP#进程转换

针对表1给出的映射规则，具体说明如下：

针对协同业务过程中每条消息msg，msg被映射为初值为0的整形变量，表示开始时msg不存在；

每个业务过程BPi用其初始状态标识进程表示，且BPi中每个状态均对应一个进程；

对于每个业务过程中任意迁移，根据触发活动不同，将其分为3类：①若触发活动是异步发送活动，则在该迁移发生后将消息msg加1(即产生消息msg)，并在执行完发送后迁移至后续状态对应进程；②若触发活动是异步接收活动，则在该迁移发生前需判断消息msg是否存在。若存在(即msg>0)则执行接收，且在接收后将消息msg减1(即消耗消息msg)，并迁移至后续状态对应进程；③若触发活动是本地活动，则直接迁移至后续状态对应进程。这与定义5中描述协同业务过程点火规则一致；

最后，协同业务过程映射为每个业务过程对应进程的并发组合。特别地，由于业务过程间只涉及异步消息通信，采用CSP#中的交错算子“|||”组合业务过程进程。

由表1所示映射规则，在将抽象协同业务过程转换为CSP#进程后，则可将以CSP#进程表示的抽象协同业务过程和以LTL公式表示的领域约束(领域约束至LTL公式映射可参考CRL的具体内容[9])分别作为PAT的模型和性质输入，PAT(其集成了基于LTL公式的模型检测引擎)将自动完成一致性检测。根据PAT检测的结果，可以判断协同业务过程是否符合领域约束。如果存在任何差异，则可以根据反例中的信息找到并纠正协同业务过程中的问题。

4 有效性分析

由于本文默认协同业务过程在符合性验证之前具备正确性，基于协同业务过程构建抽象协同业务过程也具有正确性。为证明该结论，下面先给出定理1和引理1。

定理1给定隐藏业务过程N=(S,s0,ψ, γ, Δ)，经算法1生成抽象业务过程为Na=(Sa,sa0,ψa, γa, Δa)，则N与Na满足弱轨迹等价。

证明：分两种情况进行讨论：

(1)若N中无τ-迁移关系，则由算法1中构造的Na可知：

1)对于任意sa∈Sa，sa=2S；

2)对于任意状态迁移关系(sa-1,a,sa)={(su-1,a,su) |su-1∈S∧su∈S∧su-1∈sa-1∧su∈sa}；

3)sa0=s0；

4)sae∈ψa为包含ψ的状态。

根据上述条件可推出，对于轨迹σ∈traces(s0)，存在唯一对应轨迹σ∈traces(sa0)，故N与Na满足弱轨迹等价。其中：traces(s)表示从状态s出发可达任意轨迹。

(2)若N中有τ-迁移关系，则由算法1中构造的Na可知：

1)对于任意sa∈Sa，sa=2S；

2)对于任意状态迁移关系(sa-1,a,sa)={(su-1,a,su) |su-1∈S∧su∈S∧su-1∈sa-1∧su∈sa}；

3)sa0=s0；

4)sae∈ψa为包含ψ的状态。

根据上述条件可推出，对于任意轨迹σ1∈trace(s0)，则存在唯一轨迹σ2∈trace(sa0)，满足σ1的交互迹与σ2相同，故N与Na满足弱轨迹等价。

证毕。

证明：要证明Nt是正确的，则只需明确Nai能够正确执行，且执行交互活动序列与BPi一致即可。由N是正确的可知，对于从Ni初始状态s0可达的任意状态s，终止状态sf可以达到，即存在轨迹σ1和σ2，使得s0[σ1>s[σ2>sf。由定理1可知，Ni与Nai满足弱轨迹等价，则可推出sa1[χ(σ1)>sa[χ(σ2)>saf。由于saf是Ni终止状态，则根据算法1可知sf∈saf，推出saf是Nai的终止状态。根据定义9推出Nt具有正确性。

证毕。

证明：Na可看成是对N做n次替换后生成，即每次用Nai替换Ni(i∈[1,…,n])。根据引理1，每次替换后产生的协同业务过程也具有正确性，则经过n次替换后生成抽象协同业务过程为Na也是正确的。

证毕。

之后，证明给定任意符合性约束∅，其在协同业务过程和对应抽象协同业务过程上的验证结果一致。下面先给出引理2和引理3。

证明：采用反证法证明。设Nt与N不是弱轨迹等价，则根据弱轨迹等价定义可知，存在两个格局ct∈C(Nt)和c∈C(N)违反弱轨迹等价，其中函数C(N)定义N中所有可达格局。不妨设ct1和c1是第一个违反弱轨迹等价的格局，则可知这种违反是由Nai为Ni引起。根据定理2可知，在N正确的情况下，Nt也是正确的，从而推出若存在违反，则这种违反是由Nai为Ni间不具有弱轨迹等价引起，而这与定理1结论矛盾。

证毕。

证明：Na可看成是对N做n次替换后生成，即每次用Nai替换Ni(i∈[1,…,n])。根据引理2，每次替换后产生的协同业务过程与替换前具有弱轨迹等价，则经过n次替换后生成抽象协同业务过程为Na与N满足弱轨迹等价。

证毕。

证明：由引理3可知N和Na满足弱轨迹等价，则可推出N中任意一条交互迹，Na中存在唯一轨迹与之对应。因此，根据定义10可知，若N|=∅，则Na|=∅，反之亦然。

证毕。

由定理3，可将对协同业务过程符合性验证转换为对其抽象协同业务过程的验证。在保护流程隐私信息的前提下，这将极大地提高符合性验证效率。

5 实验评价

本文提出一种基于流程抽象的协同业务过程符合性验证方法，利用实际数据集来阐述本文所提方法的有效性。通过与其他相关符合性验证方法的实验对比，从避免暴露组织内部流程信息、符合性验证结果正确性及验证效率等方面来分析不同符合性验证方法的差异性。

5.1 实验准备

本文采用实际数据集来评价所提方法的有效性，但当前可供实验的针对协同业务过程公开数据集较少。因此选择实际数据集UA(university admission)[注]https://ai.wu.ac.at/emisa2015/contest.php。。UA中包括9个德国大学入学申请流程，它们均涉及多个组织间的交互，能够较为实际准确地反映协同业务过程的协作场景。

为了进行实验，随机地从数据集UA中选取5个协同业务过程。它们所具有的属性如表2所示，将协同业务过程中含有参与组织个数表示为 No. of peers，同时协同业务过程中含有的状态数及迁移数分别表示为No. of states, trans。

特别地，UA中每个入学申请流程均采用标准业务流程建模与标注(Business Process Modeling Notation，BPMN)描述。为便于实验，将上述5个入学流程中的每个业务过程先基于文献[10]中方法转换为Petri网描述，再将其转换为LTS描述。

表2 协同业务过程属性

同时，本文选择此类中典型方法[9-10]作为实验比较对象，从避免暴露组织内部流程信息、符合性验证结果正确性及验证效率等方面进行对比分析。

5.2 实验结果及分析

首先，通过对符合性验证之前协同业务过程中的本地活动分析，来评价本文方法在支持避免暴露组织内部流程信息方面的有效性。本文提出内部流程信息可见度(简称可见度)概念，用来定量评估组织内部流程信息暴露程度。

可见度计算式如式(1)所示:

(1)

式中，n为协同业务过程中含有业务过程数量。ψi如式(2)所示，用于计算第i个业务过程(即Ni)内部流程信息暴露程度，其中#Ni表示Ni中含有本地活动数量，而#N′i则表示在开展符合性验证前Nai中含有本地活动个数。对于可见度而言，其计算值越高，则表示其在更大程度上暴露组织内部流程信息。

(2)

利用式(1)，针对选取协同业务过程，文献[9-10]方法和本文提出方法计算得到的可见度如表3所示。

表3 可见度计算结果比较 %

由表3可知，文献[9-10]方法由于没有涉及对内部流程细节的处理，导致每个业务过程中内部流程细节全部暴露，因此可见度计算结果均为100%，这与跨组织环境下的隐私保护原则相违背。而本文方法考虑流程抽象，即针对每个业务过程，采用弱轨迹等价将其中含有的内部流程细节全部移除，因此能够实现组织内部流程细节全部隐藏，即可见度计算结果均为0%。

例如，针对TU_Munich，通过本文方法构建协同业务过程NTUM=Application||TUM，其中：业务过程Application和TUM分别如图2a和图2b所示。由图2可知，NTUM没有包含任何本地活动，而只含有交互活动，故ψ=0%。

通过对符合性验证结果进行分析，评估本文所提方法的有效性，以支持验证过程中不会引入误判。通过项目组讨论分析并咨询入学申请领域专家，设计两个领域约束为每个协同业务过程的测试用例。其中：TCtrue表示测试用例与模型一致，而TCfalse表示测试用例与模型存在不一致。首先，将每个协同业务过程转换为CSP#流程，然后调用PAT来验证是否符合领域约束，结果如表4所示。

表4 验证结果比较

从表4可以看出，本文方法可以识别出协同业务过程是否满足给定的领域约束(即TCtrue和TCfalse)，这表明本文的方法有效。但是，文献[9-10]提出的方法仅能识别TCfalse，而针对TCtrue则会引起误判。

例如，针对协同业务过程Hoh，通过咨询入学申请领域专家，设计如下领域约束Scenario A及Scenario B，其中：Scenario A对应TCtrue，而Scenario B对应TCfalse。

Scenario A：若Hohenheim向Application System提交入学申请(application)，则最后可以从Office获得申请结果(即reject、accept及reservation place)，且Admission Committee在收到Office发来文档(doc)后，下一步会向Office发送最终确认(final confirmation)。

Scenario B：若Hohenheim向Application System提交入学申请(application)，则只有在提交的入学申请被接受时，才能从Office获得申请结果(即accept及reservation place)。

通过利用文献[9]中LeadsTo和DirectlyFollowedBy模式，Scenario A对应的LTL公式如下：

Scenario A_LTL：□ (!application→◇?reject∨◇?resePlace∨◇?accept)∧□ (?doc→○!finalConfimation)。

而通过利用文献[9]中LeadsTo和isAbsent模式，Scenario B对应的LTL公式如下：

ScenarioB_LTL：□ (!application→◇?resePlace∨◇?accept)∧□ (┐?reject)。

针对本文所提方法，调用PAT验证TCtrue及TCfalse的结果如图3a所示，而针对文献[9-10]方法调用PAT验证TCtrue及TCfalse的结果则如图3b所示。

从图3可看出，本文方法针对TCtrue及TCfalse的验证结果分别为true和false，与期望结果一致；而文献[9-10]方法针对TCtrue及TCfalse的验证结果均为false。针对TCtrue，文献[9-10]方法验证结果与期望不一致主要是由Admission Committee中执行本地活动(如Receive application等)导致。

最后，基于影响符合性验证的相关因素，对本文提出方法的效率进行定量评价。文献[18]通过对实际数据集SAP参考模型[19]进行交互模拟，发现协同业务过程中含有节点数量远大于交互数量。同样，也通过对选取协同业务过程进行分析，其中含有节点数量及交互数量对比如图4所示。

从图4可看出，针对每个选取协同业务过程，其中含有交互数量均远小于节点数量(例如，Mue中含有55个节点数，但只有16个交互)，表明协同业务过程中内部流程细节所占比例远大于交互比例。

具体地，本文提出方法和文献[9-10]方法均采用的形式化分析方法为模型验证技术。其基本思想是：采用一个状态迁移模型M来表示待验证的系统，并采用时序逻辑公式∅表示需验证的性质，进而就可以将“系统是否满足所期望的性质”转化为“M是否满足公式∅，即M|=∅”。由于状态迁移模型M的状态空间决定了模型验证的效率及时间。为了对上述两类方法的符合性验证效率进行对比，采用文献[20]中的可达状态(reachable state)、有效迁移(fair transition)及系统直径(system diameter)三个指标进行评价。系统直径表示系统从初始状态到最远可达状态的距离深度；而可达状态和有效迁移则直接影响了模型验证的效率[20]，因为其数量反映了系统状态空间规模的大小。需要指出的是，此处的M指由选取协同业务过程(如Col等)根据定义5中点火规则生成的状态空间；而性质∅是用来表示领域约束的时序逻辑公式(如上文中Scenario A_LTL等)。

针对选取协同业务过程集，本文方法和文献[9-10]方法在符合性分析效率对比如图5所示。

从图5可看出，由于文献[11-12]方法在分析过程中没有对业务过程内部流程细节进行处理，导致其产生的可达状态、有效迁移及系统直径均远大于本文提出方法，因此文献[9-10]方法的分析效率显著低于本文提出方法。

例如，针对协同业务过程Mue，文献[9-10]方法进行符合性验证时需要搜索状态空间如图6a所示，而本文提出方法进行符合性验证时需要搜索状态空间则如图6b所示。

由图6可以看出，本文方法进行符合性验证时，需要搜索的状态空间远小于文献[9-10]方法，这表明由于本文方法将组织内部流程细节进行抽象，故符合性验证效率远高于文献[9-10]方法。

6 相关工作

协同业务过程的正确性、一致性及符合性是与本文工作相关的研究。接下来是对这3方面的一些典型文献的介绍和分析。

6.1 正确性验证方法

协同业务过程的正确性是指在设计阶段对协同业务过程进行验证，以判断其功能正确性(如无死锁等)。在国际上，文献[8]较早提出了跨组织工作流网(Inter-Organizational Workflow，IOWF)概念，被用于跨组织工作流建模。并利用组织内业务过程合理性的思想提出了IOWF正确性的定义，即要求每个参与组织业务过程是合理的，且IOWF的展开也是合理的。之后这方面的工作主要是以此为基础开展。为了有效地开展业务协同，文献[21]最初提出了一种利用面向交互的Petri网(Interaction-Oriented Petri Net, IOPN)构建的业务流程协作模型来描述业务协同，该模型由组织内的业务流程和组织之间的交互组成。然后引入了IOPN的弱合理性概念来定义IOPN的正确性。基于不变量分解方法，将弱合理的无回路IOPN分解为一组顺序图，以检查其逻辑结构的正确性。文献[22]首先提出跨组织逻辑工作流网(interorganizational Logical Workflow nets,LWNs)用来建模跨组织环境下的协同，并以此为基础给出了逻辑结构正确性的定义并进行了分析。文献[23]首先提出非对称自由选择网(Asymmetric-Choice Workflow Nets,ACWF-nets)用来建模不同业务过程间的交互，并以合理性定义ACWF-nets逻辑结构正确性；之后对ACWF-nets的合理性与ACWF-nets的结构性质间的关系进行讨论，从而将ACWF-nets的合理性验证转换为对其弱合理性的验证。文献[3]在工作流网WF-Net的基础上扩充资源和消息要素，提出了资源消息工作流程网RM_WF_net(Resource and Message WF-net)用于建模组织内业务过程，继而为得到协同业务过程，利用库所熔合技术合并业务过程间的消息库所。之后为了保证得到的每个参与组织的业务过程是正确的，使用合理性定义协同业务过程的正确性。因此，协同业务过程执行中产生的消息全部被接受，协同业务过程执行首尾状态一致且不存在死变迁，并借助Petri网可达图验证协同业务过程逻辑结构的正确性。鉴于公共管理所具有的交互特性，为了对其进行描述，文献[24]首先采用BPMN，然后将其转化为基于Petri网的模型，并对其具有的相关性质(如死锁等)采用Petri网的展开技术(unfolding-based technique)进行描述。基于此，可以确保公共管理交互特性的良好执行。

协同业务过程正确性关注其执行时需满足的普适性质[8]，通常采用合理性及其变体(如弱合理等)定义， 对其进行验证的目的是确保可以正确执行协同业务过程的前提下，实现特定的业务目标。一般情况下，只有在确保协同业务过程正确的前提下才有必要对其符合性进行验证[16]，因此协同业务过程正确性可视为其符合性验证的前提。

6.2 一致性验证方法

协同业务过程一致性是指构建出的协同业务过程与在构建前由参与组织协商确认的规约(即编排)一致。文献[25]较早对协同业务过程一致性验证方法开展研究，它先采用消息顺序图(Message Sequence Chart，MSC)来直观地建模编排，即从全局视角定义活动间同步及异步交互；之后采用IOWF构建协同业务过程；最后基于1-consistency来验证协同业务过程是否与编排一致。由于引入1-consistency，该方法能够在一定程度上缓解状态空间爆炸问题。为了增强可用性，文献[7]提出一种可视化的建模及一致性验证方法，该方法由建模和验证两个阶段组成。具体地，在建模阶段首先利用Web服务编排定义语言(WS Choreography Definition Language ，WS-CDL)及业务流程执行语言(Business Process Execution Language ，BPEL)来可视化地描述编排及可执行过程，之后将可执行过程中内部流程细节移除，得到抽象业务过程；而在验证阶段，首先将编排转换为通信顺序进程(Communicating Sequential Process，CSP)；之后将抽象业务过程也转换为CSP进程，进而将抽象业务过程对应CSP进程并发组合得到抽象协同业务过程进程；最后为了验证抽象协同业务过程是否与编排间具有精化关系(即迹等价)来判定一致性是否满足，可以采用模型检测工具FDR2(failures-divergences refinement)进行自动验证。为了从交互及业务意图两个层面来验证一致性，文献[26]提出一种基于Agent方法。该方法首先采用承诺(能够反映业务意图)及承诺模式(如Outsourcing模式等)来建模编排；然后采用统一建模语言(Unified Modeling Language ,UML)中顺序图来描述协同业务过程；最后将描述协同业务过程的顺序图和定义编排的承诺分别转换为NuSMV规约和CTL公式，并调用NuSMV自动判定一致性是否满足。

本质上，编排关注全局交互，而本文中的领域约束则关注局部交互，它们从两个不同视角规定协同业务过程执行应满足的性质。在实际验证中，它们可以结合使用，故一致性验证可视为符合性验证的有益补充。

6.3 符合性验证方法

协同业务过程符合性意味着协同业务过程的执行符合域约束。文献[27]提出了用于多个业务流程组合验证的概念框架。为了表示进程，该框架首先将BPMN建模的协同业务过程转换为以时间通信顺序进程CSP+T(communicating sequential processes+time)，然后为了定义预期的业务规则，使用时序逻辑公式，并利用在工具FDR2上自动验证该模型方法的符合性是否满足。因此，可以确定协同业务过程可以正确地调整以适应业务规则。为了确保协同业务过程与规定领域约束一致，文献[9]提出一种符合性管理框架。它先结合行为及资源等要素定义符合性语言CRL，并对CRL中包含模式及模式到LTL公式映射规则进行详细地阐述；然后提出利用SPIN模型检测器进行符合性检测的方法，并实现业务流程合规管理工具套件(Business Process Compliance Management tool suite ,BPCM)的原型工具。文献[12]提出一种验证协同业务过程的执行符合性方法。首先为了对协同业务过程进行建模，采用BPMN技术，然后组织的流程转换为ECATNets(Recursive ECATNets)，最后为了得到ECATNets中描述的模型，利用库所融合技术将每个组织的流程进行组合。由于该模型语义可以被解释为条件重写逻辑，为了有效地验证协同业务过程的行为满足相关约束，可以使用Maude LTL模型检测器来验证协同业务过程的执行符合性。然而，上述这些研究工作的关注重点仍是符合性验证中协同业务过程可视化建模、符合性管理框架设计、符合性语言设计等方面，并未涉及业务过程中内部流程细节处理。在实际验证中，忽视内部流程细节处理将导致组织隐私信息暴露、符合性验证误判及符合性验证效率低下等问题。

7 结束语

协同业务过程面向特定行业(如教育、制造及财务等)，验证其与给定应用领域特征(如行业特征、管理规范及法律法规等)相符是其有效实施的一个关键问题。基于流程抽象，本文提出一种协同业务过程行为符合性验证方法。该方法通过将针对协同业务过程符合性验证转化为对抽象协同业务过程符合性验证，能够有效地避免暴露组织内部流程信息、确保符合性验证结果的正确性及提高形式验证效率。

未来工作主要从以下两方面展开：①本文中仅考虑涉及协同业务过程行为的领域约束，如何验证包含其他要素(如资源、数据等)的领域约束将在下一步工作中详细讨论；②为避免重复符合性验证，如何基于给定领域约束对协同业务过程进行修正是一个值得研究课题。