李宗花, 周曉峰, 葉正偉, 吳克力

(1.淮陰師范學(xué)院 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院, 江蘇 淮安 223300;2.河海大學(xué) 計(jì)算機(jī)與信息學(xué)院, 江蘇 南京 211100; 3.淮陰師范學(xué)院 城市與環(huán)境學(xué)院, 江蘇 淮安 223300)

?

利用擴(kuò)展的Petri網(wǎng)模型形式化業(yè)務(wù)場(chǎng)景模型

李宗花1, 周曉峰2, 葉正偉3, 吳克力1

(1.淮陰師范學(xué)院 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院, 江蘇 淮安 223300;2.河海大學(xué) 計(jì)算機(jī)與信息學(xué)院, 江蘇 南京 211100; 3.淮陰師范學(xué)院 城市與環(huán)境學(xué)院, 江蘇 淮安 223300)

UCM模型作為一種圖形化的業(yè)務(wù)場(chǎng)景模型,其場(chǎng)景設(shè)計(jì)可以表示需求和產(chǎn)生規(guī)格,驅(qū)動(dòng)設(shè)計(jì)和系統(tǒng)演化,UCM模型的正確性影響軟件開(kāi)發(fā)的質(zhì)量．鑒于形式化模型可以驗(yàn)證其正確性,提出了一種利用擴(kuò)展的Petri網(wǎng)模型,應(yīng)用模型驅(qū)動(dòng)實(shí)現(xiàn)業(yè)務(wù)場(chǎng)景模型的形式化方法．該方法通過(guò)細(xì)化Petri網(wǎng)模型中的Transition結(jié)點(diǎn),從而有效的描述業(yè)務(wù)場(chǎng)景模型中的路徑?jīng)Q策和動(dòng)態(tài)行為．通過(guò)對(duì)UCM模型和擴(kuò)展的Petri網(wǎng)模型的抽象語(yǔ)法定義,利用模型驅(qū)動(dòng)方法定義了UCM模型元素形式化映射為Petri網(wǎng)模型元素的規(guī)則,并根據(jù)其規(guī)則設(shè)計(jì)了映射算法;在Eclipse平臺(tái)上使用ATL語(yǔ)言實(shí)現(xiàn)了模型的形式化映射;應(yīng)用Web Payment實(shí)例演示了UCM模型的形式化分析結(jié)果．

業(yè)務(wù)場(chǎng)景模型; UCM; Petri網(wǎng); 模型形式化

0 引言

業(yè)務(wù)場(chǎng)景模型是一種客戶化交互的模型,體現(xiàn)用戶直接參與、直接交互的一個(gè)過(guò)程[1]．構(gòu)造場(chǎng)景模型使客戶能夠通過(guò)需求求精和模式應(yīng)用來(lái)逐步構(gòu)造業(yè)務(wù)模型,從而更好的集成用戶的需求．UCM(Usecase Map)作為一種表示場(chǎng)景的圖形表示語(yǔ)言由Carleton大學(xué)的Buhr教授帶領(lǐng)的團(tuán)隊(duì)研發(fā),往往應(yīng)用于一些需求易變的軟件系統(tǒng)中．UCM在用例、需求和設(shè)計(jì)之間起到橋梁作用,一方面UCM以清楚的方式連接行為和結(jié)構(gòu),以便為高層次體系結(jié)構(gòu)設(shè)計(jì)提供一個(gè)行為框架．另一方面UCM提供了建模動(dòng)態(tài)系統(tǒng)的場(chǎng)景和結(jié)構(gòu)的功能,其可視化工具使得利益相關(guān)者更容易熟悉和學(xué)習(xí)．因此, D.Amyot等[2-3]對(duì)UCM模型的元模型結(jié)構(gòu)進(jìn)行了設(shè)計(jì)和研究,同時(shí)對(duì)UCM在業(yè)務(wù)建模中的建模過(guò)程和建模方法進(jìn)行了深入的研究．但其UCM的標(biāo)記描述并不包括模型的語(yǔ)義描述,因而其模型的正確性難以驗(yàn)證．同時(shí),目前國(guó)內(nèi)關(guān)于UCM研究主要集中在利用UCM模型進(jìn)行業(yè)務(wù)建模的方法研究[4-8]和利用UCM方法為業(yè)務(wù)系統(tǒng)建立需求模型的應(yīng)用[9-10]．可以看出,當(dāng)前對(duì)UCM模型的形式化研究還很少涉及,因此,本文著重利用形式化語(yǔ)言和工具對(duì)UCM模型形式化,以使得該模型的正確性得到驗(yàn)證．

Petri網(wǎng)作為一個(gè)流類型的形式化模型,比較適合描述系統(tǒng)的行為特征．同時(shí),Petri網(wǎng)目前已經(jīng)被廣泛的應(yīng)用于工作流的形式化[11-12],且建模工具支持模型的自動(dòng)分析和設(shè)計(jì),使得Petri網(wǎng)具有可達(dá)性、死鎖檢測(cè)和邊界分析等優(yōu)點(diǎn)[13-14]．因此,用Petri網(wǎng)來(lái)定義場(chǎng)景流的動(dòng)態(tài)行為是很好的選擇．由于典型的Petri網(wǎng)模型在描述行為路徑選擇上的不足,所以本文擴(kuò)展基本的條件事件網(wǎng)(Condition-Event Net,CEN),使其形式化場(chǎng)景流的動(dòng)態(tài)行為特征和路徑?jīng)Q策特征．

1 業(yè)務(wù)場(chǎng)景模型

1.1 模型標(biāo)記與元模型結(jié)構(gòu)

目前有很多建模軟件支持場(chǎng)景建模,如WebRatio[15],Eclipse jUCMNav[16]插件等,在這些插件上都可以建立UCM模型．UCM模型的圖標(biāo)記描述見(jiàn)表1．可以看出該模型元素包括路徑工具(PathTool)、路徑元素(PathElement)、構(gòu)件(Components)和樁(Stub)等．其中路徑表示場(chǎng)景流,連接起始點(diǎn)、責(zé)任點(diǎn)和終點(diǎn);構(gòu)件是責(zé)任點(diǎn)的邏輯執(zhí)行者,可以代表系統(tǒng)的不同實(shí)體,如組織、伙伴、參與者、軟構(gòu)件等;責(zé)任點(diǎn)表示系統(tǒng)的行為、任務(wù)和需要完成的功能;在一個(gè)組件內(nèi)可以有多個(gè)責(zé)任點(diǎn),表明該責(zé)任被分配至某個(gè)構(gòu)件,需要被該構(gòu)件執(zhí)行;而樁表示暫時(shí)不能確定的行為,在設(shè)計(jì)時(shí)可以設(shè)計(jì)一個(gè)插件(plug,子UCM圖)來(lái)具體化存根;路徑還包括and-fork、and-join、or-fork和or-join等4種決策元素．UCM既是一個(gè)體系結(jié)構(gòu)視圖明確了構(gòu)件之間的責(zé)任分配和協(xié)作關(guān)系,又是面向工作流的,其每一條路徑都定義了一個(gè)業(yè)務(wù)過(guò)程．

表1 UCM模型的圖標(biāo)記

1.2 抽象語(yǔ)法

根據(jù)表1的UCM模型元素內(nèi)容,可以形式化的定義一個(gè)基本UCM模型的抽象語(yǔ)法結(jié)構(gòu)．

定義1 一個(gè)基本的場(chǎng)景模型是一個(gè)7元組:UCM=(name,PT,SE,Co,St,PI,Pa)表示,其中：

1) name是場(chǎng)景的名稱．

2) PT表示為場(chǎng)景模型的PathTool元素,PT=(StartPoint, EmptyPoint, EndPoint),其中StartPoint表示場(chǎng)景的開(kāi)始,EmptyPoint表示場(chǎng)景中的一個(gè)空結(jié)點(diǎn),EndPoint表示場(chǎng)景的結(jié)束．

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

4) Co表示為場(chǎng)景模型的組件,Co=(con,cot). 其中,con表示組件的名稱,表示業(yè)務(wù)系統(tǒng)的參與者;cot表示組件的類型,cot::=Actor|Team|Process|Object|Agent|Other,?j,k:Co?cot(j)==cot(k)?con(j)≠con(k)表示對(duì)于組件類型相同的兩個(gè)組件其組件名稱是唯一的．

5) St表示為樁,St=(sn,sr,sd,si),其中sn表示為樁的名稱,sr定義樁的需求目標(biāo),sd表示樁的一般性描述,si表示樁的內(nèi)部構(gòu)成,其結(jié)構(gòu)與場(chǎng)景模型的結(jié)構(gòu)一致．

6) PI表示為插件,該插件用來(lái)具體化樁的信息,PI=(pin,pig,pir,pid),pin表示插件的名稱,pig表示為插件的操作目標(biāo),pir描述插件的內(nèi)部實(shí)現(xiàn),pid表示插件的一般性描述．

7) Pa表示為路徑元素,代表業(yè)務(wù)場(chǎng)景流,連接起始點(diǎn)、責(zé)任點(diǎn)和終點(diǎn)．因此,Pa=(r,Timer,DirectionArrows,And-fork,Or-fork,And-Join,Or-join)．其中r表示為責(zé)任點(diǎn),往往表示為某個(gè)組件在業(yè)務(wù)系統(tǒng)中的任務(wù),其名稱是唯一的．因此,為了完成某個(gè)業(yè)務(wù)服務(wù)需要多個(gè)責(zé)任點(diǎn)的共同作用．Timer表示計(jì)時(shí)器,DirectionArrow表示場(chǎng)景流流動(dòng)的方向,And-fork表示并行執(zhí)行多個(gè)路徑,Or-fork表示可選擇性的執(zhí)行路徑,And-join表示多個(gè)路徑的與連接．Or-join表示或聯(lián)接,指多個(gè)路徑中的任一條路徑都可以觸發(fā)后續(xù)路徑．因此,一個(gè)業(yè)務(wù)場(chǎng)景模型往往從一個(gè)起始點(diǎn)開(kāi)始,連接多個(gè)責(zé)任點(diǎn)、網(wǎng)關(guān)元素、樁結(jié)點(diǎn)和多個(gè)結(jié)束點(diǎn)且穿過(guò)各個(gè)組件的路徑組成．

2 擴(kuò)展的Petri網(wǎng)模型

基本CEN模型由條件(狀態(tài))、事件(變遷)、從條件到事件和從事件到條件的連接(弧)構(gòu)成[17]．句法上條件表示為環(huán),事件表示為矩形．事件可以有一組前提條件和后置條件,使用標(biāo)符來(lái)標(biāo)記條件．由于在業(yè)務(wù)場(chǎng)景模型中的事件除了表示業(yè)務(wù)系統(tǒng)作用的動(dòng)作行為外,還包括場(chǎng)景路徑的選擇．本文對(duì)基本CEN模型中的事件進(jìn)行了擴(kuò)展．

定義2 一個(gè)擴(kuò)展的條件事件網(wǎng)EPN(Extended Petri Nets)被定義為一個(gè)7-元組組成．

EPN=

其中:PL={pl1,pl2,pl3,…,pln},表示有限個(gè)條件的集合;ST={st1,st2,st3,…,stn},表示有限個(gè)靜態(tài)事件的集合;BT={bt1,bt2,bt3,…,btn},表示有限個(gè)動(dòng)態(tài)事件的集合;?(pl×ST)∪(PL×BT),表示一組輸入弧;OA?(ST×PL)∪(ST×PL),表示一組輸出弧;M0表示初始標(biāo)識(shí);SN=sub,表示子網(wǎng)．

從以上定義的EPN模型形式化語(yǔ)法中可以看出,本文所設(shè)計(jì)的擴(kuò)展條件事件網(wǎng)模型將transition元素細(xì)化為behaviour transition和silent transition．其中silent transition表示靜態(tài)事件,以實(shí)心矩形標(biāo)記表示業(yè)務(wù)場(chǎng)景的開(kāi)始和結(jié)束,以及捕獲業(yè)務(wù)場(chǎng)景流的路徑信息．而behaviour transition表示動(dòng)態(tài)行為事件,以空心矩形標(biāo)記表示業(yè)務(wù)場(chǎng)景模型中的責(zé)任點(diǎn)元素和計(jì)時(shí)器信息．

3 業(yè)務(wù)場(chǎng)景模型的形式化

3.1 業(yè)務(wù)場(chǎng)景流分析

依據(jù)UCM模型的抽象語(yǔ)法,一個(gè)UCM場(chǎng)景模型主要由構(gòu)件和連接各路徑元素的一條路徑組成．每一個(gè)路徑元素都被鏈接在路徑工具上,路徑元素描述業(yè)務(wù)系統(tǒng)的動(dòng)態(tài)行為,包括gateway,responsibility,stub,startpoint,endpoint和timers元素．因此,場(chǎng)景模型有如下流特征:

1) 一個(gè)開(kāi)始點(diǎn)僅僅只有一個(gè)輸出流而沒(méi)有任何的輸入流;

2) 一個(gè)結(jié)束點(diǎn)僅僅只有一個(gè)輸入流而沒(méi)有任何的輸出流;

3) 一個(gè)責(zé)任點(diǎn)元素有且只有一個(gè)輸入流和一個(gè)輸出流;

4) 一個(gè)或分支和與分支網(wǎng)關(guān)只有一個(gè)輸入流和多個(gè)輸出流;

5) 一個(gè)或聯(lián)接和與聯(lián)接網(wǎng)關(guān)具有多個(gè)輸入流和只有一個(gè)輸出流.

3.2 形式化映射規(guī)則

在EPN模型中,由于事件被劃分為靜態(tài)事件和動(dòng)態(tài)事件,故UCM中的相關(guān)網(wǎng)關(guān)元素將被形式化為Petri網(wǎng)模型中的靜態(tài)事件,如“與分支”網(wǎng)關(guān)只有一個(gè)通用的輸入流,其輸出流采用布爾條件來(lái)判斷,因此該判定條件就可以形式化為靜態(tài)事件．表2列出了UCM模型形式化為EPN模型的相關(guān)規(guī)則．

特別指出的是,Stub元素在UCM模型中被看作是一個(gè)子場(chǎng)景模型或者是一個(gè)獨(dú)立的場(chǎng)景模型．雖然一個(gè)Stub元素在UCM模型中可以存在多個(gè)終止結(jié)點(diǎn),但為了保持整個(gè)場(chǎng)景路徑的完整性,表2中所描述的Stub元素在映射時(shí)被強(qiáng)制性的約束為僅有一個(gè)開(kāi)始和結(jié)束且沒(méi)有任何的例外處理．此外,在UCM模型的形式化過(guò)程中,沒(méi)有將Stub元素細(xì)化為staticstub和dynamicstub,這是因?yàn)椴还苁莝tatic stub,還是dynamic stub,當(dāng)映射為EPN模型時(shí)其映射規(guī)則與Stub一致．

3.3 映射算法

從表2的映射規(guī)則可以看出,UCM模型的形式化映射主要包括路徑的映射和路徑元素的映射．根據(jù)表2的規(guī)則設(shè)定, UML模型中的路徑工具的重點(diǎn)元素包括StartPoint和EndPoint元素,這兩個(gè)元素映射為EPN模型的實(shí)現(xiàn)算法如下:

表2 UCM模型元素形式化為EPN模型元素規(guī)則

Input:

Apt=

Output:

Aepn=

if thePTin ucm is not empty then

if asp∈pt.startpoint then//一個(gè)結(jié)點(diǎn)為業(yè)務(wù)場(chǎng)景模型中的開(kāi)始結(jié)點(diǎn)

Create placep1,p2,//創(chuàng)建兩個(gè)place結(jié)點(diǎn)

epn.PL=epn.PL∪{p1,p2}; //將這兩個(gè)place結(jié)點(diǎn)加入PL集合中

Create silent transition st1,//創(chuàng)建一個(gè)silent transition結(jié)點(diǎn)

epn.ST=epn.ST∪{st1}; //將該silent transition結(jié)點(diǎn)加入ST集合中

st1.name←sp.name; //將該開(kāi)始結(jié)點(diǎn)的name和id值賦值給epn模型中開(kāi)始silent transition結(jié)點(diǎn)

st1.id←sp.id;

//創(chuàng)建該silent transition結(jié)點(diǎn)的輸入弧和輸出弧

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

Add an initial token inepn.p1;//為該silent transition結(jié)點(diǎn)加入token標(biāo)識(shí)

end if

for eachepi∈pt.endpointdo//一個(gè)結(jié)點(diǎn)是業(yè)務(wù)場(chǎng)景模型中的結(jié)束結(jié)點(diǎn)

Create silent transitioneti//創(chuàng)建一個(gè)silent transition結(jié)點(diǎn)

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

eti.name←epi.name;//將該結(jié)束點(diǎn)的name和id值賦值給該silent transition結(jié)點(diǎn)

eti.id←epi.id;

Create placepi

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

Add arcsepn.OA=epn.OA∪{(eti,pi)};//創(chuàng)建該silent transition結(jié)點(diǎn)的輸出弧

end for

end if

return;

UCM模型中的路徑元素主要包括responsibility、and-fork、or-fork、and-join以及or-join等元素,這些元素映射為EPN模型的實(shí)現(xiàn)算法如下:

Input:

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

Output:

Aepn=

//將UCM模型中的responsibility結(jié)點(diǎn)映射為EPN模型中的behavior transition結(jié)點(diǎn)

for eachrs∈Pa.rdo//找到一個(gè)responsibility結(jié)點(diǎn)

Create placepi,epn.PL=epn.PL∪{pi};//創(chuàng)建place結(jié)點(diǎn),將該結(jié)點(diǎn)加入PL集合中

//創(chuàng)建behavior transition結(jié)點(diǎn),將該結(jié)點(diǎn)加入BT結(jié)集合中

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

bti.name←rs.name;

bti.id←rs.id;

Add arcs inepn.OA=epn.OA∪{(bti,pi)};//創(chuàng)建該behavior transition結(jié)點(diǎn)的輸出弧

end for

…

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

//假設(shè)se.SE={se1,se2,se3,…}, 構(gòu)造UCM模型中的場(chǎng)景邊結(jié)點(diǎn)

for eachaf∈Pa.And-forkdo

for eachse∈se.SEdo//遍歷每一個(gè)場(chǎng)景邊結(jié)點(diǎn)

ifse.source==afthen//判斷該場(chǎng)景邊的源結(jié)點(diǎn)的類型是否為and-fork

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

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

sti.id←af.id+1; //生成silent transition結(jié)點(diǎn)的id值

Add arcs inepn.IA=epn.IA∪{(af.source,sti)};//創(chuàng)建該silent transition結(jié)點(diǎn)的輸入弧

Add arcs inepn.OA=epn.OA∪{(sti,ipi)};//創(chuàng)建該結(jié)點(diǎn)的輸出弧

end if

end for

end for

//將UCM模型中的or-fork結(jié)點(diǎn)映射至EPN模型

for eachof∈Pa.Or-forkdo

Create silent transitionst1,epn.BT=epn.BT∪{st1};//為每一個(gè)分支創(chuàng)建silent transition結(jié)點(diǎn)

st1.id←of.id+1;

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

for eachse∈se.SEdo

ifse.source==ofthen//判斷該場(chǎng)景邊的源結(jié)點(diǎn)的類型是否為or-fork

Create placep1,epn.PL=epn.PL∪{p1};//創(chuàng)建place結(jié)點(diǎn)

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

end if

end for

end for

…

return

從以上算法中可以看出,模型轉(zhuǎn)換中路徑元素的映射比較復(fù)雜,這是由于Or-Join網(wǎng)關(guān)表示只要聯(lián)接多條路徑中的一條路徑就可觸發(fā)后續(xù)路徑;而And-Join網(wǎng)關(guān)表示聯(lián)接多條路徑后才能觸發(fā)后續(xù)路徑．因此,當(dāng)Join網(wǎng)關(guān)映射為EPN模塊時(shí)表示為靜態(tài)事件,用于捕獲場(chǎng)景的路徑行為;而Or-Fork和And-Fork網(wǎng)關(guān)的執(zhí)行需要判定條件,表示聯(lián)接多條路徑中的一條路徑和聯(lián)接多條路徑中的多條路徑,可以直接映射為EPN模塊中一個(gè)靜態(tài)事件．針對(duì)這些特點(diǎn),Or-Fork網(wǎng)關(guān)建模時(shí)采用布爾條件來(lái)表示后置條件(輸出流),但其輸入流信息相同．因此Or-Fork網(wǎng)關(guān)的前置條件(輸入流)有一個(gè)token,使得我們建模時(shí)不需要單獨(dú)設(shè)置條件本身,只需要當(dāng)某個(gè)后置條件為“真”時(shí)網(wǎng)關(guān)將會(huì)到達(dá)某個(gè)后置條件;而對(duì)于And-Fork網(wǎng)關(guān)來(lái)說(shuō),表示并行執(zhí)行多個(gè)路徑,網(wǎng)關(guān)的每一條路徑都對(duì)應(yīng)一個(gè)事件和事件的后置條件．

3.4 形式化執(zhí)行過(guò)程

圖1顯示了以UCM模型為源模型,以EPN模型為目標(biāo)模型的模型形式化轉(zhuǎn)換過(guò)程．其詳細(xì)轉(zhuǎn)換過(guò)程為:首先利用EMF插件[18]創(chuàng)建UCM模型和EPN模型的元模型;然后利用ATL插件編寫模型轉(zhuǎn)換代碼(根據(jù)模型轉(zhuǎn)換規(guī)則和模型轉(zhuǎn)換算法);最后通過(guò)ATL執(zhí)行引擎執(zhí)行模型轉(zhuǎn)換代碼,從而實(shí)現(xiàn)將UCM模型形式化轉(zhuǎn)換為EPN模型．其形式化模型轉(zhuǎn)換在MOF層次的M2層中實(shí)現(xiàn),即源模型與目標(biāo)模型之間的形式化轉(zhuǎn)換是基于元模型轉(zhuǎn)換技術(shù)的．因此,利用本文設(shè)計(jì)的模型形式化插件可實(shí)現(xiàn)將任意UCM模型形式化為EPN模型．

圖1 UCM模型形式化為EPN模型的過(guò)程 圖2 Web Payment系統(tǒng)的UCM模型

4 實(shí)例演示

本文使用的運(yùn)行實(shí)例來(lái)自于W3C標(biāo)準(zhǔn)文檔[19]中的Web Payment業(yè)務(wù)系統(tǒng),該業(yè)務(wù)系統(tǒng)的場(chǎng)景描述如下:

首先,購(gòu)物者(Customer)瀏覽Online Shopping Site的商品,然后她選擇商品并放入購(gòu)物車;一旦該Customer下訂單購(gòu)買該商品,該用戶需要登錄自己的賬戶,并向Online Shopping Site提供自己的銀行賬戶或其他支付信息(支付寶、谷歌錢包或者蘋果支付等),同時(shí)Online Shopping Site還會(huì)要求用戶提供驗(yàn)證碼等信息;Online Shopping Site提交用戶的支付信息給相應(yīng)的金融機(jī)構(gòu)(Financial Company),Customer和Online Shopping Site都能收到來(lái)自金融機(jī)構(gòu)的支付憑證;最后,Online Shopping Site發(fā)送給Customer數(shù)字憑證,同時(shí)Online Shopping Site的發(fā)貨部門會(huì)將商品發(fā)送給Customer．

根據(jù)以上的業(yè)務(wù)場(chǎng)景描述,應(yīng)用業(yè)務(wù)場(chǎng)景模型建模方法對(duì)該Web Payment業(yè)務(wù)系統(tǒng)進(jìn)行業(yè)務(wù)場(chǎng)景流的分析．圖2顯示了Web Payment業(yè)務(wù)系統(tǒng)的完整場(chǎng)景交互狀態(tài),可以看出該業(yè)務(wù)系統(tǒng)的用戶主要涉及到Customer、Online Shopping Site和Financial Company三類直接用戶．其中Online Shopping Site為Customer用戶提供了搜索服務(wù)(Search service)、支付工具服務(wù)(Payment Instruments service)、支付服務(wù)(Payment service)以及快遞服務(wù)(Delivery service)．因此,Online Shopping Site是服務(wù)的提供者,而Customer是服務(wù)的接收者,Financial Company是服務(wù)的協(xié)作者．

圖2顯示的場(chǎng)景交互狀態(tài)是從Customer的角度出發(fā),模擬了當(dāng)Customer向Online Shopping Site提出自己的購(gòu)物要求后,Online Shopping Site為Customer提供服務(wù)的場(chǎng)景狀態(tài)．值得注意的是,Customer在該場(chǎng)景模型中只與Online Shopping Site產(chǎn)生交互．同時(shí),由于Search service和Payment Instrument service是Online Shopping Site內(nèi)部處理的業(yè)務(wù),因此在業(yè)務(wù)場(chǎng)景中以Stub元素來(lái)表示,而Payment service和Delivery service需要與Customer用戶和Financial Company用戶產(chǎn)生交互,因此這兩個(gè)服務(wù)被進(jìn)一步細(xì)化為責(zé)任點(diǎn)元素．

根據(jù)場(chǎng)景模型的形式化定義,執(zhí)行UCM2ExtendPetrinets模型形式化插件,圖3顯示了使用EPN模型形式化UCM模型的結(jié)果．該形式化模型采用Petri網(wǎng)的死鎖和活性分析技術(shù),可以證明該UCM模型是正確的．以死鎖分析為例,從帶有標(biāo)符的place開(kāi)始,執(zhí)行page start靜態(tài)事件表明Petri網(wǎng)模型開(kāi)始執(zhí)行. 根據(jù)Arc遍歷圖中的每一個(gè)動(dòng)態(tài)行為(behaviour transition)事件,可以得到多條活動(dòng)路徑順序．

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

通過(guò)遍歷發(fā)現(xiàn),圖3中存在2條路徑就可以遍歷所有Petri網(wǎng)模型結(jié)點(diǎn),且每一條路徑都有其結(jié)束點(diǎn)．

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

通過(guò)對(duì)圖3實(shí)施ePNK語(yǔ)法檢查和從語(yǔ)義上的執(zhí)行路徑順序分析,表明該UCM模型描述的業(yè)務(wù)場(chǎng)景模型是正確的．當(dāng)然,UCM形式化模型也會(huì)出現(xiàn)ePNK語(yǔ)法檢查不通過(guò)的情形(如沒(méi)有開(kāi)始事件或結(jié)束事件等),或語(yǔ)義檢查不通過(guò)的情形(如存在閉環(huán)或死鎖的問(wèn)題),這兩種情形表明該UCM模型是不完整或不正確的．由此可見(jiàn),利用Petri nets模型對(duì)UCM模型進(jìn)行形式化可以確保系統(tǒng)業(yè)務(wù)模型的正確性,從而更好的指導(dǎo)軟件的設(shè)計(jì)與開(kāi)發(fā)．

5 結(jié)束語(yǔ)

針對(duì)現(xiàn)有的業(yè)務(wù)場(chǎng)景模型研究中沒(méi)有解決其模型的正確性驗(yàn)證問(wèn)題,提出了利用擴(kuò)展的Petri nets模型形式化UCM模型的方法．該方法利用元模型轉(zhuǎn)換技術(shù)制定了UCM模型形式化映射為擴(kuò)展Petri nets模型的映射規(guī)則和映射算法,并利用ATL語(yǔ)言描述該映射規(guī)則和映射算法,同時(shí)利用ATL執(zhí)行引擎在Eclipse平臺(tái)上實(shí)現(xiàn)UCM模型的形式化執(zhí)行．

通過(guò)實(shí)例演示,擴(kuò)展Petri網(wǎng)模型中的silent transition元素能夠完整的描述業(yè)務(wù)場(chǎng)景模型的開(kāi)始與結(jié)束,以及場(chǎng)景路徑的選擇;而behaviour transition元素能夠刻畫業(yè)務(wù)場(chǎng)景模型中的動(dòng)態(tài)行為．利用ePNK插件的語(yǔ)法檢查和Petri nets語(yǔ)義插件能夠驗(yàn)證UCM模型的正確性,因而該形式化方法具有確定性的優(yōu)勢(shì)．在后續(xù)的工作中,還需要進(jìn)一步降低限制性約束,使得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].計(jì)算機(jī)應(yīng)用與軟件,2009,26(7):140-142.

[5] 何頻捷,吳岳忠,文志華,等.場(chǎng)景驅(qū)動(dòng)的業(yè)務(wù)過(guò)程模型設(shè)計(jì)方法[J].計(jì)算機(jī)工程與應(yīng)用,2007,43(26):242-244.

[6] 況振宇,魏長(zhǎng)江,王曉麗.基于UML活動(dòng)圖的UCM建模[J].青島大學(xué)學(xué)報(bào)：自然科學(xué)版,2013,26(3):49-54.

[7] 袁萍萍,蔣霞,杜玉越.一種基于場(chǎng)景的需求驅(qū)動(dòng)構(gòu)件服務(wù)聚集方法[J].計(jì)算機(jī)應(yīng)用研究,2011,28(12):4607-4612.

[8] 李長(zhǎng)云,陽(yáng)愛(ài)民,滿君豐,等.一種面向按需集成服務(wù)的業(yè)務(wù)模型構(gòu)造方法[J]. 2006,29(7):1095-1104.

[9] 陳廷偉,楊艷輝,關(guān)長(zhǎng)城.基于UCM的領(lǐng)域SOA資產(chǎn)庫(kù)構(gòu)建方法[J]. 計(jì)算機(jī)工程,2011,37(2):48-51.

[10] 路超,周磊山.基于場(chǎng)景驅(qū)動(dòng)的高鐵應(yīng)急預(yù)案流程控制方法[J].交通運(yùn)輸系統(tǒng)工程與信息,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/>.

[責(zé)任編輯：蔣海龍]

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

國(guó)家自然科學(xué)基金資助項(xiàng)目(41471425); 江蘇省高校哲學(xué)社會(huì)科學(xué)基金資助項(xiàng)目(2016SJB630122); 淮安市科技支撐計(jì)劃項(xiàng)目(HAS2015005-1)

李宗花(1981-),女,重慶豐都人，講師,博士,主要研究方向?yàn)樾问交椒ê湍Ｐ万?qū)動(dòng)開(kāi)發(fā). E-mail: leeleaf@163.com

TP311.52

A

1671-6876(2016)04-0309-08