侯金奎，鹿旭東，陳春雷，王 磊

1(濰坊學院 計算機工程學院,山東 濰坊 261061)

2(山東大學 軟件學院，濟南 250061)

1 引 言

近年來，隨著云計算的服務模式在業(yè)界的廣發(fā)應用和迅猛發(fā)展，基于網(wǎng)絡的服務系統(tǒng)正在不斷替代傳統(tǒng)意義上的計算系統(tǒng)和軟件系統(tǒng)[1].Web服務是落實云計算環(huán)境中各類資源及能力交付和使用模式的主要方式，可以方便地滿足用戶需求，是實現(xiàn)面向服務計算的主要技術[2].大型復雜Web系統(tǒng)在其模型描述和系統(tǒng)演化的過程中，需保持清晰、易理解、可追蹤、可驗證、易修改[3].針對大型Web服務系統(tǒng)的建模、開發(fā)以及系統(tǒng)重構(gòu)技術和方法進行研究，為此類系統(tǒng)的設計和實現(xiàn)提供有效的方法學指導，提出有效的技術手段來提升軟件研發(fā)的質(zhì)量和效率，已成為當前面向服務的軟件工程面臨的一個亟待解決的重要任務[4].已有的研究都是針對特定的應用領域和場景[5,6]，提出的實現(xiàn)方案[7]，但這些工作并不能對一般意義下大型復雜Web系統(tǒng)的模型演化和特性考察提供支持.

采用模型驅(qū)動的軟件開發(fā)(model driven software development)方法是應對軟件開發(fā)和維護復雜性的一種有效手段，它以模型為核心制品，通過一系列的模型轉(zhuǎn)換來生成最終的目標系統(tǒng)[8].模型驅(qū)動開發(fā)作為一種開放性的理念和模式，已經(jīng)被學術界和業(yè)界廣泛接受并表現(xiàn)出了極強的生命力[6,7].模型轉(zhuǎn)換是模型驅(qū)動軟件開發(fā)的關鍵步驟，以實現(xiàn)不同抽象層次模型之間的轉(zhuǎn)換和精化[9].為了支持模型驅(qū)動開發(fā)中的模型的自動轉(zhuǎn)換，需要精確地定義和描述模型以及模型的變化.從技術發(fā)展的角度看，基于構(gòu)件和構(gòu)件組裝的工業(yè)化軟件開發(fā)仍是快速構(gòu)造系統(tǒng)、降低開發(fā)費用、減輕維護負擔的主流方案[10].市場和業(yè)界多年來的實踐和驗證也都表明，基于構(gòu)件的軟件工程和模型驅(qū)動開發(fā)方法的結(jié)合是成功的，發(fā)展前景良好.

范疇理論[11]描述能力強，可為Web服務系統(tǒng)的層次結(jié)構(gòu)提供形式化的語義描述.在我們的前期工作中[12-14]，已將范疇理論用于軟構(gòu)件和體系結(jié)構(gòu)模型之間映射關系的描述.本文進一步擴展了這種思想，從軟件設計實踐和基于體系結(jié)構(gòu)，面向軟構(gòu)件和設計模式的軟件設計出發(fā)，提出了軟件設計和精化中的模型轉(zhuǎn)換和模型驅(qū)動的軟件開發(fā)理論框架.設計模式看成是構(gòu)件規(guī)范的模版，模板的實例化和規(guī)范的集成過程就是軟件設計和實現(xiàn)的過程，在此基礎上，建立起了模型轉(zhuǎn)換和精化中特性描述和一致性研究的統(tǒng)一框架.應用研究表明，該框架符合模型驅(qū)動軟件設計的本質(zhì)要求，為模型轉(zhuǎn)換和模型驅(qū)動的Web應用服務開發(fā)提供了新的認知、分析和研究的指導架構(gòu).

2 模型定義

參考文獻[13]、[14]和[15]，本文給出標識、對象類型、對象關系等定義.在此基礎上，進一步定義規(guī)范、規(guī)范轉(zhuǎn)換、規(guī)范模板及規(guī)范集成等概念.

定義1.構(gòu)件對象標識(Component Object Signature). 標識Scmp=是一個三元組.其中,SDT是一個數(shù)據(jù)類型標識，SAT是構(gòu)件的特性符號組成的集合，SAC是構(gòu)件的動作符號組成的集合.

定義2.構(gòu)件對象類型(Component Object Type).對象類型是構(gòu)造具有序偶OTcmp=所描述共同特性的對象實例的模版,其中Scmp是一個構(gòu)件對象的標識，SAX是一個Scmp相關公式和公理組成的集合.

定義3.對象關系類型(Types of Object Relationships). 定義對象關系機制集合為R={R1，…，Rm>0}.其中每一個Ri是具有特定機制的對象間關聯(lián)方式.對于給定的對象類型集合OT={OT1,…，OTn>0}.對象關系類型集合RT=={RT1，…，RTu>1}.其中每一個RTi=Ri,是一個具有類型Ri∈R的對象類型OTp∈OT和OTq∈OT間有向序偶關系.

對象關系機制是由軟件的模型或平臺所提供和決定的[12].常見的關系機制有：方法調(diào)用、事件激發(fā)、消息發(fā)送、數(shù)據(jù)傳送、遠程過程調(diào)用等.特定對象間的關系是受到對象類型和關系機制約束的.這是軟件構(gòu)造實踐中考察一個系統(tǒng)內(nèi)對象或構(gòu)件間關系兼容性的基本必要條件.

定義4.對象關系實例的標識.對于對象關系類型RTi=Ri，它的一個關系實例是RO=Ri，它是由ORType標識以及由該標識形成的對象類型所生成的實例(參見圖1)；其中，Xp∈X(OTp)，EqE(OTq).

該標識名是用于表達和生成對象關系實例的.圖1給出了對象關系實例的標識和對象類型的結(jié)構(gòu)框架.其中,GetActionNames獲得在SO的Gso動作中調(diào)用DO.Gdo動作的文字說明，被用于改寫SO對象中Gso動作的行為；Σ代表對字符串的并置運算.

定義5.類型化范疇(Typed Category). 類型化范疇[16]是一個5元組TC=，其中：OT是非空對象類型集合，R是非空對象關系機制集合，RT是非空對象關

ORType//RTi=Ri的關系實例的標識

//和對象類型Ri

圖1 對象關系類型的標識和對象類型Fig.1 Signature and object type of types of object relationships

系類型集合，O={O1,…，On>0}(Oi的類型∈OT)是非空對象實例集合，F(xiàn)={F1，…，F(xiàn)m≥0}(Fi的類型Ri∈RT)是對象關系實例集合,其中Fi=Ri，Xp∈X(OTp)，EqE(OTq).由此，TC：(1)為f∈F指派一個操作,它是從f定義域的一個對象實例a∈O到f值域的一個對象實例b∈O,如果a= domf并且b= codf,那么f被表示為f:a→b；(2)為g，f∈F的關系對指派一個合成操作.,它是f與g的合成,記為g.f:domf→ codg,其中domg= codf.

由定義5，軟件體系結(jié)構(gòu)模型(Software Architecture)就是一個類型化范疇SA=.

根據(jù)類型化范疇的定義,極端情況下體系結(jié)構(gòu)只有一個構(gòu)件對象構(gòu)成.

定義6.體系結(jié)構(gòu)的標識及其對象類型. 由SAType()構(gòu)造的標識以及由該標識形成的對象類型，是用于表達體系結(jié)構(gòu)語義和生成體系結(jié)構(gòu)實例的一個特別的標識以及由該標識形成的對象類型.

圖2給出了由體系結(jié)構(gòu)范疇構(gòu)造標識和對象類型的結(jié)構(gòu)框架.其中，addTo()動作用文字串s改寫對象so的動作Gso的內(nèi)容，由此改寫了Gso的行為構(gòu)成.

注意，某些構(gòu)件類型是不能通過外部改寫其行為特性的.這時，應該限制其只能接受操作，而不能向其他對象發(fā)出操作.

3 服務模型轉(zhuǎn)換

規(guī)范引入了范疇符號和操作符號，并且定義了實現(xiàn)或被規(guī)范的模型必須具有的特性[17].

定義7.構(gòu)件規(guī)范(Component Specification).規(guī)范SP是一個序偶，其中SA=是一個體系結(jié)構(gòu)，Φ是一個由SA成份構(gòu)成的SA-句子匯集.所有SA-句子的集合表示為Sen[SA].

SAType//體系結(jié)構(gòu)范疇的標識和對象類型

圖2 體系結(jié)構(gòu)類型的標識和對象類型Fig.2 Signature and object type of types of software architecture

規(guī)范SP=的模型是一個SA-模型M，其中對每一個ψ∈Φ有M┝ψ.所有這種模型M的集合表示為Mod[SP].

為簡便，以后的討論中規(guī)范的特性集也用規(guī)范的名稱表示.

定義8.規(guī)范態(tài)射(Specification Morphism).從規(guī)范SP=到規(guī)范SP′ =的一個規(guī)范態(tài)射，是一個體系結(jié)構(gòu)態(tài)射σ:SA→SA′，使得每一個模型M∈Mod[SP′]可有M|σ∈Mod[SP]，其中M|σ是M的反函子(reduct functor).規(guī)范態(tài)射可表示為σ：SA→SA′.

函子(Functor)F(A，B)是從范疇A到范疇B的函數(shù)，它為每一個A對象指派一個B對象，并為每一個A中f：a→b指派一個B中F(f)：F(a)→F(b)，使得等態(tài)射和合成關系得到保持.Functor定義了范疇A到B的變換關系.反函子Reduct functor是與函子相反的變換.給定范疇A、B，從A到B的函子F定義了A是如何被包含在B中，而F的反函子B|F定義了B是如何從A形成的.

定義9.規(guī)范態(tài)射的類型(Types of Specification Morphism).設SP={S1，…，Sm>0}是所有規(guī)范的集合.規(guī)范態(tài)射是滿足特定約束C的兩個或多個規(guī)范之間的有向關系，具體形式有{S1，…，Sn>0} →t∈STS和S→t∈ST{S1，…，Sn>0}，其中S∈SP和Si∈SP都是規(guī)范，ST是有限規(guī)范態(tài)射的關系類型，ST={轉(zhuǎn)換/t，分解/a，選擇/o，And合成/ac，Or合成/oc，集成/i，復制/d，不計類型/st}.

轉(zhuǎn)換和復制都是與常規(guī)概念類似的簡單的規(guī)范態(tài)射，其它則是與常規(guī)概念不同的復雜規(guī)范態(tài)射.

定義10.轉(zhuǎn)換(Transformation).轉(zhuǎn)換F具有形式F:S1→TS2，其中S1，S2∈SP都是規(guī)范，→T代表有向關系為轉(zhuǎn)換的規(guī)范態(tài)射關系，并滿足以下特性：每一個S1中的對象a映射為S2中的對象b;為每一個S1中的關系f：a→b映射為S2中的一個關系F(f)：F(a) →F(b);a∈S1有F(ida) =idF(a);并且，對于S1中的關系合成g°f,有F(g°f) =F(g)°F(f).

圖3(a)給出了轉(zhuǎn)換的圖式表達，圖3(c)給出了多次轉(zhuǎn)換關系的合成關系.轉(zhuǎn)換關系及其合成可以用來表達在語義保持的約束下從模型到實現(xiàn)的軟件精化過程.

定義11.規(guī)范模版(Template of Specification). 規(guī)范模版[14]是一個規(guī)范類型SP(T1s1:t1,…,Tnsn:tn>0)的，其中，Tksk∶tk表示用于SP實例化的參數(shù)，Tk是形式參數(shù)，si是其類型，ti表示參數(shù)的傳送方式，可以是替換或引用的方式來實現(xiàn)參數(shù)傳送.

簡言之，規(guī)范模版是一個還沒有實例化的規(guī)范.如果不需要，可以不區(qū)分規(guī)范和規(guī)范模版，而通稱為規(guī)范.

定義12.規(guī)范模版的實例化(Instantiation of Specification Template).規(guī)范模版SP(T1s1∶t1，…，Tnsn∶tn>0)被規(guī)范S的實例化表示為運算=S<+SP(t1，…，tn)，其中，tk是S或S中某成份的標識，M是實例化后得到的規(guī)范實例，它是用S或S中的成份替換SP中相應成份后得到的規(guī)范.S可以是一個規(guī)范集合，此時，tk∈S或tk是S中某規(guī)范的某成份標識.同理，可以定義實例化運算=SP(t1，…，tn)+>S.

定義13.集成(Integration).規(guī)范S1，S2∈SP的集成是一個新的規(guī)范,記為S=S1+S2,+∈{<+,+,},表示按照特別的運算關系計算得到規(guī)范S；其中，S=S1S2表示按特性合一運算[14]；S=S1<+S2表示以S1為核通過結(jié)合S2獲得S；S=S1+>S2表示以S2為核通過結(jié)合S1獲得S.

定義14.集成的框與核(frame，kernel of Integration).當規(guī)范S1，S2∈SP發(fā)生S=S1+S2,+∈{<+,+>},的集成或結(jié)合時，在集成后的規(guī)范S中處于主導地位的S1或S2，稱為該特性集成的框，另一方稱為該特性集成的核.如果不存在處于主導地位的規(guī)范，或?qū)τ赟=S1S2,則稱該集成是無框或無核的.

圖3(d)給出了特性集成的一般圖式表達.圖3(c)表示以模型為核,結(jié)合環(huán)境的約束得到滿足語義保持的軟件實現(xiàn)的轉(zhuǎn)換關系.圖3(f)表示M1經(jīng)過兩次引入新的約束后得到M2

圖3 規(guī)范的轉(zhuǎn)換特性集成關系Fig.3 Property integration relationships of specification transformation

的轉(zhuǎn)換.圖中以實心菱形箭頭表示的是有核集成的框，核是用通常的三角箭頭表示的.

特性集成用來表示引入環(huán)境、平臺、模式、方面或其它模型等約束后得到的新的合成規(guī)范.

由于特性集成概念的存在，而且規(guī)范都是在相同抽象層次上的特性描述，因此,不引入新的規(guī)范而進行的規(guī)范轉(zhuǎn)換沒有改變抽象的層次，是沒有實際本質(zhì)意義的.據(jù)此，本文以下關于轉(zhuǎn)換的討論主要都是關于或用于集成方面的.

定義15.分解/And分解(Decomposition).設M是規(guī)范S∈SP的特性集，S的分解表示為態(tài)射集合{S→aS1，…，S→aSn>0},其中,每一個Si也是規(guī)范,其特性集表示為Mi,并且滿足要求(MiM)(M1M2…Mn=M).

圖4(a)給出了規(guī)范分解的圖式表示.規(guī)范的分解抽象地描述了復雜的模型經(jīng)過分解和合成的軟件實現(xiàn).基于體系結(jié)構(gòu)規(guī)范的系統(tǒng)構(gòu)造就是經(jīng)過分解、成分構(gòu)造，而后成分合成而建立的.

圖4 規(guī)范的分解和選擇關系Fig.4 Decomposition and alternative of specification

定義16.選擇/Or選擇(Alternative).設M是規(guī)范S∈SP的特性集，S的選擇表示為態(tài)射集合{S→oS1，…，S→oSn>0},其中，每一個Si也是規(guī)范,并且滿足要求S=Si.

圖4(b)給出了規(guī)范選擇的圖式表示.“Or選擇”指任選其一的運算，特指多個分支轉(zhuǎn)換關系中任選其中一個的設計選擇；對于各個分支，其實都是源規(guī)范的等價復制；所以，選擇等價于多個規(guī)范的復制.

由圖4可以看出，從范疇角度看，規(guī)范的分解和選擇都是類似椎(cone)[11]的概念.以下規(guī)范的合成則是類似余錐(cocone)[11]概念，它們的出現(xiàn)應該看成是對規(guī)范分解和選擇的逆或?qū)ε歼\算.對于建立完整的模型轉(zhuǎn)換概念這是必須的，這可以通過圖4中它們的出現(xiàn)情況說明.

圖5 規(guī)范的選擇與合成關系舉例Fig.5 Example of alternative and composition

規(guī)范的合成有“And合成”和“Or合成”兩種類型.

定義17.And合成(And Composition).設M是規(guī)范S∈SP的特性集，S的And合成表示為態(tài)射集合{S1→acS，…，Sn→acS},其中,每一個Si也是規(guī)范，其特性集表示為Mi，并且滿足要求(M=M1M2…Mn).

定義18.Or合成(Or Composition).設M是規(guī)范S∈SP的特性集，S的Or合成表示為態(tài)射集合{S1→ocS，…，Sn→ocS},其中，每一個Si也是規(guī)范,其特性集表示為Mi,并且滿足要求(S=Si)(M=Mi).

“And合成”是“And分解”的對偶，“Or合成”是“Or選擇”的對偶，而且它們的出現(xiàn)應該是成對的.圖4通過圖示說明了這種對偶的出現(xiàn)，其中間節(jié)點所代表的規(guī)范可以進一步發(fā)生其它轉(zhuǎn)換、分解和選擇.

圖4(a)還指出，分解和And合成的綜合轉(zhuǎn)換結(jié)果是(P1→S1Q1→T1M21)(P2→S2Q2→T2M22),這與轉(zhuǎn)換M1→TM2從結(jié)構(gòu)邏輯上是等價的.類似地，圖3(b)指出,選擇和Or合成的綜合轉(zhuǎn)換結(jié)果是(P1→S1Q1→T1M2)(P2→S2Q2→T2M2),這與轉(zhuǎn)換M1→TM2從語義邏輯上應該是等價的.

圖5給出了一個規(guī)范經(jīng)過選擇和集成，而后又經(jīng)合成和集成所形成的轉(zhuǎn)換過程.M1→TM2= 其綜合轉(zhuǎn)換結(jié)果是((M11+N11)→F1Q1→T1M21)((M12+N12)→F2Q2→T2M22),這從語義邏輯上與轉(zhuǎn)換M1→TM2等價.

定義19.規(guī)范范疇(SpecificationCategory). 規(guī)范范疇SC=，其中，S={S1,…,Sn>0}是非空規(guī)范集合,ST={轉(zhuǎn)換/t，分解/a,選擇/o,And合成/ac,Or合成/oc,集成/i,復制/d,不計類型/st }是態(tài)射類型集合，T={Si→stSj|Si,Sj∈S，st∈RT}是可為空的規(guī)范態(tài)射集合；其中，(規(guī)范復制)→d是一個等價態(tài)射.

可見，規(guī)范范疇也是一個類型化的范疇.

定義20.轉(zhuǎn)換路徑(Route of Transformation).對于規(guī)范M1和M2，如果可由M1經(jīng)歷一次或多次轉(zhuǎn)換態(tài)射推導而到達M2，則稱存在一條從M1到M2的轉(zhuǎn)換路徑R，并記為Rou∶M1M2.對于經(jīng)歷一次的轉(zhuǎn)換記為R∶M1→stM2.

定義21.路徑等價性(Equivalence of Route). 兩條從規(guī)范M1到M2的轉(zhuǎn)換路徑Rou1∶M1M2和Rou2∶M1M2是等價的，記為Rou1=Rou2，當且僅當轉(zhuǎn)換的結(jié)果都得到相等的特性集合.

考慮轉(zhuǎn)換的語義保持性，可以得到在語義保持意義下兩條從規(guī)范M1到M2轉(zhuǎn)換路徑的等價性定義.

使用以上對于分解,選擇和合成關系的簡記形式,可以得到如下推論：

推論1. 對于規(guī)范M1,M2,S={S1,…,Sn>0}∈SP,以下態(tài)射關系集合所表達的轉(zhuǎn)換關系是等價的：

M1→TM2= {M1→aS1→acM2，…，M1→aSn→acM2}；

M1→TM2= {M1→oS1→ocM2，…，M1→oSn→ocM2}.

以上關系形成了發(fā)自M1到達M2的路徑束(bundle of route).如果壓縮這個束,以上關系可簡記為：

M1→TM2= {M1→aS→acM2},當S={S1,…,Sn>0}；

M1→TM2= {M1→oS→ocM2},當S={S1,…,Sn>0}.

推論2. 對于規(guī)范M1,M2，S1={S11,…,S1n>0}，S2={S21,…,S2n>0}∈SP,以下態(tài)射關系集合所表達的轉(zhuǎn)換關系是等價的,其中指不計類型和次數(shù)的轉(zhuǎn)換.這里再次出現(xiàn)了路徑束及其壓縮現(xiàn)象：

M1→TM2= {M1→aS11S21→acM2，…，M1→aS1nS2n→acM2} = {M1→aS1S2→acM2}

M1→TM2= {M1→oS11S21→ocM2，…，M1→oS1nS2n→ocM2} = {M1→oS1S2→ocM2}

兩條不包含分解、選擇、合成、集成的從規(guī)范M1到M2的轉(zhuǎn)換路徑的等價性是容易判定的.使用以上的兩個推論可以得到類似，但可包含分解、選擇、合成、集成的兩條轉(zhuǎn)換路徑的等價性定義.因此有以下定義.

定義22.良定的規(guī)范范疇(Well-formed Specification Category).規(guī)范范疇SC=是良定的，當且僅當滿足以下條件：

1) 對于T所給出的規(guī)范態(tài)射,存在非空集合NSS和NFS,其中,s∈NS不存在任何s的前驅(qū)，而且s∈NF不存在任何s的后繼；

3) 轉(zhuǎn)換態(tài)射→a和→ac,→o和→oc必須分別先后成對出現(xiàn),其間可以存在其它轉(zhuǎn)換態(tài)射,單不存在與其它→a和→ac,→o和→oc對的交叉.一個良定的規(guī)范范疇可以記為WFSC=.

除具有多種態(tài)射類型外，良定的規(guī)范范疇是一個規(guī)范的偏序集合或DAG(Directed Acyclic Graph)圖.

4 應用研究

本節(jié)通過一個關于學生信息管理的服務系統(tǒng)，作為實例闡述本文所提描述框架的應用.應用示例研究Student對象從基本規(guī)范到具體平臺(J2EE/.NET)下實現(xiàn)Grid展示的轉(zhuǎn)換.其轉(zhuǎn)換框架如圖6所示.考慮到篇幅限制，在示例中做了適當簡化.

圖6 應用示例的轉(zhuǎn)換框架Fig.6 Transformation framework of the exmple

首先建立學生對象規(guī)范Student(圖7)，這是模型設計的基礎，根據(jù)前面定義，主要是屬性、動作和公理的定義屬性有學號、姓名、出生日期等，而在動作中示例中只給出了與出生日期有關的兩個動作.相應的公理則對其作了約束.

根據(jù)設計需求，Student對象規(guī)范實例需要展示在界面中，為此需要建立展示特性規(guī)范PresentPropertyofStudent(圖8)，該規(guī)范中定義了為滿足student規(guī)范實例在界面展示方面的需求，需要增加的屬性及動作等.其中，屬性類型中的alias是別名，主要用于顯示時對屬性的提示說明，length是最大允許長度，這將決定屬性顯示時的布局空間限制.age是新增加的屬性，并指明是屬性birthday的導出項，由此將引起動作的增加，getAge()是完成對屬性值的提取，而calculteAge()則描述導出語義，其中Current是指當前日期.需要說明的是calculteAge()被激發(fā)完成age屬性的重新計算后，所有已經(jīng)被調(diào)用的getAge()動作需要重新激發(fā)，以完成age屬性值的同步.

圖7 學生對象規(guī)范Fig.7 Specification of student

圖8 展示特性規(guī)范Fig.8 Specification of presentive property

圖9 集成顯示特性的規(guī)范Fig.9 Specification of presentive property integrated

基本對象規(guī)范集成展示特性規(guī)范會形成適合界面展示方面需求的規(guī)范，此規(guī)范將作為界面展示轉(zhuǎn)換的設計基礎.根據(jù)前面集成定義，完成StudentPresentPropertyofStudent計算將很容易得到集成顯示特性的學生規(guī)范IntegratedStudent(圖9).需要說明的是由于age是birthday的導出項，在集成后的公理中增加了setBirthday(d)=> calculteAge()，語義為出生日期的設置將會引起年齡的重新計算.

設計需求表明，最終呈現(xiàn)在界面上的將是對象匯集，而對象匯集具有其特殊的結(jié)構(gòu)和操作特性，為此建立匯集特性規(guī)范模板