MDA框架中CIM业务流模型与PIM工作流模型的一致性验证

李宗花 常逢佳

(淮阴师范学院计算机科学与技术学院 江苏 淮安 223300)

0 引 言

模型驱动体系结构(Model Driven Architecture，MDA)中，计算无关模型(Computation Independent Model，CIM)代表业务视图，主要描述系统被使用的情形，关注系统的环境和需求而不需要了解系统结构的细节[1-2]。而平台无关模型(Platform Independent Model，PIM)代表系统视图，描述独立于平台的功能实现细节[1,3]。PIM层次上的工作流模型与CIM层次上的工作流模型相比，具有更多、更完善的实现细节。然而PIM层次上的初始工作流模型往往由CIM层次上的工作流模型转换而来。经过完善和细化(refinement)的PIM工作流模型如果改变了CIM层次上规定的动作执行顺序，表明实现一个业务服务的执行流程被更改，说明工作流模型的细化和改进改变了业务需求。这些细化和完善操作会造成分析与设计上的二义性。对于一个业务系统来说，系统视图上工作流的细化和完善，是否造成业务需求的改变，会对业务系统的最终质量产生重要的影响[4]。因此，分析PIM层次上的工作流模型与CIM层次上的业务流模型的语义一致性显得尤为必要[5]。

语义一致性的验证不但存在于模型与模型之间[5-6]，还存在于构件与构件之间[7]及知识库的实体链接上[8]。Xiu等[5]利用Petri模型解决业务流程模型中的数据不一致问题，而文献[6]基于通用本体语义，构建了三层本体元模型语义的一致性验证流程。文献[7]使用带有语义约束的UML交互概观图来表示基于场景的需求规约，通过对语义扩展接口自动机模型(SIA)和带语义约束的UML交互概观图的行为的理论分析，解决构件之间的语义一致性验证。在知识库实体方面，文献[8]提出一种利用知识库实体间结构化语义的一致性集成实体链接算法，提高实体链接的准确率和召回率。文献[9]提出了使用系统行为属性的方法来验证模型精化过程中模型间的一致性，从而找出模型精化过程中的不一致行为。

可见，利用形式化方法验证语义一致性是当前的主流方法。在模型语义一致验证方面，Petri网作为一个被广泛使用的形式化模型[10]，无论是控制流、对象流还是信息流，Petri网适用于描述系统的这些“流”行为，该特征使得Petri网更好地定义业务流的语义[11-12]。当前诸多研究显示，Petri网能够形式化MDA框架中与业务系统或信息系统行为有关的每一个层次模型[13]。在CIM抽象层次上，Dijkman等[14]提出将BPMN模型映射至Petri网模型，并应用有效性分析技术分析业务过程模型的死锁与模型正确性状态。在PIM抽象层次上，Petri网可以直接描述PIM模型并直接在平台上自动执行[15]；在PSM抽象层次上，Petri网用于描述业务服务模型，且可以直接在DENEB(Development and execution of interoperable dynamic Web processes)平台上执行[12]；在代码层，Philippi[16]实现了Petri网模型自动生成代码的功能。此外，Petri网标记语言[17-18](Petri Net Markup Language，PNML)是一个基于XML交换格式描述Petri网的语言，能够被众多的Petri网建模工具和分析工具识别和读取，如YAML[19]和ePNK[20]。

因此本文利用Petri网模型对CIM层次的业务流模型和PIM层次上的工作流模型进行一致性语义分析。

1 扩展的Petri网模型

定义1一个工作流模型被定义为一个八元组组成的扩展Petri网模型[21]，即PN=。其中：IP={ip1,ip2,…,ipn}表示有限个内部工作流的集合；OP={op1,op2,…,opn}表示有限个外部工作流的集合；ST={st1,st2,…,stn}表示有限个开始、结束和网关元素的集合，sti表示工作流模型中的某个开始节点、结束节点或网关节点；BT={bt1,bt2,…,btn}表示有限个动作元素的集合；IA⊆(IP×ST)∪(IP×BT)∪(OP×ST)∪(OP×BT)表示一组输入弧；OA⊆(ST×IP)∪(ST×OP)∪(BT×IP)∪(BT×OP)表示一组输出弧；M0表示初始标识；SN=sub表示子工作流模型。

定义2对于任意Petri网模型EPN=，∃∀st1,st2∈ST，若IP(bt1×ip1)=IP(ip1×bt2)，或者OP(bt1×op1)=IP(op1×bt2)，则设定ρ:bt1→bt2，表示动作节点bt1和bt2之间存在顺序关系，bt1和bt2是一个执行顺序对，表示为bt1→bt2，表明bt1在bt2之前实施。ρ表示连接这两个节点的place节点。本文定义source(·)和target(·)两个函数表示连接IP或OP节点的前驱节点和后继节点，因此有source(ρ)=bt1，target(ρ)=bt2。

而多个执行顺序对，加上开始顺序对和结束执行顺序对就可以组成一个执行顺序序列Pi={st1→bt1→bt2→…→stn}。

2 语义一致性验证

2.1 验证思路

由于在PIM抽象层次上需要进一步细化工作流，CIM抽象层次上的业务活动在PIM抽象层次上将被细化为若干个原子活动。因此，这两个层次模型的语义一致性验证主要考虑细化的程度，即CIM层次上的活动及活动的执行顺序在PIM层次上做了何种修改。

因此，本节定义了PIM工作流模型与CIM业务流模型之间存在三种不同情形的细化：(1) 分层独立，在PIM工作流模型中完全找不到一个CIM业务流模型中的原子活动(事件或任务)。(2) 分层细化，在PIM工作流模型中存在一个参与者对象，当且仅当找到一个该参与者对象所作用的原子活动，这一原子活动在CIM业务流模型中也是由该参与者作用的。(3) 部分细化，在PIM工作流模型中存在一些原子活动与CIM业务流模型中的原子活动相互交织。

2.2 语义验证方法

接下来从形式化语义上定义CIM业务流模型与PIM工作流模型之间三种不同情形的细化条件。

给定CIM业务流模型PN1，PIM工作流模型PN2，设∑C1表示模型PN1中所有活动元素的集合，∑C2表示模型PN2中所有活动元素的集合。∑C=∑C1∩∑C2表示为PN1和PN2中相同活动的集合。在判断CIM业务流模型是否与CIM工作流模型语义一致时，必须先判断它们相同活动的执行顺序对集合是完全一致的，即∑(SequencePN1|∑C)=∑(SequencePN2|∑C)。当该条件满足的情况下，设∑Sequence-pn1表示PN1模型中的所有执行顺序对集合，∑Sequence-pn2表示为PN2模型中的所有执行顺序对集合，则满足以下条件：

(1) 分层独立。∀Sequence-pn2i,Sequence-pn2j∈∑Sequence-pn2，∃source(Sequence-pn2i)∈∑C1∩∑C2且target(Sequence-pn2i)∈∑C2-∑C1，∃source(Sequence-pn2j)∈∑C2-∑C1且target(Sequence-pn2j)∈∑C1∩∑C2，则表示PN2模型的细化和提炼操作属于分层独立。这意味着在细化后的PIM工作流模型中找不到任何一个CIM业务流模型中的原子活动。

以图1所示的CIM业务流模型和PIM工作流模型来说明分层独立的问题。图1中下方所示的工作流模型中存在执行顺序对B→SP1-A，其source(B→SP1-A)∈{A,B,C}，而target(B→SP1-A)∈{SP1-A,SP1-B,SP1-C}；同时还存在一个执行顺序对SP1-C→C，source(SP1-C→C)∈{SP1-A,SP1-B,SP1-C}，而target(B→SP1-A)∈{A,B,C}；这两个执行顺序对分别表示CIM业务流模型中子过程SP1的输入流节点和输出流节点。而细化后的PIM工作流模型中这两个执行顺序对的前驱节点和后继节点却与BPMN模型中保持一致。因此，图1中虚线框内的原子活动节点对于CIM业务流模型中的子过程SP1来说属于分层独立。

图1 PIM工作流模型分层独立

(2) 分层细化。∀Sequence-pn2i,Sequence-pn2j∈∑Sequence-pn2，∀ati∈∑C1∩∑C2，∀x,y∈∑C2-∑C1，∃sequence-pn2i:x→ati,sequence-pn2j:ati→y，则表明PN2模型针对PN1模型的细化和提炼操作属于分层细化。意味着在细化后的PIM工作流模型中当且仅当能找到一个原子活动ati，该原子活动同时也在CIM业务流模型中存在。

以图2所示的CIM业务流模型和PIM工作流模型来说明分层细化的问题。从图2中下方所示的PIM工作流模型中可见，原子活动B∈∑C1∩∑C2，而与节点B存在执行顺序关系的节点SP1-A,SP1-B∈∑C2-∑C1，存在两个执行顺序对SP1-A→B和B→SP1-B。这表明在子过程SP1中将CIM业务流模型中的原子节点B作为细化模型中的原子活动，即原子节点B的直接前驱和直接后继都是属于子过程SP1的原子活动。可见，图2中虚线框内的原子节点是子过程SP1的分层细化。

图2 PIM工作流模型分层细化

(3) 部分细化。∀ati∈∑C2-∑C1，∃Sequence-pn2i:ati-1→ati，Sequence-pn2j:atj-1→ati，或者∃Sequence-pn2i:ati→ati+1,Sequence-pn2j:ati→atj+1，其中ati-1,ati+1∈∑C2-∑C1，atj-1,atj+1∈∑C1∩∑C2，细化的PIM工作流模型中至少有一个原子活动ati，它的紧邻前驱节点或者紧邻后继节点存在多个。

同时，∀Sequence-pn1i∈∑Sequence-pn1，∃source(sequence-pn2j)=source(sequence-pn1i)，或者∃target(sequence-pn2j)=target(sequence-pn1i)，表明在细化的PIM工作流模型中，原子活动ati的多个执行顺序对中至少存在一个执行顺序对，其源节点或者目标节点是CIM业务流模型中的原子活动。表明细化后的PN2模型中的原子活动节点与PN1模型中的原子节点存在相互交织的情况。满足这种条件的PN2模型针对PN1模型的细化和提炼操作属于部分细化。

以图3所示的CIM业务流模型和PIM工作流模型来说明部分细化的问题。从图3中下方的工作流模型可见，与原子活动节点SP1-B有关的执行顺序对包括三个：SP1-A→SP1-B，D→SP1-B，SP1-B→SP1-C，而SP1-A,SP1-B,SP1-C∈∑C2-∑C1，而节点D∈∑C1∩∑C2。这表明节点SP1-B的紧邻前驱节点D是CIM业务流模型中的原子节点，且原子节点D也正好是子过程SP1的紧邻前驱节点，即source(D→SP1)=source(D→SP1-B)。因此CIM业务流模型中的原子节点D与细化PIM工作流模型中的原子节点SP1-B相互交织。同样，CIM业务流模型中的节点C也与细化PIM工作流模型中的原子节点SP1-A相互交织。因此，图3所示的PIM工作流模型是对CIM业务流模型的部分细化。

图3 PIM工作流模型部分细化

2.3 验证步骤

步骤一计算两个模型中相同原子活动的执行顺序对集合∑(SequencePN1|∑C)和∑(SequencePN2|∑C)。如果∑(SequencePN1|∑C)=∑(SequencePN2|∑C)，转向步骤二；否则，表明细化的PIM工作流模型完全改变了CIM业务流模型中业务活动执行顺序，导致业务视图模型与系统视图模型不一致。

步骤二分别计算PN1模型和PN2模型的所有执行顺序对∑(Sequence-pn1|∑C1)和∑(Sequence-pn2|∑C2)。

步骤三计算PN2模型中细化的所有原子活动节点∑C2-∑C1。

步骤四应用2.2节定义的三个条件进行比较分析。

3 语义一致性验证

根据以上四个验证步骤，以网上购物系统为例，分析图4所示的CIM业务流模型与图5所示的细化PIM工作流模型之间的语义一致性问题。可见图5所示的PIM工作流模型是细化了图4中支付服务。因此，设图4为PN1，图5为PN2。

图4 网上购物系统的CIM形式化业务流模型

图5 网上购物系统的PIM形式化工作流模型

第一步：首先计算两个模型的相同节点集合。

∑C=∑C1∩∑C2={搜索商品，接收搜索需求，商品推荐服务，接收商品选项，选择商品，下订单，支付，验证信用卡，确认订单，发送通知}。然后，基于相同节点集合，计算CIM业务流模型和PIM工作流模型执行顺序对集合∑(SequencePN1|∑C)=∑(SequencePN2|∑C)={搜索商品接收搜索需求,接收搜索需求商品推荐服务，商品推荐服务接收商品选项，接收商品选项搜索商品，接收商品选项选择商品，选择商品下订单，下订单支付，确认订单发送通知}。

可以看出∑(SequencePN1|∑C)=∑(SequencePN2|∑C)，表明细化后的PIM工作流模型中，其业务服务活动的执行顺序与CIM业务流模型中的执行顺序保持了一致(顺序流一致)，其消息发送者与消息接收者也保持了一致(消息流一致)。

第二步：计算PN1模型和PN2模型的所有执行顺序对∑(Sequence-pn1|∑C1)和∑(Sequence-pn2|∑C2)。其中：∑(Sequence-pn1|∑C1)={搜索商品接收搜索需求,接收搜索需求商品推荐服务，…，下订单支付，支付支付服务，支付服务验证信用卡，支付服务确认订单，确认订单发送通知}，∑(Sequence-pn2|∑C2)={搜索商品接收搜索需求,接收搜索需求商品推荐服务，…，支付接收支付信息，接收支付信息发送信用卡信息，发送信用卡信息验证信用卡，验证信用卡订单收费，订单收费确认订单，确认订单发送通知}。

第三步：计算PN2模型中细化的所有原子活动节点。

∑C2-∑C1={接收支付信息，发送信用卡信息，订单收费}，∑C2-∑C1集合中的原子活动节点就是PN1模型中子EPN模型支付服务的细化。

第四步：比较分析。∀Seq1,Seq2∈∑Sequence-pn2,∀验证信用卡∈∑C1∩∑C2，∀发送信用卡信息，订单收费∈∑C2-∑C1，∃seq1:发送信用卡信息→验证信用卡，seq2:验证信用卡→订单收费，表明细化后的PIM工作流模型中当且仅当找到一个原子活动“验证信用卡”，该活动同时也存在于CIM业务流模型中。

从以上四个模型验证步骤可知，图5所示的模型的细化操作属于分层细化。细化后的PIM工作流模型与CIM抽象层次上的业务流模型在语义上保持了一致。

4 结 语

针对PIM抽象层次中的工作流模型细化问题，本文利用扩展Petri网模型，首先设计了PIM工作流模型细化的分层独立、分层细化和部分细化的三种不同情形；然后从语义上定义了这三种细化的条件，并设计了这三种不同情形细化的验证步骤；最后应用网上购物系统演示了CIM业务流模型与PIM工作流模型之间的一致性验证过程。实例验证结果表明，本文设计的语义一致性验证方案，可有效地验证PIM抽象层次上的工作流模型在细化和修改的过程中，是否影响了系统的业务流，以及其影响的程度。