利用扩展的Petri网模型形式化业务场景模型

李宗花, 周晓峰, 叶正伟, 吴克力

(1.淮阴师范学院 计算机科学与技术学院, 江苏 淮安 223300;2.河海大学 计算机与信息学院, 江苏 南京 211100; 3.淮阴师范学院 城市与环境学院, 江苏 淮安 223300)



利用扩展的Petri网模型形式化业务场景模型

李宗花1, 周晓峰2, 叶正伟3, 吴克力1

(1.淮阴师范学院 计算机科学与技术学院, 江苏 淮安 223300;2.河海大学 计算机与信息学院, 江苏 南京 211100; 3.淮阴师范学院 城市与环境学院, 江苏 淮安 223300)

UCM模型作为一种图形化的业务场景模型,其场景设计可以表示需求和产生规格,驱动设计和系统演化,UCM模型的正确性影响软件开发的质量．鉴于形式化模型可以验证其正确性,提出了一种利用扩展的Petri网模型,应用模型驱动实现业务场景模型的形式化方法．该方法通过细化Petri网模型中的Transition结点,从而有效的描述业务场景模型中的路径决策和动态行为．通过对UCM模型和扩展的Petri网模型的抽象语法定义,利用模型驱动方法定义了UCM模型元素形式化映射为Petri网模型元素的规则,并根据其规则设计了映射算法;在Eclipse平台上使用ATL语言实现了模型的形式化映射;应用Web Payment实例演示了UCM模型的形式化分析结果．

业务场景模型; UCM; Petri网; 模型形式化

0 引言

业务场景模型是一种客户化交互的模型,体现用户直接参与、直接交互的一个过程[1]．构造场景模型使客户能够通过需求求精和模式应用来逐步构造业务模型,从而更好的集成用户的需求．UCM(Usecase Map)作为一种表示场景的图形表示语言由Carleton大学的Buhr教授带领的团队研发,往往应用于一些需求易变的软件系统中．UCM在用例、需求和设计之间起到桥梁作用,一方面UCM以清楚的方式连接行为和结构,以便为高层次体系结构设计提供一个行为框架．另一方面UCM提供了建模动态系统的场景和结构的功能,其可视化工具使得利益相关者更容易熟悉和学习．因此, D.Amyot等[2-3]对UCM模型的元模型结构进行了设计和研究,同时对UCM在业务建模中的建模过程和建模方法进行了深入的研究．但其UCM的标记描述并不包括模型的语义描述,因而其模型的正确性难以验证．同时,目前国内关于UCM研究主要集中在利用UCM模型进行业务建模的方法研究[4-8]和利用UCM方法为业务系统建立需求模型的应用[9-10]．可以看出,当前对UCM模型的形式化研究还很少涉及,因此,本文着重利用形式化语言和工具对UCM模型形式化,以使得该模型的正确性得到验证．

Petri网作为一个流类型的形式化模型,比较适合描述系统的行为特征．同时,Petri网目前已经被广泛的应用于工作流的形式化[11-12],且建模工具支持模型的自动分析和设计,使得Petri网具有可达性、死锁检测和边界分析等优点[13-14]．因此,用Petri网来定义场景流的动态行为是很好的选择．由于典型的Petri网模型在描述行为路径选择上的不足,所以本文扩展基本的条件事件网(Condition-Event Net,CEN),使其形式化场景流的动态行为特征和路径决策特征．

1 业务场景模型

1.1 模型标记与元模型结构

目前有很多建模软件支持场景建模,如WebRatio[15],Eclipse jUCMNav[16]插件等,在这些插件上都可以建立UCM模型．UCM模型的图标记描述见表1．可以看出该模型元素包括路径工具(PathTool)、路径元素(PathElement)、构件(Components)和桩(Stub)等．其中路径表示场景流,连接起始点、责任点和终点;构件是责任点的逻辑执行者,可以代表系统的不同实体,如组织、伙伴、参与者、软构件等;责任点表示系统的行为、任务和需要完成的功能;在一个组件内可以有多个责任点,表明该责任被分配至某个构件,需要被该构件执行;而桩表示暂时不能确定的行为,在设计时可以设计一个插件(plug,子UCM图)来具体化存根;路径还包括and-fork、and-join、or-fork和or-join等4种决策元素．UCM既是一个体系结构视图明确了构件之间的责任分配和协作关系,又是面向工作流的,其每一条路径都定义了一个业务过程．

表1 UCM模型的图标记

1.2 抽象语法

根据表1的UCM模型元素内容,可以形式化的定义一个基本UCM模型的抽象语法结构．

定义1 一个基本的场景模型是一个7元组:UCM=(name,PT,SE,Co,St,PI,Pa)表示,其中：

1) name是场景的名称．

2) PT表示为场景模型的PathTool元素,PT=(StartPoint, EmptyPoint, EndPoint),其中StartPoint表示场景的开始,EmptyPoint表示场景中的一个空结点,EndPoint表示场景的结束．

3) SE表示场景模型中ScenariosEdge元素的集合,SE={se1,se2,se3,se4,…}．

4) Co表示为场景模型的组件,Co=(con,cot). 其中,con表示组件的名称,表示业务系统的参与者;cot表示组件的类型,cot::=Actor|Team|Process|Object|Agent|Other,∀j,k:Co∃cot(j)==cot(k)⟹con(j)≠con(k)表示对于组件类型相同的两个组件其组件名称是唯一的．

5) St表示为桩,St=(sn,sr,sd,si),其中sn表示为桩的名称,sr定义桩的需求目标,sd表示桩的一般性描述,si表示桩的内部构成,其结构与场景模型的结构一致．

6) PI表示为插件,该插件用来具体化桩的信息,PI=(pin,pig,pir,pid),pin表示插件的名称,pig表示为插件的操作目标,pir描述插件的内部实现,pid表示插件的一般性描述．

7) Pa表示为路径元素,代表业务场景流,连接起始点、责任点和终点．因此,Pa=(r,Timer,DirectionArrows,And-fork,Or-fork,And-Join,Or-join)．其中r表示为责任点,往往表示为某个组件在业务系统中的任务,其名称是唯一的．因此,为了完成某个业务服务需要多个责任点的共同作用．Timer表示计时器,DirectionArrow表示场景流流动的方向,And-fork表示并行执行多个路径,Or-fork表示可选择性的执行路径,And-join表示多个路径的与连接．Or-join表示或联接,指多个路径中的任一条路径都可以触发后续路径．因此,一个业务场景模型往往从一个起始点开始,连接多个责任点、网关元素、桩结点和多个结束点且穿过各个组件的路径组成．

2 扩展的Petri网模型

基本CEN模型由条件(状态)、事件(变迁)、从条件到事件和从事件到条件的连接(弧)构成[17]．句法上条件表示为环,事件表示为矩形．事件可以有一组前提条件和后置条件,使用标符来标记条件．由于在业务场景模型中的事件除了表示业务系统作用的动作行为外,还包括场景路径的选择．本文对基本CEN模型中的事件进行了扩展．

定义2 一个扩展的条件事件网EPN(Extended Petri Nets)被定义为一个7-元组组成．

EPN=

其中:PL={pl1,pl2,pl3,…,pln},表示有限个条件的集合;ST={st1,st2,st3,…,stn},表示有限个静态事件的集合;BT={bt1,bt2,bt3,…,btn},表示有限个动态事件的集合;⊆(pl×ST)∪(PL×BT),表示一组输入弧;OA⊆(ST×PL)∪(ST×PL),表示一组输出弧;M0表示初始标识;SN=sub,表示子网．

从以上定义的EPN模型形式化语法中可以看出,本文所设计的扩展条件事件网模型将transition元素细化为behaviour transition和silent transition．其中silent transition表示静态事件,以实心矩形标记表示业务场景的开始和结束,以及捕获业务场景流的路径信息．而behaviour transition表示动态行为事件,以空心矩形标记表示业务场景模型中的责任点元素和计时器信息．

3 业务场景模型的形式化

3.1 业务场景流分析

依据UCM模型的抽象语法,一个UCM场景模型主要由构件和连接各路径元素的一条路径组成．每一个路径元素都被链接在路径工具上,路径元素描述业务系统的动态行为,包括gateway,responsibility,stub,startpoint,endpoint和timers元素．因此,场景模型有如下流特征:

1) 一个开始点仅仅只有一个输出流而没有任何的输入流;

2) 一个结束点仅仅只有一个输入流而没有任何的输出流;

3) 一个责任点元素有且只有一个输入流和一个输出流;

4) 一个或分支和与分支网关只有一个输入流和多个输出流;

5) 一个或联接和与联接网关具有多个输入流和只有一个输出流.

3.2 形式化映射规则

在EPN模型中,由于事件被划分为静态事件和动态事件,故UCM中的相关网关元素将被形式化为Petri网模型中的静态事件,如“与分支”网关只有一个通用的输入流,其输出流采用布尔条件来判断,因此该判定条件就可以形式化为静态事件．表2列出了UCM模型形式化为EPN模型的相关规则．

特别指出的是,Stub元素在UCM模型中被看作是一个子场景模型或者是一个独立的场景模型．虽然一个Stub元素在UCM模型中可以存在多个终止结点,但为了保持整个场景路径的完整性,表2中所描述的Stub元素在映射时被强制性的约束为仅有一个开始和结束且没有任何的例外处理．此外,在UCM模型的形式化过程中,没有将Stub元素细化为staticstub和dynamicstub,这是因为不管是static stub,还是dynamic stub,当映射为EPN模型时其映射规则与Stub一致．

3.3 映射算法

从表2的映射规则可以看出,UCM模型的形式化映射主要包括路径的映射和路径元素的映射．根据表2的规则设定, UML模型中的路径工具的重点元素包括StartPoint和EndPoint元素,这两个元素映射为EPN模型的实现算法如下:

表2 UCM模型元素形式化为EPN模型元素规则

Input:

Apt=

Output:

Aepn=

if thePTin ucm is not empty then

if asp∈pt.startpoint then//一个结点为业务场景模型中的开始结点

Create placep1,p2,//创建两个place结点

epn.PL=epn.PL∪{p1,p2}; //将这两个place结点加入PL集合中

Create silent transition st1,//创建一个silent transition结点

epn.ST=epn.ST∪{st1}; //将该silent transition结点加入ST集合中

st1.name←sp.name; //将该开始结点的name和id值赋值给epn模型中开始silent transition结点

st1.id←sp.id;

//创建该silent transition结点的输入弧和输出弧

Add arcsepn.IA=epn.IA∪{(p1,st1)} andepn.OA=epn.OA∪{(st1,p2)};

Add an initial token inepn.p1;//为该silent transition结点加入token标识

end if

for eachepi∈pt.endpointdo//一个结点是业务场景模型中的结束结点

Create silent transitioneti//创建一个silent transition结点

epn.ST=epn.ST∪{eti};

eti.name←epi.name;//将该结束点的name和id值赋值给该silent transition结点

eti.id←epi.id;

Create placepi

epn.PL=epn.PL∪{pi};

Add arcsepn.OA=epn.OA∪{(eti,pi)};//创建该silent transition结点的输出弧

end for

end if

return;

UCM模型中的路径元素主要包括responsibility、and-fork、or-fork、and-join以及or-join等元素,这些元素映射为EPN模型的实现算法如下:

Input:

APa=(r,Timer,DirectionArrows,And-fork,Or-fork,And-Join,Or-join)

Output:

Aepn=

//将UCM模型中的responsibility结点映射为EPN模型中的behavior transition结点

for eachrs∈Pa.rdo//找到一个responsibility结点

Create placepi,epn.PL=epn.PL∪{pi};//创建place结点,将该结点加入PL集合中

//创建behavior transition结点,将该结点加入BT结集合中

Create behavior transitionbti,epn.BT=epn.BT∪{bti};

bti.name←rs.name;

bti.id←rs.id;

Add arcs inepn.OA=epn.OA∪{(bti,pi)};//创建该behavior transition结点的输出弧

end for

…

//将UCM模型中的and-fork元素映射至EPN模型

//假设se.SE={se1,se2,se3,…}, 构造UCM模型中的场景边结点

for eachaf∈Pa.And-forkdo

for eachse∈se.SEdo//遍历每一个场景边结点

ifse.source==afthen//判断该场景边的源结点的类型是否为and-fork

Create placepi,epn.PL=epn.PL∪{pi};

Create silent transitionsti,epn.BT=epn.BT∪{sti};

sti.id←af.id+1; //生成silent transition结点的id值

Add arcs inepn.IA=epn.IA∪{(af.source,sti)};//创建该silent transition结点的输入弧

Add arcs inepn.OA=epn.OA∪{(sti,ipi)};//创建该结点的输出弧

end if

end for

end for

//将UCM模型中的or-fork结点映射至EPN模型

for eachof∈Pa.Or-forkdo

Create silent transitionst1,epn.BT=epn.BT∪{st1};//为每一个分支创建silent transition结点

st1.id←of.id+1;

Add arcs inepn.IA=epn.IA∪{(of.source,st1)};

for eachse∈se.SEdo

ifse.source==ofthen//判断该场景边的源结点的类型是否为or-fork

Create placep1,epn.PL=epn.PL∪{p1};//创建place结点

Add arcs inepn.OA=epn.OA∪{(of,p1)};

end if

end for

end for

…

return

从以上算法中可以看出,模型转换中路径元素的映射比较复杂,这是由于Or-Join网关表示只要联接多条路径中的一条路径就可触发后续路径;而And-Join网关表示联接多条路径后才能触发后续路径．因此,当Join网关映射为EPN模块时表示为静态事件,用于捕获场景的路径行为;而Or-Fork和And-Fork网关的执行需要判定条件,表示联接多条路径中的一条路径和联接多条路径中的多条路径,可以直接映射为EPN模块中一个静态事件．针对这些特点,Or-Fork网关建模时采用布尔条件来表示后置条件(输出流),但其输入流信息相同．因此Or-Fork网关的前置条件(输入流)有一个token,使得我们建模时不需要单独设置条件本身,只需要当某个后置条件为“真”时网关将会到达某个后置条件;而对于And-Fork网关来说,表示并行执行多个路径,网关的每一条路径都对应一个事件和事件的后置条件．

3.4 形式化执行过程

图1显示了以UCM模型为源模型,以EPN模型为目标模型的模型形式化转换过程．其详细转换过程为:首先利用EMF插件[18]创建UCM模型和EPN模型的元模型;然后利用ATL插件编写模型转换代码(根据模型转换规则和模型转换算法);最后通过ATL执行引擎执行模型转换代码,从而实现将UCM模型形式化转换为EPN模型．其形式化模型转换在MOF层次的M2层中实现,即源模型与目标模型之间的形式化转换是基于元模型转换技术的．因此,利用本文设计的模型形式化插件可实现将任意UCM模型形式化为EPN模型．

图1 UCM模型形式化为EPN模型的过程 图2 Web Payment系统的UCM模型

4 实例演示

本文使用的运行实例来自于W3C标准文档[19]中的Web Payment业务系统,该业务系统的场景描述如下:

首先,购物者(Customer)浏览Online Shopping Site的商品,然后她选择商品并放入购物车;一旦该Customer下订单购买该商品,该用户需要登录自己的账户,并向Online Shopping Site提供自己的银行账户或其他支付信息(支付宝、谷歌钱包或者苹果支付等),同时Online Shopping Site还会要求用户提供验证码等信息;Online Shopping Site提交用户的支付信息给相应的金融机构(Financial Company),Customer和Online Shopping Site都能收到来自金融机构的支付凭证;最后,Online Shopping Site发送给Customer数字凭证,同时Online Shopping Site的发货部门会将商品发送给Customer．

根据以上的业务场景描述,应用业务场景模型建模方法对该Web Payment业务系统进行业务场景流的分析．图2显示了Web Payment业务系统的完整场景交互状态,可以看出该业务系统的用户主要涉及到Customer、Online Shopping Site和Financial Company三类直接用户．其中Online Shopping Site为Customer用户提供了搜索服务(Search service)、支付工具服务(Payment Instruments service)、支付服务(Payment service)以及快递服务(Delivery service)．因此,Online Shopping Site是服务的提供者,而Customer是服务的接收者,Financial Company是服务的协作者．

图2显示的场景交互状态是从Customer的角度出发,模拟了当Customer向Online Shopping Site提出自己的购物要求后,Online Shopping Site为Customer提供服务的场景状态．值得注意的是,Customer在该场景模型中只与Online Shopping Site产生交互．同时,由于Search service和Payment Instrument service是Online Shopping Site内部处理的业务,因此在业务场景中以Stub元素来表示,而Payment service和Delivery service需要与Customer用户和Financial Company用户产生交互,因此这两个服务被进一步细化为责任点元素．

根据场景模型的形式化定义,执行UCM2ExtendPetrinets模型形式化插件,图3显示了使用EPN模型形式化UCM模型的结果．该形式化模型采用Petri网的死锁和活性分析技术,可以证明该UCM模型是正确的．以死锁分析为例,从带有标符的place开始,执行page start静态事件表明Petri网模型开始执行. 根据Arc遍历图中的每一个动态行为(behaviour transition)事件,可以得到多条活动路径顺序．

图3 形式化UCM模型的EPN模型

通过遍历发现,图3中存在2条路径就可以遍历所有Petri网模型结点,且每一条路径都有其结束点．

P1=page start→Search Items→Receive Search Requirement→Search service→Receive Options→Select Goods→Payment Instruments service→Select Payment Instrument→Input Authentication Code→Initiates Payment Authorization→Receive Payment Authorization→Verify Available Funds→Authorize Transfer→Finalize Payment→Receive Payment Proof→page end.

P2=page start→Search Items→Receive Search Requirement→Search service→Receive Options→Select Goods→Payment Instruments service→Select Payment Instrument→Input Authentication Code→Initiates Payment Authorization→Receive Payment Authorization→Verify Available Funds→Authorize Transfer→Finalize Payment→Complete Transfer→Send Digital Receipt→Receive Digital Receipt→Delivery Goods→page end

通过对图3实施ePNK语法检查和从语义上的执行路径顺序分析,表明该UCM模型描述的业务场景模型是正确的．当然,UCM形式化模型也会出现ePNK语法检查不通过的情形(如没有开始事件或结束事件等),或语义检查不通过的情形(如存在闭环或死锁的问题),这两种情形表明该UCM模型是不完整或不正确的．由此可见,利用Petri nets模型对UCM模型进行形式化可以确保系统业务模型的正确性,从而更好的指导软件的设计与开发．

5 结束语

针对现有的业务场景模型研究中没有解决其模型的正确性验证问题,提出了利用扩展的Petri nets模型形式化UCM模型的方法．该方法利用元模型转换技术制定了UCM模型形式化映射为扩展Petri nets模型的映射规则和映射算法,并利用ATL语言描述该映射规则和映射算法,同时利用ATL执行引擎在Eclipse平台上实现UCM模型的形式化执行．

通过实例演示,扩展Petri网模型中的silent transition元素能够完整的描述业务场景模型的开始与结束,以及场景路径的选择;而behaviour transition元素能够刻画业务场景模型中的动态行为．利用ePNK插件的语法检查和Petri nets语义插件能够验证UCM模型的正确性,因而该形式化方法具有确定性的优势．在后续的工作中,还需要进一步降低限制性约束,使得UCM模型的形式化精度更高．

[1] Alix T, Zacharewicz G. Product-service systems scenarios simulation based on G-DEVS/HLA: generalized discrete event specification/high level architecture[J]. Comput Ind, 2012,63 (4): 370-378.

[2] Amyot D. URN Metamodel Version 0.27[EB/OL]. 2012 .

[3] Amyot D, He X Y, He Y,et al. Generating scenarios from use case map specifications[C]. Dallas: Proceedings of the Third International Conference on Quality Software, USA, 2003:108-115.

[4] 李胜勇,饶德虎,艾小川,等.IDEF0/UCM-集成的需求分析建模方法[J].计算机应用与软件,2009,26(7):140-142.

[5] 何频捷,吴岳忠,文志华,等.场景驱动的业务过程模型设计方法[J].计算机工程与应用,2007,43(26):242-244.

[6] 况振宇,魏长江,王晓丽.基于UML活动图的UCM建模[J].青岛大学学报：自然科学版,2013,26(3):49-54.

[7] 袁萍萍,蒋霞,杜玉越.一种基于场景的需求驱动构件服务聚集方法[J].计算机应用研究,2011,28(12):4607-4612.

[8] 李长云,阳爱民,满君丰,等.一种面向按需集成服务的业务模型构造方法[J]. 2006,29(7):1095-1104.

[9] 陈廷伟,杨艳辉,关长城.基于UCM的领域SOA资产库构建方法[J]. 计算机工程,2011,37(2):48-51.

[10] 路超,周磊山.基于场景驱动的高铁应急预案流程控制方法[J].交通运输系统工程与信息,2012,12(4):161-166.

[11] Wong P Y H,Gibbons J. Formalisations and applications of BPMN[J]. Science of Computer Programming, 2011, 76(8): 633-650.

[12] Dijkman R M, Dumas M, Ouyang C. Semantics and analysis of business process models in BPMN[J]. Information and Software Technology, 2008,50(12): 1281-1294.

[13] Kostin A E. Reachability analysis in T-invariant-less Petri Nets[J]. IEEE Transactions on Automatic Control, 2003,48(6): 1019-1024.

[14] Yoo T, Jeong B, Cho H. A Petri nets based functional validation for services composition[J]. Expert Systems with Applications,2010,37:3768-3776.

[15] Brambilla M,Fraternali P. Large-scale Model-Driven Engineering of web user interaction: The WebML and WebRatio experience[J]. Science of Computer Programming,2014,89:71-87.

[16] Mussbacher G, Ghanavati S,Amyot D. Modeling and Analysis of URN Goals and Scenarios with jUCMNav[C]. Dallas: Proceeding of Requirements Engineering Conference, 2009:383-384.

[17] Ye Y, Jiang Z B, Diao X D, et al. Extended event-condition-action rules and fuzzy Petri nets based exception handling for workflow management[J]. Expert Systems with Applications, 2011, 38(9): 10847-10861.

[18] Steinberg D, Budinsky F,Paternostro M, et al. Eclipse Modeling Framework[M]. 2nd. Dallas: Addison-Wesley Professional, 2008.

[19] W3C, Web Payments Use Cases 1.0[EB/OL]. 2015. < https://www.w3.org/TR/web-payments-use-cases/>.

[责任编辑：蒋海龙]

Using Extended Petri Nets Model to Formalize the Business Scenario Model

LI Zong-hua1, ZHOU Xiao-feng2, YE Zheng-wei3, WU Ke-li1

(1.School of Computer Science and Technology, Huaiyin Normal University, Huaian Jiangsu 223300, China)(2.College of Computer and Information Engineering, Hohai University, Nanjing Jiangsu 211100, China)(3.School of Urban and Environment Sciences, Huaiyin Normal University, Huaian Jiangsu 223300, China)

The UCM (Usecase Map) model as a graphical scenario model focuses on the interaction between custom and business system. It graphical scene not only can represent the requirements and specifications, but also can drive the design and evolution of the business system. So, the correctness of the UCM model is a key to influencing the software development. In view of the formal model can verify the model correctness. In this paper proposes a formalization approach, which extends the Petri nets model, and applies model driven technology to carry out the UCM model formalization. This approach can effectively describe the path decision and dynamic behavior of the business scenario model via refining transition element of the Petri nets model. Firstly, the abstract syntax of the UCM model and Petri nets model are defined, and the formal mapping rules between UCM model elements and Petri nets model elements are designed on account of the model driven technology. Then, the mapping algorithms are designed according to mapping rules, and the mapping algorithms are carried out by Eclipse framework by using ATL language. Finally, the Web Payment system is applied to illustrate the executing result of the formalization.

business scenario model; UCM; Petri nets; model formalization

2016-07-04

国家自然科学基金资助项目(41471425); 江苏省高校哲学社会科学基金资助项目(2016SJB630122); 淮安市科技支撑计划项目(HAS2015005-1)

李宗花(1981-),女,重庆丰都人，讲师,博士,主要研究方向为形式化方法和模型驱动开发. E-mail: leeleaf@163.com

TP311.52

A

1671-6876(2016)04-0309-08