业务流程建模标注2.0(business process modeling notation 2.0, 简称BPMN 2.0)^[1]是业务流程管理领域的一种标准符号.BPMN 2.0存在3种基本类型的端到端的业务流程, 分别是:编制(orchestration)、编排(choreography)和协作(collaboration).建模者不仅可以使用编制来建模组织内部的业务流程, 还可以使用编排来建模组织间业务流程的交互.与编制相比, 编排是在BPMN 2.0中首次提出的概念.它用于定义参与者(peer)之间的消息交互序列, 其关注点是参与者间的消息交换, 而非参与者内部的工作编制^[1].

一方面, BPMN 2.0具有面向图流程定义语言(graph-oriented process definition languages)的特征^[2]; 另一方面, 它还具有Web服务业务流程执行语言(Web service business process execution language, 简称BPEL)^[3]的特征.这使得BPMN 2.0编排不仅会表现出由面向图流程定义产生的语义错误, 例如流不一致(流增加或流减少)、死编排任务等, 还会表现出整体编排与局部参与者间语义不一致的错误, 例如可实现性(realizability)^[4].其中, 可实现性是指给定一个编排, 参与者未必总能正确实现该编排^[4].

由于上述原因, 对BPMN 2.0编排进行语义分析成为了BPMN 2.0编排建模工具所期望具有的功能.但是, 语义分析将面临下述挑战:一是, BPMN 2.0标准规约用自然语言描述编排的语义, 描述的语义存在不一致和二义性.二是, BPMN 2.0标准规约缺乏分析技术, 无法对编排进行语义分析.

面对上述挑战, 本文关注BPMN 2.0编排的形式语义定义和语义分析, 其主要贡献如下.

(1) 通过建立BPMN 2.0编排到工作流网(WF-nets)的映射, 使用Petri网来准确定义BPMN 2.0编排的语义.首先, 给出良构编排的概念, 以消除构造结构的多样性, 从而方便BPMN 2.0编排到工作流网的映射; 其次, 给出编排到工作流网映射的直观描述; 最后, 给出映射的形式定义.

(2) 借助Petri网的分析技术, 把BPMN 2.0编排中存在的语义错误规约为工作流网的结构问题或性质问题, 对BPMN 2.0编排进行语义分析.

(3) 本文实现了一种工具, 用于将BPMN 2.0编排自动转换为工作流网, 并借助现有的Petri网工具和自行设计的算法实现了对编排的语义分析.

本文第1节介绍编排和Petri网的相关概念.第2节定义良构编排.第3节讨论BPMN 2.0编排到Petri网的映射.第4节对编排进行语义分析.第5节是实验评估.第6节是相关工作的比较.最后是对本文进行总结.

1 相关基础 1.1 编排

在BPMN 2.0中, 编排由下述4种元素组成:编排活动(choreography activity)、事件(event)、网关(gateway)和序列流(sequence flow).编排的核心子集如图 1所示, 其中, 编排活动、事件、网关统称为流对象(flow object); 序列流又称为连接对象(connection object).本文将对图 1所示的编排核心子集进行形式语义的定义.

编排活动是编排中执行的工作, 分为编排任务和调用编排(call choreogprahy).编排任务又可分析为:标准编排任务(choreography task)和带内部标记(marker)的编排任务.标准编排任务是编排中的一个原子活动, 用以描述两个参与者之间的一次或两次消息交换.带内部标记的编排任务用于描述编排任务的重复执行, 包含3种类型:标准循环的编排任务(standard loop choreography task)、多实例并行的编排任务(parallel multi-instance choreography task)和多实例串行的编排任务(sequential multi-instance choreography task).调用编排是编排中的一个点, 用以调用全局编排(global choreography).

事件是发生在编排中的事情, 包含:开始事件(start event)、中间事件(intermediate event)和结束事件(end event).这些事件分别用以开始、中断、结束编排的流.其中, 开始事件可分为5种类型:无(none)、计时器(timer)、条件(conditional)、信号(signal)和多个(multiple); 中间事件可分为6种类型:无(none)、计时器(timer)、条件(conditional)、链接(link)、信号(signal)和多个(multiple); 结束事件可分为两种类型:无(none)和终止(terminate).

网关用于控制编排中序列流的收敛(converge)和发散(diverge), 包含3种类型:排他数据网关(data-based exclusive gateway)、排他事件网关(event-based exclusive gateway)和并行网关(parallel gateway).其中, 排他数据(事件)网关又包含:排他数据(事件)决策网关(data/event-based XOR decision gateway)和排他数据(事件)合并网关(data/event-based XOR merge gateway).排他数据(事件)决策网关用于从互斥的流中选择一个流; 排他数据(事件)合并网关用于将一组互斥的流合成为一个流.并行网关又包含:并行分叉网关(parallel fork gateway)和并行汇聚网关(parallel join gateway).并行分叉网关用于产生并发流; 并行汇聚网关用于同步并发流.

序列流用于连接流对象, 表示编排中流对象间的控制流关系.

1.2 Petri网

Petri网是1962年由德国科学家Petri博士在他的博士论文《用自动机通信》中创立的一种网状结构^[5].它是并发系统的一种形式模型, 通过流来建模系统的行为.此外, Petri网拥有大量的分析技术和工具, 可以方便我们对编排进行分析和验证.

Petri网是一个有向二分图, 由库所和变迁组成.其图形化的表示方式使得Petri网直观、易懂.通常, 库所使用圆圈表示, 变迁使用方框表示, 流关系使用有向线段表示, 托肯使用实心小黑点表示.

定义1^[6](Petri网). Petri网是一个4元组$\mathit{\Sigma } = (P, T;F, M), $其中,

(1) $P \cup T \ne \emptyset, $习惯称P为库所集, T为变迁集;

(2) $P \cap T = \emptyset ;$

(3) $F \subseteq (P \times T) \cup (T \times P), $称F为流关系;

(4) 映射$M:P \to \{ 0, {\rm{ }}1, {\rm{ }}2, {\rm{ }}3, ...\} $称为Petri网的一个标识.通常用M₀表示Petri网的初始标识.

定义2^[6](前集和后集). 设$\mathit{\Sigma } = (P, T;F, M)$是一个Petri网, 若$x \in P \cup T, \dot x = \{ y\left| {(y, x) \in F \wedge y \in P \cup T} \right.\}, $则称$\dot x$为x的前集; 若$x \in P \cup T, \dot x = \{ y\left| {(x, y) \in F \wedge y \in P \cup T} \right.\}, $则称$\dot x$为x的后集.

定义3^[7](工作流网). 一个$\mathit{\Sigma } = (P, T;F, M)$是工作流网(WF-net)当且仅当:

(1) 存在一个源库所$i \in P, $使得$\dot i = \emptyset ;$

(2) 存在一个汇聚库所$o \in P, $使得$\dot o = \emptyset ;$

(3) 每一个节点$x \in P \cup T$都位于从i到o的一条路径上.

本质上, 工作流网是Petri网的一类子网, 要求只有一个源库所和一个汇聚库所, 且每个变迁都在从源库所到汇聚库所的路径上.

定义4^[7](合理性). 设$\mathit{\Sigma } = (P, T;F, M)$是一个工作流网, 该工作流网是合理的当且仅当:

(1) 对于每一个从状态i可达的状态M, 存在一个实施序列, 从状态M通往状态o, 形式化表示为

$ {\forall _M}(i\xrightarrow{*}M) \Rightarrow (M\xrightarrow{*}o); $

(2) 状态o是从状态i可达的唯一最终状态, 且结束时其中至少会有一个标记, 形式化表示为

$ {\forall _M}(i\xrightarrow{*}M \wedge M \geqslant o) \Rightarrow (M = o); $

(3) 无死变迁

$ {\forall _{t \in T}}{\exists _{M, M'}}i\xrightarrow{*}M\xrightarrow{t}M'. $

2 良构编排 2.1 良构编排的定义

由于BPMN 2.0编排是面向流的, 所以使用Petri网来定义BPMN 2.0编排的语义是非常合适的.本节将提出良构编排的概念, 用于将结构不同但语义相同的编排转换为结构统一的编排, 以消除构造结构的多样性.这样做的好处是:在定义编排的形式语义时, 只需考虑良构编排到工作流网的映射.此外, 良构编排的提出主要是为了方便BPMN 2.0编排到工作流网的映射, 不会损失编排的一般性.

良构编排具有下述特征.

(1) 开始事件有一个, 且只有一个输出流, 而无输入流;

(2) 结束事件有一个, 且只有一个输入流, 而无输出流;

(3) 编排活动或中间事件均只有一个输入流和输出流;

(4) 编排活动只表示单向的发送或接收消息;

(5) 并行分叉网关、排他数据决策网关、排他事件决策网关只能有一个输入流, 多个输出流;

(6) 并行汇聚网关、排他数据合并网关、排他事件合并网关只能有一个输出流, 多个输入流;

(7) 网关必须与编排活动相连.

定义上述特征的目的在于规范编排的结构.其中, 特征(1)~(3)、(5)、(6)用于确保编制中只有网关能够控制流的收敛和发散, 而编排活动和事件只有一个输入流和输出流; 特征(4)用于确保编排中每个活动只描述单向消息发送; 特征(7)用于确保编排中不允许网关间直接嵌套.

为定义良构编排, 下面先定义核心编排过程和编排的语法.

使用图 2所示编排核心子集定义的编排过程, 称为核心编排过程, 参见定义5.

定义5(核心编排过程). 一个核心编排过程是一个5元组CP={O, CA, E, G, F}, 其中,

(1) O是流对象的集合, $O = (CA \cup E \cup G) \wedge (CA \cap E \cap G = \emptyset ), $即划分为3个不相交的集合CA, E和G;

(2) CA是编排活动的集合, $CA = (CT \cup Call) \wedge (CT \cap Call = \emptyset ), $即划分为两个不相交的集合, 分别是编排任务的集合CT和调用编排的集合Call;

(3) E是事件的集合, $E = ({E^S} \cup {E^I} \cup {E^E}) \wedge ({E^S} \cap {E^I} \cap {E^E} = \emptyset ), $即划分为3个不相交的集合, 分别是开始事件的集合E^S、中间事件的集合E^I、结束事件的集合E^E.其中, E^I又可划分为6个不相交的集合, 分别是正常事件的集合E^IN、计时器事件的集合E^IT、计时器事件的集合E^IC、链接事件的集合E^IL、信号事件的集合E^IS、多事件的集合E^IM;

(4) G是网关的集合,

$\begin{gathered} G = ({G^{PF}} \cup {G^{PJ}} \cup {G^{XD}} \cup {G^{DM}} \cup {G^{ED}} \cup {G^{EM}}) \wedge \hfill \\ ({G^{PF}} \cap {G^{PJ}} \cap {G^{XD}} \cap {G^{DM}} \cap {G^{ED}} \cap {G^{EM}} = \emptyset ), \hfill \\ \end{gathered} $

即可划分为6个不相交的集合, 分别是并行分叉网关的集合G^PF、并行汇聚网关的集合G^PJ、排他数据决策网关的集合G^XD、排他数据合并网关的集合G^DM、排他事件决策网关的集合G^ED、排他事件合并网关的集合G^EM;

(5) $F \subseteq O \times O$是连接对象的集合.

编排由一系列核心编排过程组成, 参见定义6.

定义6(编排). 编排是一个4元组$Chor = \{ CPs,Calls,map,ER\} ,$其中,

(1) CPs是核心编排过程的集合;

(2) $ Calls = { \cup _{cp \in CPs}}cp.Call$是调用编排的集合;

(3) $ map:Calls \to CPs$是一个单射函数, 用于将调用编排映射为一个核心编排过程;

(4) $ER = \{ (cp, cp') \subseteq CP \times CP\left| {\exists calls \in cp.Call, map(call) = cp'} \right.\} $是一个嵌入关系, 其中, cp′是cp的一个子核心编排过程.

函数map和关系ER用于描述BPMN 2.0编排中嵌入的编排过程.在BPMN 2.0编排中, 建模者可以使用不同的调用编排调用同一个核心编排过程.

为了定义良构编排过程, 对于编排过程中的流对象元素o∈O, 需引入两个辅助函数.o的输入节点定义为$in(x) = \{ x\left| {x \in O, (x, o) \in F} \right.\} ;$o的输出节点定义为$out(x) = \{ x\left| {x \in O, (o, x) \in F} \right.\} .$此外, 编排活动x的接收消息表示为$rec(x);$x的发送消息表示为$send(x).$

定义7(良构编排过程). 设$CP = \{ O, CA, E, G, F\} $是一个核心编排过程, CP是良构核心编排过程需同时满足下述条件.

(1) $\forall e \in {E^S}, in(e) = \emptyset \wedge \left| {out(e)} \right| = 1, $即开始事件有且只有一个输出流, 而无输入流;

(2) $\forall e \in {E^E}, |in(e)| = 1 \wedge out(e) = \emptyset, $即结束事件有且只有一个输入流, 而无输出流;

(3) $\forall x \in CA \cup {E^I}, \left| {in(x)} \right| = 1 \wedge \left| {out(x)} \right| = 1, $即编排活动或中间事件只有一个输入流和输出流;

(4) $\forall x \in CA, rec(x) \ne \emptyset \wedge send(x) = \emptyset \cup rec(x) = \emptyset \wedge send(x) \ne \emptyset, $即编排活动只表示单向的发送或接收消息;

(5) $\forall x \in {G^{PF}} \cup {G^{XD}} \cup {G^{ED}}, |in(x)| = 1 \wedge \left| {out(x)} \right| > 1, $即并行分叉网关、排他数据决策网关、排他事件决策网关只能有一个输入流, 多于一个的输出流;

(6) $ \forall x \in {G^{PJ}} \cup {G^{DM}} \cup {G^{EM}}, |in(x)| > 1 \wedge \left| {out(x)} \right| = 1, $即并行汇聚网关、排他数据合并网关、排他事件合并网关只能有一个输出流, 多于一个的输入流;

(7) $\forall x \in G, \exists y \in CA \wedge (x, y) \in F \cup \exists y \in CA \wedge (y, x) \in F, $即网关必须与编排活动相连.

定义8(良构编排). 设$Chor = \{ CPs, Calls, map, ER\} $是一个编排, Chor是良构编排当且仅当CPs的每个核心编排过程是良构的, 且ER是反对称的.

2.2 转换规则

若一个编排不满足良构编排的特征, 可使用图 2所示的7条规则对其转换, 使之变成良构编排.

(1) 规则1:若开始事件具有多个输出流, 可通过与具有多个输出流的并行分叉网关相连, 使之转换成一个具有一个输出流的开始事件;

(2) 规则2:若结束事件有多个输入流, 可通过与具有多个输入流的排他数据(事件)合并网关相连, 使之转换成一个具有一个输入流的结束事件;

(3) 规则3:若编排活动或中间事件具有多个输入流, 可通过与具有多个输入流的排他数据(事件)合并网关相连, 使之转换成一个具有一个输入流的编排活动或中间事件;

(4) 规则4:若编排活动或中间事件具有多个输出流, 可通过与具有多个输出流的并行分叉网关相连, 使之转换成一个具有一个输出流的编排活动或中间事件;

(5) 规则5:若编排任务表示双向消息, 可将该编排任务转换为两个紧邻的编排任务, 其中, 前驱编排任务表示单向发送消息, 后继编排任务表示单向接收消息;

(6) 规则6:若网关具有多个输入流和多个输出流, 可将该网关转换为两个紧邻的同类网关相连, 其中, 前驱网关与多个输入流相连, 后继网关与多个输出流相连;

(7) 规则7:若网关间通过序列流直接相连, 可在网关间增加一个编排任务.通常, 网关间的直接相连可以分为4种情况:并行网关与并行网关间的直接相连、排他网关与排他网关间的相连、并行网关与排他网关间的相连、排他网关与并行网关间的相连.为了简化和理解的方便, 图 2所示规则7中并没有显示区分排他数据网关和排他事件网关, 两者均用菱形框表示.

由定义4可知, 构成编排的基本建模元素是:开始事件、结束事件、编排活动(包含编排任务)、中间事件和网关.也就是说, 任意一个编排均是由这些建模元素组合而成; 结构不同的编排体现为建模元素的组合方式不同.另一方面, 上述7条转换规则的作用是将这些基本建模元素的输入流或输出流进行规范化处理.因而, 对任何一个编排, 我们总能唯一求出组成该编排的基本建模元素集, 并按照上述规则对这些基本建模元素依次进行转换, 最终得到良构编排.

3 编排到工作流网的映射

下面将定义良构编排到工作流网的映射.在工作流网中, 我们把变迁元素分为两类:标号变迁和空变迁.其中, 标号变迁用于建模编排中的编排活动和事件; 空变迁用于建模编排中的网关路由行为, 记为tau.这些路由行为在工作流网执行时将被视为空变迁, 不产生任何可视效果.

3.1 编排任务、事件、网关和序列流

图 3描述了BPMN 2.0编排中事件(开始事件、中间事件、结束事件)、编排任务、序列流及网关(并行网关、排他数据网关、排他事件网关)到Petri网片段的映射.

事件的映射包含3种情况:(1)开始事件被映射为Petri网中的一个库所、一个标号变迁及一个流关系, 且将该标号变迁的标号命名为start.映射过程不区分开始事件的类型, 均将其映射为标号变迁.(2)中间事件被映射为Petri网中的一个标号变迁, 且将该标号变迁的标号命名为:类型_中间事件名.映射过程不区分中间事件的类型, 均将其映射为标号变迁.(3)结束事件被映射为Petri网中的一个库所、一个标号变迁及一个流关系, 且该标号变迁的标号命名为end.映射过程不区分结束事件的类型, 均将其映射为标号变迁.

编排任务被映射为Petri网中的一个标号变迁, 且该变迁的标号命名采用:发送者_接收者_编排任务名的格式.

序列流的映射分为两种情况:(1)与排他数据(事件)网关相关的序列流被映射为Petri网中的一个库所和两个流关系; (2)与排他数据(事件)网关无关的序列流被映射为一个流关系.

网关映射分两种情况:(1)并行分叉网关和并行汇聚网关分别被映射为Petri网中带空变迁的Petri网片段, 以描述该网关的并行路由行为.(2)排他数据(事件)决策网关和排他数据(事件)合并网关被分别映射为Petri网中的一个库所, 以描述该网关的选择路由行为.此外, 映射过程不区分排他数据网关和排他事件网关.

3.2 标准循环的编排任务、多实例并行的编排任务和多实例串行的编排任务

标准循环的编排任务用以表示编排任务的重复执行, 存在两种情况:一种表示编排任务0至多次的重复执行, 称为While-do循环, 如图 4(a2)所示; 另一种表示编排任务1至多次的重复执行, 称为do-until循环, 如图 4(a3)所示.While-do循环映射为的Petri网片段如图 4(a4)所示; do-until循环映射为的Petri网片段如图 4(a5)所示.

多实例并行的编排任务用以表示编排任务实例的并行执行, 其实例数目(n)应在设计时指定.事实上, 一个多实例并行的编排任务可由同一编排任务的n个拷贝及并行分叉网关与并行汇聚网关与之相连所代替, 如图 4(b2)所示.多实例并行的编排任务映射为的Petri网片段如图 4(b3)所示.

多实例串行的编排任务用以表示多个编排任务实例的串行执行, 其实例数目(n)应在设计时指定.事实上, 一个多实例串行的编排任务可由同一编排任务的n个拷贝及序列流与之相连所代替, 如图 4(c2)所示.多实例串行的编排任务映射为的Petri网片段如图 4(c3)所示.

3.3 子编排

子编排可视为一个独立的编排.图 5描述了将一个具有单一开始事件和单一结束事件的子编排映射为Petri网片段的过程.在Petri网片段中, sub_start变迁用于建模子编排的开始, sub_end变迁用于建模子编排的结束, 变迁A_B_m1用于建模编排任务m1, 变迁B_A_m2用于建模编排任务m2.

子编排可以具有多个开始事件和结束事件, 但为了简化, 我们将子编排限制为只能具有单一的开始事件和结束事件.

3.4 初始标识配置

BPMN 2.0编排的初始状态可用对应Petri网的初始状态来描述.配置初始状态的基本思想是:对顶层编排中每个开始事件对应的库所中添加一个托肯, 对子编排中每个开始事件对应的库所中不添加托肯, 如图 6所示.

3.5 映射的形式定义

本节将形式化地定义BPMN 2.0编排到工作流网的映射, 见定义9.

定义9(BPMN 2.0编排的形式语义). 设Chor={CPs, Calls, map, ER}是一个良构编排, Chor被映射为一个工作流网(P, T; F, M), 其中,

$ \left. \begin{array}{l} P{\rm{ = }}{ \cup _{cp \in CPs}}(\{ {p_s}|e \in cp.{E^s}\} \cup ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~-开始事件\\ ~~~~~~~~~ \{ {p_e}|e \in cp.{E^E}\} \cup ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~-结束事件\\ ~~~~~~~~~ \{ {p_{(x, y)}}|(x, y) \in cp.F \wedge x \notin cp.{G^{XD}} \wedge x \notin cp.{G^{DM}} \\\wedge x \notin cp.{G^{ED}} \wedge x \notin cp.{G^{E{\rm{M}}}} \wedge y \notin cp.{G^{XD}}\\ \wedge y \notin cp.{G^{DM}} \wedge y \notin cp.{G^{ED}} \wedge y \notin cp.{G^{EM}}\} \cup \\~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~-与排他数据(事件)网关无关的序列流\\ ~~~~~~~~~ \{ {p_{\rm{g}}}|g \in cp.{G^{XD}} \vee \\g \in cp.{G^{DM}} \vee g \in cp.{G^{ED}} \vee g \in cp.{G^{EM}}\} ) ~~~~~~~~-排他数据(事件)网关 ~~~~~~~~~~~~~\end{array} \right\} $

(1)

$ \left. {\begin{array}{*{20}{l}} T{\rm{ = }}{ \cup _{cp \in CPs}}(\{ {t_{start}}|e \in cp.{E^s}\} \cup &-开始事件\\ ~~~~~~~~~~~~~~~~~~~~~ \{ {t_{end}}|e \in cp.{E^E}\} \cup &-结束事件\\ ~~~~~~~~~~~~~~~~~~~~~\{ {t_{type\_e}}|e \in cp.{E^I}\} \cup &-中间事件\\ ~~~~~~~~~~~~~~~~~~~~~\{ {t_{tau}}|g \in cp.{G^{PF}} \cup cp.{G^{PJ}}\} \cup =&-并行网关\\ ~~~~~~~~~~~~~~~~~~~~~\{ {t_{send{\rm{er}}\_receiver\_a}}|a \in cp.CT\} \cup &-编排任务\\ ~~~~~~~~~~~~~~~~~~~~~\{ {t_{call}}|g \in cp.Call\} ) &-调用编排 ~~~~~~\end{array}} \right\} $

(2)

$ \left. {\begin{array}{*{20}{l}} F{\rm{ = }}{ \cup _{cp \in CPs}}(\{ ({p_s}, {t_{s{\rm{tart}}}})|e \in cp.{E^S}\} \cup ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~-开始事件\\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\{ ({t_{end}}, {p_e})|e \in cp.{E^E}\} \cup ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~-结束事件\\ \;\;\;\;\;\;\;\{ (x, {p_{(x, y)}}), ({p_{(x, y)}}, y)|(x, y) \in cp.F \wedge x \notin cp.{G^{XD}} \\\wedge x \notin cp.{G^{DM}} \wedge x \notin cp.{G^{ED}} \wedge x \notin cp.{G^{E{\rm{M}}}}\\ \wedge y \notin cp.{G^{XD}} \wedge y \notin cp.{G^{DM}} \wedge y \notin cp.{G^{ED}} \wedge y \notin cp.{G^{EM}}\} \cup\\ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~-与排他数据(事件)网关无关的序列流\\ \;\;\;\;\;\;\;\{ (x, y)|((x, y) \in cp.F \wedge y \in cp.{G^{XD}} \cup cp.{G^{DM}} \cup cp.{G^{ED}} \cup cp.{G^{E{\rm{M}}}}) \vee \\ ((x, y) \in cp.F \wedge x \in cp.{G^{XD}} \cup cp.{G^{DM}} \cup cp.{G^{ED}} \cup cp.{G^{E{\rm{M}}}})\} )\\~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~-与排他数据(事件)网关相关的序列流 ~~~~~~~~~~~~~~~~~~~~~~~~~~~\end{array}} \right\} $

(3)

$ M(Ps) = 1~~~~~-每个开始事件对应生成的库所中添加 个托肯 $

(4)

在上述的形式定义中, (1)定义库所将由开始事件、结束事件、与排他数据(事件)网关无关的序列流及排他数据(事件)网关映射而来; (2)定义变迁将由开始事件、结束事件、中间事件、并行网关、编排任务及调用编排映射而来, 其中, 并行网关映射产生是空变迁; (3)定义流关系将由开始事件、结束事件、与排他数据(事件)网关无关的序列流及与排他数据(事件)网关有关的序列流映射而来.(4)定义托肯将由开始事件对应生成的库所映射而来.需要特别注意的是, 良构编排中不会出现网关与网关直接相连.所以, (3)中在定义与排他数据(事件)网关有关的序列流时, 只需说明序列流的一端与排他数据(事件)网关有关即可.

4 分析BPMN 2.0编排

第4.1节描述工具的设计与实现, 用于将BPMN 2.0编排自动映射为工作流网.第4.2节讨论BPMN 2.0编排中存在的问题.第4.3节讨论如何使用Petri网的分析技术对编排进行语义分析.

4.1 工具设计与实现

图 7是我们实现的转换工具Chor2PetriNet的结构.其中, YaoQiang BPMN Editor是一个图形化的编排编辑器, 用以创建编排模型; Pre-processor用以对编排模型进行预处理, 将语义相同但结构不同的编排模型处理为良构编排模型; Transformer根据第3节提出的映射, 用以将良构编排模型转换为工作流网.该工具以基于XML格式的BPMN文件作为输入, 以基于XML格式的PNML文件(Petri net markup language, 简称PNML)^[8]作为输出.PNML是存储Petri网模型的标准文件格式, 其好处是可被多个Petri网的建模和分析工具所支持.

4.2 编排中存在的问题

在将BPMN 2.0编排映射为工作流网的过程中, 我们发现了BPMN 2.0编排中存在的结构方面和控制流方面的问题.结构方面的问题是指编排无开始和结束或违背了BPMN 2.0标准规约中对编排的结构约束; 控制流方面的问题是指编排会出现死锁、活锁和死任务.下面对这些问题进行讨论.

(1) 编排缺少开始事件或结束事件.BPMN 2.0标准规约规定:开始事件用来表示编排的开始; 结束事件用来表示编排的结束.若编排缺少开始事件, 则编排不能直观、显式地描述业务流程间的交互从何处开始; 若编排缺少结束事件, 则编排不能直观、显式地描述业务流程间的交互在何处结束.图 8所示为没有开始事件和结束事件的编排.

(2) 编排违反了编排活动序列的基本规则(the basic rule of choreography activity sequencing).由于编排缺少集中机制, 因而编排中的参与者只能通过消息的接收或消息的发送来知道编排的进展.为此, BPMN 2.0标准规约规定:编排中的编排任务必须满足编排活动序列的基本规则, 即每个后继编排任务(除首编排任务外)的消息发送者必须为前驱编排任务的参与者.否则, 该编排任务将不知道前驱编排任务是否已经执行.图 9所示为违反了编排活动序列基本规则的编排.

(3) 编排中存在网关类型不匹配问题.在BPMN 2.0编排中, 并行网关与排他网关的混用将带来流的增加或流的减少.图 10(a)所示为并行网关和排他网关混用带来流的增加.图 10(b)所示为排他网关和并行网关混用带来流的减少.

(4) 编排存在死锁、活锁和死任务.编排存在永远无法执行的编排任务, 即死编排任务.图 11所示的编排存在无法执行的编排任务.对于编排中出现死锁和活锁的情况, 这里不再举例.

4.3 分析

针对上述编排中存在的4类问题, 我们将这些问题规约为工作流网的结构问题或性质问题, 并使用Petri网的分析技术对其进行检测.

针对问题(1):编排缺少开始事件或结束事件, 将此类编排转换映射为工作流网后, 可把此类问题规约为检测对应的工作流网中是否存在变迁的前集为空或变迁的后集为空的问题.在图 8所示的工作流网中, 变迁SSP Client_SSP_Invoice的前集为空, 则表示该编排缺少开始事件; 变迁SSP Client_SSP_Compliance的后集为空, 则表示该编排缺少结束事件.

针对问题(2):编排违反了编排活动序列的基本规则, 将此类编排转换映射为工作流网后, 可把此类问题规约为检测对应的工作流网中相邻标号变迁间的可见性问题, 即后继标号变迁的标号名字中的发送者必须出现在前驱标号变迁的标号名字中, 或是发送者, 或是接收者.在图 9所示的工作流网中, 后继标号变迁C_A_m2的发送者为C, 而前驱标号变迁的参与者是A和B, 则表示该编排的编排任务违反了编排活动序列的基本规则.

针对(3):编排中网关类型不匹配, 将此类编排转换映射为工作流网后, 可把此类问题规约为检测对应的工作流网中是否存在P-T结构或T-P结构的问题.在图 10所示的工作流网(a)中, 变迁tau和库所p4形成了T-P结构, 则表示该编排中存在网关类型不匹配; 在图 10所示的工作流网(b)中, 库所p1和变迁tau形成了P-T结构, 则表示该编排中存在网关类型不匹配.

针对(4):编排存在死锁、活锁和死任务, 将此类编排转换映射为工作流网后, 可把此类问题规约为检测对应工作流网的合理性问题.在图 11所示的工作流网中, 变迁A_B_m1是死变迁, 则表示该编排中存在死编排任务, 即为不合理的编排.

进一步地, 可将上述规约为的工作流网的结构问题或性质问题转换为对工作流网的结构分析或性质分析问题.其中, 结构分析包括:检测工作流网中是否存在变迁的前集为空或变迁的后集为空、检测工作流网中相邻标号变迁间的可见性及检测工作流网中是否存在P-T结构或T-P结构.性质分析包括:检测对应的工作流网是否合理.

对于检测工作流网中是否存在P-T结构或T-P结构及工作流网是否合理这一问题, 可把BPMN 2.0编排经Chor2PetriNet自动映射产生的PNML文件作为一个Petri网验证工具:WoPeD^[9]的输入, 使用WoPeD对其进行检测.

对于检测工作流网中是否存在变迁的前集为空或变迁的后集为空这一问题, 可把BPMN 2.0编排经Chor2PetriNet自动映射产生的PNML文件作为算法1的输入, 使用算法1对其进行检测.

对于检测工作流网中相邻标号变迁间的可见性问题, 可把BPMN 2.0编排经Chor2PetriNet自动映射产生的PNML文件作为算法2的输入, 使用算法2对其进行检测.

算法1.检测变迁.给定一个PNML文件, 输出该文件中是否存在前集为空的变迁或后集为空的变迁.

算法名:checking_transition.

输入:PNML文件;

输出:该工作流网中存在前集为空的变迁或该工作流网中存在后集为空的变迁或该工作流网不存在前集和后集为空的变迁.

BEGIN

  解析PNML文件;

  读取标签为〈transition〉的元素放入集合T中;

  读取标签为〈arc〉的元素放入集合ARC中;

  WHILE T中存在未被标识的元素

    BEGIN

    从T中任选一个未被标识的元素t并标识它;

      WHILE ARC中存在未被标识的元素

      BEGIN

        从ARC中任选一个未被标识的元素arc并标识它;

        IF arc的源点为t THEN

          source_flag=true;

        IF arc的目标点为t THEN

          target_flag=true;

       END

      IF source_flag!=true THEN

        BEGIN

          输出:该工作流网中存在后集为空的变迁;

          Break;

        END

      IF target_flag!=true THEN

        BEGIN

          输出:该工作流网中存在前集为空的变迁;

          Break;

        END

    END

    IF source_flag==true∧target_flag==true THEN

      输出:该工作流网不存在前集和后集为空的变迁;

END

例1:以图 8右边所示的工作流网作为算法1的输入, 算法1将检测出:变迁SSP Client_SSP_Invoice的前集为空, 变迁SSP Client_SSP_Compliance的后集为空.因而, 原编排缺少开始事件和结束事件.

算法2.检测相邻标号变迁间的可见性.给定一个PNML文件, 输出该文件中是否存在违反编排活动序列基本规则的变迁.

算法名:checking_ visibility.

输入:PNML文件;

输出:该工作流网中存在违反编排活动序列基本规则的变迁或该工作流网不存在违反编排活动序列基本规则的变迁.

BEGIN

  解析PNML文件;

  读取标签为〈transition〉的元素放入集合T中;

  WHILE T中未被标识的元素

    BEGIN

      从T中任选一个未被标识的元素t并标识它;

计算变迁t的后集的后集, 记为t^••;

WHILE t^••中未被标识的元素

        BEGIN

          从t^••中任选一个未被标识的元素t'并标识它;

          IF t'是标号变迁∧t'的发送者不是t的发送者或接收者THEN

          BEGIN

            输出:该变迁t'违反了编排活动序列的基本规则;

            t_flag=true;

            BREAK;

        END

      END

      IF t_flag!=true THEN

        输出:该工作流网不存在违反编排活动序列基本规则的变迁;

END

例2:以图 9右边所示的工作流网作为算法2的输入, 算法2将检测出:变迁C_A_m2的发送者为C, 其前驱变迁A_B_m1的发送者为A、接收者为B, 变迁C_A_m2的发送者不是前驱变迁A_B_m1的参与者.因而, 原编排违反了编排活动序列的基本规则.

5 实验 5.1 转换工具的性能及语义分析结果

本文将使用BPM AI过程模型库^[10](http://bpt.hpi.uni-potsdam.de/BPMAcademicInitiative)作为实验评估编排模型的数据源.BPM AI是由工业界和学术界合作创建的用于科学研究的流程建模平台, 合作组织的研究人员和学生使用平台提供的在线建模工具创建了大量的真实编排模型.我们共获得422个编排模型, 通过将相似和相同的编排模型过滤掉及人工方式的筛选, 最终选取了10个具有代表性的编排模型.

使用Chor2PetriNet工具对上述10个编排模型进行映射转换, 得到了对应的工作流网, 见表 1.运行该工具的笔记本电脑的软/硬件配置如下.

(1) 内存4G;

(2) 操作系统:Windows 7旗舰版64;

(3) 处理器:Intel(R) Core(TM) i5-3470 CPU @ 3.20GHz;

(4) JDK:1.8.0_65;

(5) Eclipse: Mars.1 Release (4.5.1).

表 1第1列为序号.该序号所对应的BPM AI过程模型中的编排文件名, 见表 2.表 1第2列显示了每个测试编排中编排任务、事件、排他数据(事件)网关及并行网关的数量.表 1的第3列显示了经工具映射转换后得到的工作流网, 该工作流网具有的库所、标号变迁及空变迁的数量.表 1的第4列显示了映射转换的时间(单位为ms).表 1的第5列显示了对编排的分析结果.

需要注意的是, (1)转换时间主要包括两部分:预处理时间和映射转换时间.其中, 预处理时间用于将编排转换为良构编排; 映射转换时间用于根据映射定义, 将编排映射为Petri网片段.(2)在BPM AI过程模型库中, 经分析我们发现, 编排容易产生的语义是:缺少开始事件或结束事件、违反了编排活动序列的基本规则及编排中网关类型不匹配, 存在死编排任务的编排不常见.例如, 序号1、3、4、10对应的编排缺少开始事件或结束事件; 序号2、6、9对应的编排存在网关类型不匹配; 序号7、10对应的编排违反了编排活动序列的基本规则.

例3:图 12中黑色箭头左边所示是表 1中序号7对应的编排, 图 12中黑色箭头右边所示是映射产生的工作流网.在工作流网中, 变迁start对应的是开始事件, 变迁end对应的是结束事件, 变迁Customer_Sales_verfiy对应的是编排任务Veriy RFQ, 变迁Sales_Customer_ask对应的是编排任务Ask for More Information, 变迁Customer_Sales_provide对应的是编排任务Provide Clarification, 变迁Engineering_Sales_analyze对应的是编排任务Analyze the RFQ and Provide L & M cost Estimates, 变迁Finance_Sales_add对应的是编排任务Add overhead costs and generate pricing portions, 变迁Sales_Customer_generate对应的是编排任务Generate Sales Quote, 变迁Customer_Sales_receive对应的是编排任务Receive Sales Quote_, 库所p2由排他决策网关生成.经语义分析后, 该编排违反了编排活动序列的基本规则, 其原因在于:在工作流网中, 变迁Engineering_Sales_analyze的发送者为Engineering, 其前驱变迁Customer_Sales_verfiy的发送者为Customer、接收者为Sales, 变迁Engineering_ Sales_analyze的发送者不是前驱变迁的参与者.

5.2 测试映射规则的一致性

本文第3节给出了编排到工作流网映射的直观描述和形式定义, 但没有讨论映射规则的正确性.讨论映射规则的正确性的关键是证明BPMN 2.0编排与映射生成的工作流网间行为等价.本节将对映射规则的一致性进行测试, 具体思路如图 12所示.第1步, 将BPMN 2.0编排使用Chor2PetriNet工具生成对应的工作流网; 第2步, 根据BPMN 2.0标准规约中对编排的语义描述, 采用人工方式生成BPMN 2.0编排对应的标号迁移系统; 第3步, 将映射生成的工作流网, 使用WoPeD工具生成对应的可达图; 第4步, 将标号迁移系统和可达图作为第5步的输入; 第5步, 测试标号迁移系统与可达图间是否满足弱互模拟关系, 若满足, 则该编排和工作流网是行为等价的; 否则, 行为不等价.更多关于标号迁移系统和弱互模拟的内容, 请参考文献[11].

上述测试映射规则一致性的思路是从弱互模拟关系的角度, 检测BPMN 2.0编排与映射生成的工作流网间是否满足行为等价.之所以选择弱互模拟关系作为行为等价检测的标准, 而不采用迹等价或强互模拟关系, 原因有二:一是, 映射产生的工作流网中具有tau变迁, 对观察者而言, 该变迁是透明的、不可见的.例如, 将并行分叉网关和并行汇聚网关映射产生的Petri网片段中便会出现tau变迁.由于强互模拟关系无法比较不可见动作, 因此, 本文不采用强互模拟关系.二是, 迹等价不区分选择的时机, 会将不确定性的可达图等价为确定性的可达图, 未考虑编排在某状态下的所有分支结构.因此, 本文也不采用迹等价.

针对表 1中列举的编排及其映射生成的工作流网, 我们通过人工分析的方式对映射规则进行了一致性测试.测试结果表明, 第3节提出的映射规则是一致性的.

6 相关工作

相关工作将从BPMN标准规约中编制与编排的形式语义定义、编排建模语言的形式语义定义及编排的语义分析这3个方面进行对比.

6.1 编制与编排的形式语义定义

BPMN 2.0标准规约使用自然语言定义了编制的执行语义^[1].但是, 用自然语义定义的编制的执行语义, 无法直接实现为工具, 用于对编制进行模拟、验证和执行^{[12, 13]}.为此, 文献[2, 12-18]使用不同的形式化方法定义了BPMN编制的形式语义.

文献[2]使用Petri网形式定义了BPMN 1.0编制子集的语义.它提出了BPMN中建模符号到Petri网元素的映射关系.这样做的好处是:可以使用Petri网丰富的分析技术对BPMN进行合理性检测.

文献[12]使用图重写规则(graph rewriting rule)形式定义了BPMN 2.0编制子集的执行语义.该文献建立了BPMN 2.0标准中非形式定义编制的执行语义与用图重写规则形式定义的编制的执行语义间的直接联系.这样做的好处是:每个形式定义规则的正确性都可以通过BPMN 2.0标准中非形式的规约来验证.此外, 该形式化的执行语义还可视作一个测试套件, 用来测试实现BPMN执行语义的工具的一致性.作为该文献工作的扩展, 文献[13]使用图重写规则形式定义了更大的BPMN 2.0编制子集的执行语义.

文献[14, 15]使用进程代数CSP形式定义了BPMN 1.0编制子集的语义.这样做的好处是:建模者可以使用形式语义检测不同抽象层次业务流程模型间的一致性.具体而言, 一方面, 建模者可以对业务流程模型领域相关的时序性质进行检测, 例如订单提交后, 一个响应必须在24小时内发送到客户端; 另一方面, 建模者可以对业务流程模型的通用性质进行检测, 例如:无死锁(deadlock-freeness)和正常结束(proper completion).通常, 在业务流程管理领域, 把对无死锁性质和正常结束性质的检测称为合理性检测(soundness checking).

文献[16]使用YAWL定义了BPMN 1.0编制子集的语义.它提出了BPMN元素到YAWL元素的映射关系.这样做的好处是:建模者可以使用YAWL的验证技术对业务流程模型的合理性和活性进行检测.

文献[17]使用进程代数COWS(calculus of orchestration of Web services)形式定义了BPMN 1.0编制子集的语义.这样做的好处是:基于形式语义, 建模者不仅可以对业务流程模型进行合理性检测, 还可以对业务流程模型(只要业务流程模型具有模拟信息)进行定量模拟.与文献[2, 14, 15]相比, 该文献从控制流和数据流两个方面定义了BPMN 1.0子集的语义.

文献[18]使用线性时序逻辑LTL(linear temporal logic)形式定义了BPMN 1.2编制子集的执行语义.这样做的好处是:一方面, 在LTL框架下, 建模者可以对业务流程模型的时序性质进行检测; 另一方面, 还可以为BPMN 1.2标准提供形式的语义规约.

文献[19]提出了一种模型转换的方法, 将企业流程建模语言TiPLM(Tsinghua InfoTech product lifecycle management solution)定义的工作流流程转换为行为等价的Petri网, 并使用WoPeD对Petri网进行了可靠性验证.TiPLM是一种类似BPMN编制的流程建模语言.

与上述文献相比, 本文关注的是BPMN 2.0编排的形式语义定义, 而非编制的形式语义定义.需要特别注意的是, BPMN 1.X(BPMN 1.0、BPMN 1.1和BPMN 1.2)中只有编制模型的概念, 没有编排模型.表 3从对象、方法、用途、范围这4个方面, 将本文工作与上述工作进行了对比和总结.本文定义的形式语义不仅可作为BPMN 2.0编排的语义规约, 用于消除二义性和不一致, 还可作为形式化分析的基础, 支持编排的语义分析.具体比较如下.

与文献[12-17]相比, 本文所做工作的区别在于:(1)关注对象.本文关注的建模语言是BPMN 2.0编排, 而这些文献关注的建模语言是编制.(2)使用的形式化方法不同.本文使用Petri网定义编排的形式语义, 而这些文献使用的是其他形式化方法定义编制的形式语义, 如CSP、YAWL、COWS、LTL、graph rewriting rule.

与本文工作最为相似的是文献[2]和文献[19]所做的工作.文献[2]使用Petri网形式定义了编制的语义, 与之相比, 本文所做工作的区别在于:(1)本文定义开始事件、结束事件、中间事件、排他数据(事件)网关和并发网关到Petri网片段的映射方式与文献[2]不同; (2)文献[2]使用库所融合的方式将映射得到的Petri网模块组合为一个Petri网, 而本文使用流关系将映射得到的Petri网片段组合为一个Petri网.这样做的好处是, 本文映射产生的Petri网具有更少的库所.(3)文献[2]中没有单独定义流关系到Petri网片段的映射, 而本文考虑了这一点.文献[19]使用Petri网形式定义了TiPLM工作流流程的形式语义, 并使用WoPeD对Petri网进行了合理性验证, 与之相比, 本文所做工作的区别在于:(1)在TiPLM工作流流程中, 建模元素有4种:开始事件、结束事件、任务和网关; 而本文定义的编排中, 建模元素有5种:开始事件、结束事件、编排活动、中间事件和网关, 其中, 编排活动包含编排任务和调用编排; (2) TiPLM工作流流程没有层次任务(hierarchical task), 不考虑层次性; 而本文定义的编排可以具有层次结构的子编排.

6.2 编排建模语言的形式语义定义

为定义编排, 大量编排建模语言被提了出来, 例如:BPMN 2.0^[1]、协作图(collaboration diagram, 简称CD)^[20]、Web服务编排规约语言(Web services choreography description language, 简称WS-CDL)^[3]、Let’s Dance^[21]、IPN(interaction Petri nets)^[22]、会话协议(conservation protocol, 简称CP)^[23].这些编排建模语言可分为两类:具有形式语义的编排建模语言和不具有形式语义的编排建模语言.具有形式语义的编排建模语言包括:CD、IPN和会话协议.针对不具有形式语义的编排建模语言, 文献[1, 24-26]使用不同的方法定义了编排的形式语义.

为了支持编排的定义, 与BPMN 1.X(BPMN 1.0、BPMN 1.1和BPMN 1.2)相比, BPMN 2.0首次提出了编排的概念, 将其视为“头等公民”^[1].BPMN 2.0标准规约中用自然语言描述了BPMN 2.0编排的语义, 但是用自然语义描述的语义存在二义性和不一致.

文献[24]使用Pi演算定义了Let’s Dance的形式语义.这样做的好处是:基于形式语义, 建模者可以把对编排的可达性(reachability)进行分析的问题规约为判断两个Pi演算进程间是否满足弱互模拟关系的问题.

文献[25]使用时间自动机(timed automata)形式定义了WS-CDL子集的操作语义.这样做的好处是:基于操作语义, 建模者可以使用UPPAAL工具来对编排进行各种性质的检测, 例如:不变量、可达性、前条件和后条件(pre and post conditions)、隐含属性(implication properties)和时间限制(time restriction).

文献[26]针对互连式编排建模存在的不足, 借鉴交互式编排建模的思想, 将BPMN 1.1扩展为iBPMN, 并使用交互式Petri网(IPN)形式定义了iBPMN的执行语义.这样做的好处是:一方面, 建模者可以避免对编排解释的二义性; 另一方面, 可以使用Petri网的分析技术对编排模型进行合理性分析.

文献[27]针对BPMN 2.0编排, 使用进程代数LOTOS NT定义了其形式语义.这样做的好处是:基于形式语义, 可以对BPMN 2.0进行可实现性(realizability)分析.

与上述文献相比, 本文关注的是BPMN 2.0编排的形式语义定义.表 4从编排建模语言、方法、用途、范围这4个方面, 将本文工作与上述工作进行了对比和总结.文献[24-26]分别针对的编排建模语言是:Let’s Dance、WS-CDL、iBPMN, 而本文关注的是BPMN 2.0编排.具体比较如下.

与文献[24-26]相比, 本文所做工作的区别在于:关注的编排建模语言不同.本文关注的编排建模语言是BPMN 2.0编排, 而这些文献分别关注的是其他编排建模语言:Let’s Dance、WS-CDL和iBPMN.

与本文工作最为相似的是文献[1]和文献[27]所做的工作, 文献[1]使用自然语言描述BPMN 2.0编排的语义, 会产生二义性和不一致; 而本文使用Petri网, 准确定义了BPMN 2.0编排的语义.文献[27]使用进程代数LOTOS NT定义了BPMN 2.0编排的语义, 而本文使用Petri网定义BPMN 2.0编排的语义.与文献[27]所做工作的区别在于:(1)文献[27]定义编排语义时, 限制网关必须是平衡的, 即若一个网关有n个输入分支, 则应有一个对应的网关有n个输出分支, 本文无此限制; (2)文献[27]没有考虑构造结构的多样性.(3)文献[27]未考虑标准循环的编排任务和子编排的形式语义定义.

6.3 编排的语义分析

编排作为参与者协同的全局规约, 需将其合成为每个参与者, 才能用于指导参与者的实现.但是, 合成的参与者未必总能准确实现编排^[28].进一步地, 给定一个编排, 能否将全局编排映射为每个参与者并确保这些参与者间的交互精确匹配流程编排, 这就是可实现性分析的内涵^[4].为此, 文献[4, 22, 23, 29-34]对编排进行了可实现性分析.这些方法大致可以分为3类:基于自动机的可实现性分析方法、基于进程代数的可实现性分析方法和基于Petri网的可实现性分析方法.

基于自动机的可实现性分析方法.针对基于会话协议定义的编排, 文献[23]以自动机作为形式化基础, 最早提出了会话协议可实现需满足的3个充分条件:无损连接(lossless join)、同步兼容(synchronous compatible)、自治性(autonomous).在此基础上, 文献[29-31]针对会话协议的子类, 提出了同步性条件(synchronizability conditions), 并将会话协议的可实现性分析转换为对同步性条件的检验.文献[32]针对任意发起者的会话协议(arbitrary-initiator protocols), 提出了一个新的充分条件, 用于检验会话协议的可实现性.文献[33]提出了会话协议可实现的充分必要条件, 将可实现性分析转换为对同步性和合适性(well-formedness)的检测, 从而可使用现有的行为等价检测工具和模型检测工具, 对会话协议的可实现性进行自动检测.

基于进程代数的可实现性分析方法.针对基于协作图定义的编排子类, 文献[4]以进程代数LOTOS NT作为形式化基础, 提出一种将协作图定义的编排形式转换为基于LOTOS NT定义的进程表达式的方法, 从强互模拟的角度, 检验了同步通信和异步通信环境下协作图的可实现性.针对BPMN 2.0中的编排子类, 文献[27]以进程代数LOTOS NT作为形式化基础, 提出一种把编排形式转换为LOTOS NT定义的进程表达式的方法, 从强互模拟的角度, 对同步通信环境和异步通信环境下编排的可实现性进行检验.在此基础上, 文献[34]提出一种模块化的框架, 用于自动验证WSDL、会话协议和BPMN 2.0编排的可实现性.

基于Petri网的可实现性分析方法.文献[22]以Petri网作为形式化基础, 用IPN定义编排, 并从分支互模拟的角度, 对同步通信环境下IPN的可实现性进行了分析.但Internet环境下存在网络延迟, 因此必须对异步通信环境下编排的可实现性进行分析.但是, 该方法只能分析同步通信环境下IPN的可实现性, 不能对异步通信环境下IPN的可实现性进行分析.

与上述文献相比, 本文的语义分析更关注从控制流的角度, 分析BPMN 2.0编排表现出由面向图流程定义产生的语义错误, 如流增加、流减少、死编排任务等.这样做的原因在于:从控制流方面, 确保编排的语义正确性是讨论可实现性的前提.因为, 可实现性分析本质上是讨论整体编排与局部参与者间的语义一致性.若整体编排的正确性无法保证, 则讨论整体编排与局部参与者间的语义将无任何实际意义.此外, 本文的语义分析还考虑了BPMN 2.0标准规约中对编排的结构约束:编排活动序列的基本规则.

7 结束语

BPMN 2.0标准规约中编排缺少形式语义及相应的分析技术, 这将阻碍对BPMN 2.0编排的语义分析.首先, 通过建立BPMN 2.0编排到工作流网的映射, 使用Petri网准确定义编排的语义; 其次, 借助Petri网的分析技术, 把BPMN 2.0编排中存在的语义错误规约为工作流网的结构问题或性质问题, 对BPMN 2.0编排进行语义分析; 最后, 通过实验表明, 这种形式化可以识别BPMN 2.0编排中存在的错误.

本文并没有考虑复杂网关和包含网关的语义定义.下一步的工作重点是:提出BPMN 2.0编排到参与者的映射算法、对BPMN 2.0编排进行可实现性分析以及根据Petri网中发现的问题, 自动地将其对应到原编排.