李宗花 常逢佳

(淮陰師范學(xué)院計算機科學(xué)與技術(shù)學(xué)院 江蘇 淮安 223300)

0 引 言

模型驅(qū)動體系結(jié)構(gòu)(Model Driven Architecture，MDA)中，計算無關(guān)模型(Computation Independent Model，CIM)代表業(yè)務(wù)視圖，主要描述系統(tǒng)被使用的情形，關(guān)注系統(tǒng)的環(huán)境和需求而不需要了解系統(tǒng)結(jié)構(gòu)的細(xì)節(jié)[1-2]。而平臺無關(guān)模型(Platform Independent Model，PIM)代表系統(tǒng)視圖，描述獨立于平臺的功能實現(xiàn)細(xì)節(jié)[1,3]。PIM層次上的工作流模型與CIM層次上的工作流模型相比，具有更多、更完善的實現(xiàn)細(xì)節(jié)。然而PIM層次上的初始工作流模型往往由CIM層次上的工作流模型轉(zhuǎn)換而來。經(jīng)過完善和細(xì)化(refinement)的PIM工作流模型如果改變了CIM層次上規(guī)定的動作執(zhí)行順序，表明實現(xiàn)一個業(yè)務(wù)服務(wù)的執(zhí)行流程被更改，說明工作流模型的細(xì)化和改進(jìn)改變了業(yè)務(wù)需求。這些細(xì)化和完善操作會造成分析與設(shè)計上的二義性。對于一個業(yè)務(wù)系統(tǒng)來說，系統(tǒng)視圖上工作流的細(xì)化和完善，是否造成業(yè)務(wù)需求的改變，會對業(yè)務(wù)系統(tǒng)的最終質(zhì)量產(chǎn)生重要的影響[4]。因此，分析PIM層次上的工作流模型與CIM層次上的業(yè)務(wù)流模型的語義一致性顯得尤為必要[5]。

語義一致性的驗證不但存在于模型與模型之間[5-6]，還存在于構(gòu)件與構(gòu)件之間[7]及知識庫的實體鏈接上[8]。Xiu等[5]利用Petri模型解決業(yè)務(wù)流程模型中的數(shù)據(jù)不一致問題，而文獻(xiàn)[6]基于通用本體語義，構(gòu)建了三層本體元模型語義的一致性驗證流程。文獻(xiàn)[7]使用帶有語義約束的UML交互概觀圖來表示基于場景的需求規(guī)約，通過對語義擴(kuò)展接口自動機模型(SIA)和帶語義約束的UML交互概觀圖的行為的理論分析，解決構(gòu)件之間的語義一致性驗證。在知識庫實體方面，文獻(xiàn)[8]提出一種利用知識庫實體間結(jié)構(gòu)化語義的一致性集成實體鏈接算法，提高實體鏈接的準(zhǔn)確率和召回率。文獻(xiàn)[9]提出了使用系統(tǒng)行為屬性的方法來驗證模型精化過程中模型間的一致性，從而找出模型精化過程中的不一致行為。

可見，利用形式化方法驗證語義一致性是當(dāng)前的主流方法。在模型語義一致驗證方面，Petri網(wǎng)作為一個被廣泛使用的形式化模型[10]，無論是控制流、對象流還是信息流，Petri網(wǎng)適用于描述系統(tǒng)的這些“流”行為，該特征使得Petri網(wǎng)更好地定義業(yè)務(wù)流的語義[11-12]。當(dāng)前諸多研究顯示，Petri網(wǎng)能夠形式化MDA框架中與業(yè)務(wù)系統(tǒng)或信息系統(tǒng)行為有關(guān)的每一個層次模型[13]。在CIM抽象層次上，Dijkman等[14]提出將BPMN模型映射至Petri網(wǎng)模型，并應(yīng)用有效性分析技術(shù)分析業(yè)務(wù)過程模型的死鎖與模型正確性狀態(tài)。在PIM抽象層次上，Petri網(wǎng)可以直接描述PIM模型并直接在平臺上自動執(zhí)行[15]；在PSM抽象層次上，Petri網(wǎng)用于描述業(yè)務(wù)服務(wù)模型，且可以直接在DENEB(Development and execution of interoperable dynamic Web processes)平臺上執(zhí)行[12]；在代碼層，Philippi[16]實現(xiàn)了Petri網(wǎng)模型自動生成代碼的功能。此外，Petri網(wǎng)標(biāo)記語言[17-18](Petri Net Markup Language，PNML)是一個基于XML交換格式描述Petri網(wǎng)的語言，能夠被眾多的Petri網(wǎng)建模工具和分析工具識別和讀取，如YAML[19]和ePNK[20]。

因此本文利用Petri網(wǎng)模型對CIM層次的業(yè)務(wù)流模型和PIM層次上的工作流模型進(jìn)行一致性語義分析。

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

定義1一個工作流模型被定義為一個八元組組成的擴(kuò)展Petri網(wǎng)模型[21]，即PN=。其中：IP={ip1,ip2,…,ipn}表示有限個內(nèi)部工作流的集合；OP={op1,op2,…,opn}表示有限個外部工作流的集合；ST={st1,st2,…,stn}表示有限個開始、結(jié)束和網(wǎng)關(guān)元素的集合，sti表示工作流模型中的某個開始節(jié)點、結(jié)束節(jié)點或網(wǎng)關(guān)節(jié)點；BT={bt1,bt2,…,btn}表示有限個動作元素的集合；IA?(IP×ST)∪(IP×BT)∪(OP×ST)∪(OP×BT)表示一組輸入??；OA?(ST×IP)∪(ST×OP)∪(BT×IP)∪(BT×OP)表示一組輸出弧；M0表示初始標(biāo)識；SN=sub表示子工作流模型。

定義2對于任意Petri網(wǎng)模型EPN=，??st1,st2∈ST，若IP(bt1×ip1)=IP(ip1×bt2)，或者OP(bt1×op1)=IP(op1×bt2)，則設(shè)定ρ:bt1→bt2，表示動作節(jié)點bt1和bt2之間存在順序關(guān)系，bt1和bt2是一個執(zhí)行順序?qū)?，表示為bt1→bt2，表明bt1在bt2之前實施。ρ表示連接這兩個節(jié)點的place節(jié)點。本文定義source(·)和target(·)兩個函數(shù)表示連接IP或OP節(jié)點的前驅(qū)節(jié)點和后繼節(jié)點，因此有source(ρ)=bt1，target(ρ)=bt2。

而多個執(zhí)行順序?qū)Γ由祥_始順序?qū)徒Y(jié)束執(zhí)行順序?qū)涂梢越M成一個執(zhí)行順序序列Pi={st1→bt1→bt2→…→stn}。

2 語義一致性驗證

2.1 驗證思路

由于在PIM抽象層次上需要進(jìn)一步細(xì)化工作流，CIM抽象層次上的業(yè)務(wù)活動在PIM抽象層次上將被細(xì)化為若干個原子活動。因此，這兩個層次模型的語義一致性驗證主要考慮細(xì)化的程度，即CIM層次上的活動及活動的執(zhí)行順序在PIM層次上做了何種修改。

因此，本節(jié)定義了PIM工作流模型與CIM業(yè)務(wù)流模型之間存在三種不同情形的細(xì)化：(1) 分層獨立，在PIM工作流模型中完全找不到一個CIM業(yè)務(wù)流模型中的原子活動(事件或任務(wù))。(2) 分層細(xì)化，在PIM工作流模型中存在一個參與者對象，當(dāng)且僅當(dāng)找到一個該參與者對象所作用的原子活動，這一原子活動在CIM業(yè)務(wù)流模型中也是由該參與者作用的。(3) 部分細(xì)化，在PIM工作流模型中存在一些原子活動與CIM業(yè)務(wù)流模型中的原子活動相互交織。

2.2 語義驗證方法

接下來從形式化語義上定義CIM業(yè)務(wù)流模型與PIM工作流模型之間三種不同情形的細(xì)化條件。

給定CIM業(yè)務(wù)流模型PN1，PIM工作流模型PN2，設(shè)∑C1表示模型PN1中所有活動元素的集合，∑C2表示模型PN2中所有活動元素的集合?！艭=∑C1∩∑C2表示為PN1和PN2中相同活動的集合。在判斷CIM業(yè)務(wù)流模型是否與CIM工作流模型語義一致時，必須先判斷它們相同活動的執(zhí)行順序?qū)鲜峭耆恢碌?，即?SequencePN1|∑C)=∑(SequencePN2|∑C)。當(dāng)該條件滿足的情況下，設(shè)∑Sequence-pn1表示PN1模型中的所有執(zhí)行順序?qū)?，∑Sequence-pn2表示為PN2模型中的所有執(zhí)行順序?qū)?，則滿足以下條件：

(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模型的細(xì)化和提煉操作屬于分層獨立。這意味著在細(xì)化后的PIM工作流模型中找不到任何一個CIM業(yè)務(wù)流模型中的原子活動。

以圖1所示的CIM業(yè)務(wù)流模型和PIM工作流模型來說明分層獨立的問題。圖1中下方所示的工作流模型中存在執(zhí)行順序?qū)→SP1-A，其source(B→SP1-A)∈{A,B,C}，而target(B→SP1-A)∈{SP1-A,SP1-B,SP1-C}；同時還存在一個執(zhí)行順序?qū)P1-C→C，source(SP1-C→C)∈{SP1-A,SP1-B,SP1-C}，而target(B→SP1-A)∈{A,B,C}；這兩個執(zhí)行順序?qū)Ψ謩e表示CIM業(yè)務(wù)流模型中子過程SP1的輸入流節(jié)點和輸出流節(jié)點。而細(xì)化后的PIM工作流模型中這兩個執(zhí)行順序?qū)Φ那膀?qū)節(jié)點和后繼節(jié)點卻與BPMN模型中保持一致。因此，圖1中虛線框內(nèi)的原子活動節(jié)點對于CIM業(yè)務(wù)流模型中的子過程SP1來說屬于分層獨立。

圖1 PIM工作流模型分層獨立

(2) 分層細(xì)化。?Sequence-pn2i,Sequence-pn2j∈∑Sequence-pn2，?ati∈∑C1∩∑C2，?x,y∈∑C2-∑C1，?sequence-pn2i:x→ati,sequence-pn2j:ati→y，則表明PN2模型針對PN1模型的細(xì)化和提煉操作屬于分層細(xì)化。意味著在細(xì)化后的PIM工作流模型中當(dāng)且僅當(dāng)能找到一個原子活動ati，該原子活動同時也在CIM業(yè)務(wù)流模型中存在。

以圖2所示的CIM業(yè)務(wù)流模型和PIM工作流模型來說明分層細(xì)化的問題。從圖2中下方所示的PIM工作流模型中可見，原子活動B∈∑C1∩∑C2，而與節(jié)點B存在執(zhí)行順序關(guān)系的節(jié)點SP1-A,SP1-B∈∑C2-∑C1，存在兩個執(zhí)行順序?qū)P1-A→B和B→SP1-B。這表明在子過程SP1中將CIM業(yè)務(wù)流模型中的原子節(jié)點B作為細(xì)化模型中的原子活動，即原子節(jié)點B的直接前驅(qū)和直接后繼都是屬于子過程SP1的原子活動?？梢?，圖2中虛線框內(nèi)的原子節(jié)點是子過程SP1的分層細(xì)化。

圖2 PIM工作流模型分層細(xì)化

(3) 部分細(xì)化。?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，細(xì)化的PIM工作流模型中至少有一個原子活動ati，它的緊鄰前驅(qū)節(jié)點或者緊鄰后繼節(jié)點存在多個。

同時，?Sequence-pn1i∈∑Sequence-pn1，?source(sequence-pn2j)=source(sequence-pn1i)，或者?target(sequence-pn2j)=target(sequence-pn1i)，表明在細(xì)化的PIM工作流模型中，原子活動ati的多個執(zhí)行順序?qū)χ兄辽俅嬖谝粋€執(zhí)行順序?qū)?，其源?jié)點或者目標(biāo)節(jié)點是CIM業(yè)務(wù)流模型中的原子活動。表明細(xì)化后的PN2模型中的原子活動節(jié)點與PN1模型中的原子節(jié)點存在相互交織的情況。滿足這種條件的PN2模型針對PN1模型的細(xì)化和提煉操作屬于部分細(xì)化。

以圖3所示的CIM業(yè)務(wù)流模型和PIM工作流模型來說明部分細(xì)化的問題。從圖3中下方的工作流模型可見，與原子活動節(jié)點SP1-B有關(guān)的執(zhí)行順序?qū)Πㄈ齻€：SP1-A→SP1-B，D→SP1-B，SP1-B→SP1-C，而SP1-A,SP1-B,SP1-C∈∑C2-∑C1，而節(jié)點D∈∑C1∩∑C2。這表明節(jié)點SP1-B的緊鄰前驅(qū)節(jié)點D是CIM業(yè)務(wù)流模型中的原子節(jié)點，且原子節(jié)點D也正好是子過程SP1的緊鄰前驅(qū)節(jié)點，即source(D→SP1)=source(D→SP1-B)。因此CIM業(yè)務(wù)流模型中的原子節(jié)點D與細(xì)化PIM工作流模型中的原子節(jié)點SP1-B相互交織。同樣，CIM業(yè)務(wù)流模型中的節(jié)點C也與細(xì)化PIM工作流模型中的原子節(jié)點SP1-A相互交織。因此，圖3所示的PIM工作流模型是對CIM業(yè)務(wù)流模型的部分細(xì)化。

圖3 PIM工作流模型部分細(xì)化

2.3 驗證步驟

步驟一計算兩個模型中相同原子活動的執(zhí)行順序?qū)稀?SequencePN1|∑C)和∑(SequencePN2|∑C)。如果∑(SequencePN1|∑C)=∑(SequencePN2|∑C)，轉(zhuǎn)向步驟二；否則，表明細(xì)化的PIM工作流模型完全改變了CIM業(yè)務(wù)流模型中業(yè)務(wù)活動執(zhí)行順序，導(dǎo)致業(yè)務(wù)視圖模型與系統(tǒng)視圖模型不一致。

步驟二分別計算PN1模型和PN2模型的所有執(zhí)行順序?qū)Α?Sequence-pn1|∑C1)和∑(Sequence-pn2|∑C2)。

步驟三計算PN2模型中細(xì)化的所有原子活動節(jié)點∑C2-∑C1。

步驟四應(yīng)用2.2節(jié)定義的三個條件進(jìn)行比較分析。

3 語義一致性驗證

根據(jù)以上四個驗證步驟，以網(wǎng)上購物系統(tǒng)為例，分析圖4所示的CIM業(yè)務(wù)流模型與圖5所示的細(xì)化PIM工作流模型之間的語義一致性問題。可見圖5所示的PIM工作流模型是細(xì)化了圖4中支付服務(wù)。因此，設(shè)圖4為PN1，圖5為PN2。

圖4 網(wǎng)上購物系統(tǒng)的CIM形式化業(yè)務(wù)流模型

圖5 網(wǎng)上購物系統(tǒng)的PIM形式化工作流模型

第一步：首先計算兩個模型的相同節(jié)點集合。

∑C=∑C1∩∑C2={搜索商品，接收搜索需求，商品推薦服務(wù)，接收商品選項，選擇商品，下訂單，支付，驗證信用卡，確認(rèn)訂單，發(fā)送通知}。然后，基于相同節(jié)點集合，計算CIM業(yè)務(wù)流模型和PIM工作流模型執(zhí)行順序?qū)稀?SequencePN1|∑C)=∑(SequencePN2|∑C)={搜索商品接收搜索需求,接收搜索需求商品推薦服務(wù)，商品推薦服務(wù)接收商品選項，接收商品選項搜索商品，接收商品選項選擇商品，選擇商品下訂單，下訂單支付，確認(rèn)訂單發(fā)送通知}。

可以看出∑(SequencePN1|∑C)=∑(SequencePN2|∑C)，表明細(xì)化后的PIM工作流模型中，其業(yè)務(wù)服務(wù)活動的執(zhí)行順序與CIM業(yè)務(wù)流模型中的執(zhí)行順序保持了一致(順序流一致)，其消息發(fā)送者與消息接收者也保持了一致(消息流一致)。

第二步：計算PN1模型和PN2模型的所有執(zhí)行順序?qū)Α?Sequence-pn1|∑C1)和∑(Sequence-pn2|∑C2)。其中：∑(Sequence-pn1|∑C1)={搜索商品接收搜索需求,接收搜索需求商品推薦服務(wù)，…，下訂單支付，支付支付服務(wù)，支付服務(wù)驗證信用卡，支付服務(wù)確認(rèn)訂單，確認(rèn)訂單發(fā)送通知}，∑(Sequence-pn2|∑C2)={搜索商品接收搜索需求,接收搜索需求商品推薦服務(wù)，…，支付接收支付信息，接收支付信息發(fā)送信用卡信息，發(fā)送信用卡信息驗證信用卡，驗證信用卡訂單收費，訂單收費確認(rèn)訂單，確認(rèn)訂單發(fā)送通知}。

第三步：計算PN2模型中細(xì)化的所有原子活動節(jié)點。

∑C2-∑C1={接收支付信息，發(fā)送信用卡信息，訂單收費}，∑C2-∑C1集合中的原子活動節(jié)點就是PN1模型中子EPN模型支付服務(wù)的細(xì)化。

第四步：比較分析。?Seq1,Seq2∈∑Sequence-pn2,?驗證信用卡∈∑C1∩∑C2，?發(fā)送信用卡信息，訂單收費∈∑C2-∑C1，?seq1:發(fā)送信用卡信息→驗證信用卡，seq2:驗證信用卡→訂單收費，表明細(xì)化后的PIM工作流模型中當(dāng)且僅當(dāng)找到一個原子活動“驗證信用卡”，該活動同時也存在于CIM業(yè)務(wù)流模型中。

從以上四個模型驗證步驟可知，圖5所示的模型的細(xì)化操作屬于分層細(xì)化。細(xì)化后的PIM工作流模型與CIM抽象層次上的業(yè)務(wù)流模型在語義上保持了一致。

4 結(jié) 語

針對PIM抽象層次中的工作流模型細(xì)化問題，本文利用擴(kuò)展Petri網(wǎng)模型，首先設(shè)計了PIM工作流模型細(xì)化的分層獨立、分層細(xì)化和部分細(xì)化的三種不同情形；然后從語義上定義了這三種細(xì)化的條件，并設(shè)計了這三種不同情形細(xì)化的驗證步驟；最后應(yīng)用網(wǎng)上購物系統(tǒng)演示了CIM業(yè)務(wù)流模型與PIM工作流模型之間的一致性驗證過程。實例驗證結(jié)果表明，本文設(shè)計的語義一致性驗證方案，可有效地驗證PIM抽象層次上的工作流模型在細(xì)化和修改的過程中，是否影響了系統(tǒng)的業(yè)務(wù)流，以及其影響的程度。