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

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

?

利用擴展的Petri網模型形式化業(yè)務場景模型

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

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

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

業(yè)務場景模型; UCM; Petri網; 模型形式化

0 引言

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

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

1 業(yè)務場景模型

1.1 模型標記與元模型結構

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

表1 UCM模型的圖標記

1.2 抽象語法

根據(jù)表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表示組件的名稱,表示業(yè)務系統(tǒng)的參與者;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描述插件的內部實現(xiàn),pid表示插件的一般性描述．

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

2 擴展的Petri網模型

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

定義2 一個擴展的條件事件網EPN(Extended Petri Nets)被定義為一個7-元組組成．

EPN=

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

從以上定義的EPN模型形式化語法中可以看出,本文所設計的擴展條件事件網模型將transition元素細化為behaviour transition和silent transition．其中silent transition表示靜態(tài)事件,以實心矩形標記表示業(yè)務場景的開始和結束,以及捕獲業(yè)務場景流的路徑信息．而behaviour transition表示動態(tài)行為事件,以空心矩形標記表示業(yè)務場景模型中的責任點元素和計時器信息．

3 業(yè)務場景模型的形式化

3.1 業(yè)務場景流分析

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

1) 一個開始點僅僅只有一個輸出流而沒有任何的輸入流;

2) 一個結束點僅僅只有一個輸入流而沒有任何的輸出流;

3) 一個責任點元素有且只有一個輸入流和一個輸出流;

4) 一個或分支和與分支網關只有一個輸入流和多個輸出流;

5) 一個或聯(lián)接和與聯(lián)接網關具有多個輸入流和只有一個輸出流.

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

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

特別指出的是,Stub元素在UCM模型中被看作是一個子場景模型或者是一個獨立的場景模型．雖然一個Stub元素在UCM模型中可以存在多個終止結點,但為了保持整個場景路徑的完整性,表2中所描述的Stub元素在映射時被強制性的約束為僅有一個開始和結束且沒有任何的例外處理．此外,在UCM模型的形式化過程中,沒有將Stub元素細化為staticstub和dynamicstub,這是因為不管是static stub,還是dynamic stub,當映射為EPN模型時其映射規(guī)則與Stub一致．

3.3 映射算法

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

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

Input:

Apt=

Output:

Aepn=

if thePTin ucm is not empty then

if asp∈pt.startpoint then//一個結點為業(yè)務場景模型中的開始結點

Create placep1,p2,//創(chuàng)建兩個place結點

epn.PL=epn.PL∪{p1,p2}; //將這兩個place結點加入PL集合中

Create silent transition st1,//創(chuàng)建一個silent transition結點

epn.ST=epn.ST∪{st1}; //將該silent transition結點加入ST集合中

st1.name←sp.name; //將該開始結點的name和id值賦值給epn模型中開始silent transition結點

st1.id←sp.id;

//創(chuàng)建該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//一個結點是業(yè)務場景模型中的結束結點

Create silent transitioneti//創(chuàng)建一個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)};//創(chuàng)建該silent transition結點的輸出弧

end for

end if

return;

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

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};//創(chuàng)建place結點,將該結點加入PL集合中

//創(chuàng)建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)};//創(chuàng)建該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)};//創(chuàng)建該silent transition結點的輸入弧

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

end if

end for

end for

//將UCM模型中的or-fork結點映射至EPN模型

for eachof∈Pa.Or-forkdo

Create silent transitionst1,epn.BT=epn.BT∪{st1};//為每一個分支創(chuàng)建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};//創(chuàng)建place結點

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

end if

end for

end for

…

return

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

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

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

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

4 實例演示

本文使用的運行實例來自于W3C標準文檔[19]中的Web Payment業(yè)務系統(tǒng),該業(yè)務系統(tǒng)的場景描述如下:

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

根據(jù)以上的業(yè)務場景描述,應用業(yè)務場景模型建模方法對該Web Payment業(yè)務系統(tǒng)進行業(yè)務場景流的分析．圖2顯示了Web Payment業(yè)務系統(tǒng)的完整場景交互狀態(tài),可以看出該業(yè)務系統(tǒng)的用戶主要涉及到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是服務的協(xié)作者．

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

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

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

通過遍歷發(fā)現(xiàn),圖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語法檢查和從語義上的執(zhí)行路徑順序分析,表明該UCM模型描述的業(yè)務場景模型是正確的．當然,UCM形式化模型也會出現(xiàn)ePNK語法檢查不通過的情形(如沒有開始事件或結束事件等),或語義檢查不通過的情形(如存在閉環(huán)或死鎖的問題),這兩種情形表明該UCM模型是不完整或不正確的．由此可見,利用Petri nets模型對UCM模型進行形式化可以確保系統(tǒng)業(yè)務模型的正確性,從而更好的指導軟件的設計與開發(fā)．

5 結束語

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

通過實例演示,擴展Petri網模型中的silent transition元素能夠完整的描述業(yè)務場景模型的開始與結束,以及場景路徑的選擇;而behaviour transition元素能夠刻畫業(yè)務場景模型中的動態(tài)行為．利用ePNK插件的語法檢查和Petri nets語義插件能夠驗證UCM模型的正確性,因而該形式化方法具有確定性的優(yōu)勢．在后續(xù)的工作中,還需要進一步降低限制性約束,使得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] 何頻捷,吳岳忠,文志華,等.場景驅動的業(yè)務過程模型設計方法[J].計算機工程與應用,2007,43(26):242-244.

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

[7] 袁萍萍,蔣霞,杜玉越.一種基于場景的需求驅動構件服務聚集方法[J].計算機應用研究,2011,28(12):4607-4612.

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

[9] 陳廷偉,楊艷輝,關長城.基于UCM的領域SOA資產庫構建方法[J]. 計算機工程,2011,37(2):48-51.

[10] 路超,周磊山.基于場景驅動的高鐵應急預案流程控制方法[J].交通運輸系統(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/>.

[責任編輯：蔣海龍]

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-),女,重慶豐都人，講師,博士,主要研究方向為形式化方法和模型驅動開發(fā). E-mail: leeleaf@163.com

TP311.52

A

1671-6876(2016)04-0309-08