0 引言

    人工设计或自动构建的系统组合可能存在死锁、活锁等主要问题，特别是对于复杂信息系统。因此，系统交付前软件开发人员必须对信息系统进行严格的验证，以及时发现系统组合中存在的问题。

    目前使用的BPMN(Business Process Model Notation)流程验证方法主要集中在：(1)BPMN—Petri网映射及验证；(2)BPMN—Business Process Execution Language(BPEL)映射及验证；(3)BPMN—进程代数映射及验证等。

    文献[1，2]中，DIJKMAN R M等人提出的方法是将BPMN映射到Petri网。Petri网能揭示系统的许多并发特性，但是它只有模型而没有演算^[3]，对于一个复杂的信息系统，若将BPMN模型映射为其对应的Petri网模型也会相对比较复杂，因此，Petri网对于复杂信息系统的描述有一定的局限性^[4]。文献[5]展现了BPMN模型如何生成一个BPEL流程，但是采用的是人工方式，没有提供一个通用的自动解决方案。在文献[6，7]中，利用业务流程建模符号(BPMN)建立的业务流程模型可以直接映射到业务流程执行语言(BPEL4WS)，在业务流程执行引擎中直接运行,但并不是每一个BPMN元素和BPEL元素都可以形成一一对应，所以不可避免地存在映射对应问题，降低了效率。还有一些文献提出了将BPMN映射到进程代数的方法(如π演算)^[8]，这种方法需要基于MWB（Mobility WorkBench）验证工具来验证存在的死锁、活锁和平台不统一^[9]。

    文中验证方法直接实现为eclipse的一个插件，可在统一建模平台上直接处理BPMN模型的输出，从BPMN2.0开始直接生成java程序，有利于系统移植，减少验证的复杂度；同时在解决复杂信息系统的信息爆炸方面，本文实现了优化展开算法。

1 研究内容

1.1 业务流程建模

    BPMN2.0体系5种核心元素介绍如下：

    (1)流对象(Connecting Objects)

    活动(Activitics)：企业所作的工作,活动的类型包括:任务(Task)、进程(Process)和子进程(Sub-Process)。

    事件(Events)：业务流程的运行过程中发生的事情。包括启动事件、中间事件和结束事件。

    网关(Gateways)：用于控制流程的分支和聚合。使用最多的是互斥网关和并行网关。

    (2)连接对象(Connecting Objects)

    顺序流(Sequence Flow)：用来表示活动执行的顺序。

    关联(Association)：把流对象联系起来。关联用于展示活动的输入和输出。

    数据关联(Data Association)：用于将数据信息与流对象联系起来。

    消息流(Message Flow)：表示两个实体间消息的传递。

    (3)数据(Date）

    数据对象(Data Objects)：表示活动所需要或产生的数据。它们通过关联与活动连接起来。

    数据输入对象(Data Input Objects)：整个流程中可以被活动读取的外部数据。

    数据输出对象(Data Output Objects)：整个流程的输出数据量。

    数据存储(Data Store)：整个流程存储数据的地方，如数据库或文件。

    (4)泳道(Swimlanes)

    池(Pools)：描述流程中的一个参与者。可看做是将一系列活动区别于其他池的一个图形容器，一般用于B2B建模。

    道(Lanes)：是池的细分，代表同一实体的不同部分。

    (5)描述对象(Artifacts)

    组(Group)：用于分析文档，不会影响流程。

    注释(Annotation)：为了便于理解，提供一些附加性的文本信息。

1.2 流程到Java代码的转换

    本文在eclipse平台集成环境中设计并验证BP(Business Process)模型，eclipse插件的体系结构如图1所示。

    对于BPMN2.0模型，使用Xpand引擎给出了Java的形式化语义，Xpand引擎为每个BPMN2.0模型的元素创建了合适的Java代码。这个引擎专门用于代码生成，它是基于EMF框架和转换模板定义的。这就意味着能够从BPMN2.0流程开始直接生成Java程序代码。为了表示BPMN2.0元素的每个类型（例如开始、网关、事件等），介绍了适于支持验证的每种类型的具体方法，它们都遵循BPMN2.0的语义。定义如下方法：

    addPObject（）：一旦Activity被创建就被加到特定的进程中；

    setNext（）：设置它的下一个元素，定义BP的流向；

    setMsgToSend（）：用来表示发送消息的任务；

    sendMsg（）：是为了指定用setMsgToSend方法定义的Activity发送一个消息。

2 BPMN流程验证

2.1 优化算法及验证

    展开算法是一种较好的死锁检测的方法。它是一个偏序规约的技术，被广泛应用到Petri网和进程代数中，以减少验证活动中发生的状态爆炸问题。事实上，模型的展开算法是无限的，但如果在算法中设置一个特殊的点，称之为“结束前缀”或“截止点”，一旦构造了结束前缀， 找到识别活锁状态的截止点，就可以减少对路径的搜索，避免状态爆炸问题，这样就实现了展开算法的优化。

2.2 BPMN验证

2.2.1 活锁验证

    对于活锁的验证，利用配置树找到识别活锁状态的截止点。当且仅当在配置树的一个祖先节点的勘探阶段已经观察到当前节点时，路径是活锁，并标记当前这个点为截止点。截止点的标识可以有效防止复杂信息系统的状态爆炸问题。活锁的BPMN流程图如图2所示。

    图2 BPMN流程不用转换成状态较多的Petri网而生成Main.java。

    public Main(){

        Process Process_1= new Process("Process_1");

        Activity ExclusiveGateway_1 = new Activity

        (Activity.GATEWAY_EXCLUSIVE); 

        Activity Task_2 = new Activity(Activity.TASK);

        Activity Task_1 = new Activity(Activity.TASK);

        Activity StartEvent_1 = new Activity(Activity.EVENT_START);

        Activity EndEvent_1 = new Activity(Activity.EVENT_END);

        Process_1.addActivity(ExclusiveGateway_1);

        Process_1.addActivity(Task_2);

        Process_1.addActivity(Task_1);

        Process_1.addActivity(StartEvent_1);

        Process_1.addActivity(EndEvent_1);

        ExclusiveGateway_1.setData("EG 1");

        ExclusiveGateway_1.setNext(EndEvent_1);

        ExclusiveGateway_1.setNext(Task_1);

        Task_2.setData("T2");

        Task_2.setNext(ExclusiveGateway_1);

        Task_1.setData("T1");

        Task_1.setNext(Task_2);

        StartEvent_1.setData("S1");

        StartEvent_1.setNext(ExclusiveGateway_1);

            EndEvent_1.setData("E1");

    }

    参照上面的代码段，涉及到图2 Process1中的元素，把Process1中所创建的S1、EG1、T1、T2、E1分别作为不同类型的Activity：START、GATEWAY_EXCLUSIVE、TASK、TASK、END。对每个元素都用setNext方法设置它的下一个元素；对于发送消息的任务，用setMsgToSend方法；发送消息用sendMsg方法。那么，对象就添加到程序中了。图2示例验证结果如图3所示。

2.2.2 死锁验证

    对于死锁的验证，遵循BPMN2.0的终止范式。在BPMN2.0中，进程执行期间，结束或终止事件发生时，BP才会终止。从配置中一一删除结束事件，路径发生死锁当且仅当当前配置中有阻塞元素（即任务或事件等待消息并且一个并行网关等待的输入流将永远不会到来），就说明路径有死锁发生，这种方法也符合展开算法。死锁的BPMN流程图如图4所示。

    图4 BPMN流程不用转换成状态较多的Petri网而生成Main.java(略)。图4示例验证结果如图5所示。

2.3 Petri网验证BPMN流程

    DIJKMAN R M等人提出的用Petri网验证BPMN流程是将BPMN模型转换为等价的Petri网模型，BPMN模型在ILOG BPMN Modeler中创建并使用ProM验证。

    死锁、活锁定义：Petri网模型的可达图G=<V：E>是有向图，顶点集V是Petri 网的状态集合{M(P₀，P₁，…，P_n)}；

     有向弧E记录可执行变迁及其引起的状态迁移。当遍历完Petri网的所有变迁后，库所能够到达结束库所并且其他的库所都是空的时，这个流程是可达的。当可达树中，叶子节点的状态标识存在P_i=1但不是结束库所的库所时，流程存在死锁。当可达图G的任一条路径L_i=M₀→M₁…M_n(M_i表示库所变迁后的状态)表示从初始状态到结束状态，那么若任一路径中存在L_i=M_i→M₁→M₀→M₁…M_j（M_i=M_j），则流程存在活锁^[10]。

2.3.1 Petri网的活锁验证

    如图6所示是图2的BPMN模型转化为等价的Petri网模型， P₁和t₁是开始库所和变迁，P₆和t₆是结束库所和变迁。图6的Petri网手工模拟分析结果如图7所示。

2.3.2 Petri网的死锁验证

    如图8所示是图4的BPMN模型转化为等价的Petri网模型，用圆圈表示Petri网的库所，用长方形表示Petri网的变迁，P₀和t₀是开始库所和变迁，P₁₃和t₄是结束库所和变迁。图8 的Petri网手工模拟分析结果如图9所示。

3 验证结果分析

    对比BPMN模型和Petri网模型，如表1。

    通过以上对两种验证死锁和活锁方法的比较以及表1，可得出本文的BPMN直接验证法优点：

    (1)BPMN模型比等价的Petri网模型的图元总数少。BPMN模型转换成等价的Petri网模型时，随着BPMN模型的复杂度提高，生成的Petri网模型复杂性也会增加。

    (2)BPMN模型验证可在统一建模平台上直接处理BPMN模型输出，从BPMN2.0开始直接生成Java程序，并自动检验业务流程模型中可能存在的死锁、活锁。BPMN模型转换成等价的Petri网模型时，不可避免地存在映射对应问题，降低了效率。

    (3)对于一个复杂的信息组合系统，用BPMN模型直接验证，可采用“截止点”防止状态爆炸问题。但若将BPMN模转换成等价的Petri网模型，状态增多，同时Petri网所引起的状态爆炸问题和资源消耗问题很难避免，对于复杂信息系统的描述有一定的局限性。

4 结束语

    本文研究了对BPMN流程的直接验证方法，并与Petri网验证作比较，通过对两个典型的死锁、活锁例子的整个过程的建模、转换和验证，结果表明对于复杂系统，所提方法可以验证死锁、活锁并有效地避免状态爆炸问题和映射问题，且平台统一，可移植性好。今后的工作准备引入π-演算，在统一平台上实现π-演算的形式化验证。

参考文献

[1] DIJKMAN R M，DUMAS M，OUYANG C.Semantics and anaIysis of business proces models in BPMN[J].Information and Software Technology，2008，50(12)：1281-1294.

[2] DIJKMAN R M，DUMAS M，OUYANG C.Formal semantics and anaIysis of BPMN process models using Petri Nets[J].Information and Software Technology，2008，50(12)：1281-1294.

[3] 钱军，冯玉琳．系统动态行为语义模型及其形式描述[J]．Journal of Computer Research&Development，1999，36(8)：907-914.

[4] 朱明英.基于BPMN的Web服务组合模型的形式化分析[D].天津：南开大学，2009.

[5] WHITE S.Using BPMN to model a BPEL process[J].BP Trends，2005，3(3)：1-18.

[6] 秦天保.从BPMN到可执行业务流程建模[J].计算机应用，2006(S1)：266-268，284.

[7] 魏明，夏永霖，魏峻.BPMN到BPEL2.0的模型转换方法[J].计算机应用研究，2008(11)：3363-3366.

[8] 云本胜.基于π-演算的信任Web服务组合建模[J].计算机科学，2012(S3)：240-244.

[9] 李元，李祥.通信系统演算CCS与自动验证工具MWB[J].通信技术，2005(S1)：178-180.

[10] 怀文佳，刘旭东，孙海龙，等.一种基于时间Petri网的业务流程模型验证方法[C].2010年全国软件与应用学术会议(NASAC2010)论文集，2010：76-81.