陳 穎，劉冬梅，朱 鴻，蘭 斌，何娟娟

(1.南京理工大學計算機科學與工程學院，江蘇 南京 210094;2.英國Oxford Brookes大學計算與通信系，英國 牛津 OX33 1HX)

1 引言

近年來，服務(wù)計算得到越來越廣泛的關(guān)注和應(yīng)用[1]。面向網(wǎng)絡(luò)、分布式、模塊化的服務(wù)計算已經(jīng)成為支持異構(gòu)環(huán)境下分布式計算的主要途徑[2]。然而，單個服務(wù)提供的功能有限，為更充分地利用已有服務(wù)，提高系統(tǒng)開發(fā)效率，需要將單個服務(wù)組合成更強大的服務(wù)。因此，服務(wù)組合一直是服務(wù)計算研究的熱點。現(xiàn)有的服務(wù)組合描述方法主要基于業(yè)務(wù)流程，這些方法雖然可以有效地描述組合服務(wù)的實現(xiàn)方式，但缺乏對預期組合結(jié)果的功能性語義定義，從而難以支持服務(wù)組合正確性的驗證和測試[3,4]。

代數(shù)規(guī)約[5]作為一種形式化方法，最早被用于描述抽象數(shù)據(jù)類型。在過去30多年中，它發(fā)展到用于描述各種軟件系統(tǒng)，尤其是將行為代數(shù)[6]和合代數(shù)[7 - 9]理論相結(jié)合后，能夠抽象地描述并發(fā)系統(tǒng)、基于狀態(tài)系統(tǒng)和軟件構(gòu)件。在前期工作中，我們擴展了行為代數(shù)和合代數(shù)理論，提出面向服務(wù)的代數(shù)規(guī)約語言SOFIA(Service-Oriented Formalism In Algebras)[10]，并開發(fā)了自動化測試工具，實現(xiàn)了基于SOFIA語言書寫的規(guī)約對單個服務(wù)進行自動化測試[11,12]。與其他形式化方法相比，代數(shù)規(guī)約高度抽象且支持自動化軟件測試[11 - 15]。

本文針對服務(wù)組合的正確性驗證和測試問題，提出用代數(shù)規(guī)約描述服務(wù)組合的方法。該方法以現(xiàn)有服務(wù)的代數(shù)規(guī)約為基礎(chǔ)，用代數(shù)規(guī)約形式化地、抽象地定義服務(wù)組合的實現(xiàn)，并進一步用代數(shù)規(guī)約定義組合服務(wù)對外提供的抽象接口和功能語義，從而形成了由實現(xiàn)規(guī)約和抽象規(guī)約組成的服務(wù)組合代數(shù)規(guī)約的雙元結(jié)構(gòu)。在雙元結(jié)構(gòu)的基礎(chǔ)上，進一步定義了服務(wù)組合實現(xiàn)規(guī)約和抽象規(guī)約之間必須滿足的“實現(xiàn)”關(guān)系。為了支持該方法的實現(xiàn)，本文擴展了面向服務(wù)代數(shù)規(guī)約語言SOFIA，提出了規(guī)約包機制，將定義一個服務(wù)系統(tǒng)的眾多規(guī)約單元封裝在一個規(guī)約包中，形成一個命名空間，增強了代數(shù)規(guī)約的重用性和可組合性。

本文第2節(jié)介紹代數(shù)規(guī)約的基本概念；第3節(jié)定義代數(shù)規(guī)約的規(guī)約包機制，討論如何應(yīng)用代數(shù)規(guī)約描述服務(wù)組合，并定義代數(shù)規(guī)約之間的實現(xiàn)關(guān)系；第4節(jié)結(jié)合實例介紹服務(wù)組合描述機制；第5節(jié)分析所提描述機制的一些特性；第6節(jié)討論本研究的一些相關(guān)工作；第7節(jié)展望未來的工作。

2 軟件系統(tǒng)的代數(shù)規(guī)約

一個面向服務(wù)的系統(tǒng)可以看成一組相互關(guān)聯(lián)的軟件實體的集合，每個軟件實體可以是抽象數(shù)據(jù)類型、類、構(gòu)件、服務(wù)或服務(wù)組合等，用來表示現(xiàn)實世界中的物理對象、設(shè)備、數(shù)據(jù)、抽象概念或商業(yè)過程等[10]。在面向服務(wù)系統(tǒng)的代數(shù)規(guī)約中，每個軟件實體可以用一個規(guī)約單元來描述，規(guī)約單元也稱為類子。類子之間有使用和擴展兩種關(guān)系，類似于面向?qū)ο笾械年P(guān)聯(lián)和繼承關(guān)系，記為?和?。通過這兩種關(guān)系可從已有規(guī)約單元構(gòu)造新的規(guī)約單元。一個結(jié)構(gòu)良好的代數(shù)規(guī)約將系統(tǒng)中每個軟件單元及相關(guān)概念和實體都抽象為相應(yīng)的規(guī)約單元，并且實體之間的關(guān)系對應(yīng)成規(guī)約單元之間的關(guān)系。

2.1 代數(shù)規(guī)約的基調(diào)

定義1(系統(tǒng)基調(diào)(System Signature)) 軟件系統(tǒng)的基調(diào)由有序?qū)?S,Σ)表示，其中，

(1)S=(St,?,?)，其中St是類子的有限集；?是集合St上的使用關(guān)系，s1?s2表示類子s1使用類子s2；?是集合St上的擴展關(guān)系，s1?s2表示類子s1擴展類子s2。

(2)Σ={Σs|s∈St}是所有單元基調(diào)Σs的集合。

2.2 代數(shù)規(guī)約的公理

令(S,Σ)為系統(tǒng)基調(diào)，定義Vs為類型為s的變量集，其中s∈St。假設(shè)ss1,s2,…,sn,s′，其中ss′表示s?s′或s=s′。

定義3(s-項(s-term)) 類子s的項記為s-項，其遞歸定義如下：

(1)類型為w的s′-項τ是類型為w的s-項；

(2)對所有v∈Vs′，v是類型為s′的s-項；

(3)對所有類型為s1,…,sn的s-項τ1,…,τn，〈τ1,…,τn〉是類型為(s1，…，sn)的s-項；

(4)對所有類型為(s1,…,sn)的s-項τ，τ#i,1≤i≤n，是類型為si的s-項；

(5)對所有φs:w→w′，φ(τ)是類型為w′的s-項，其中τ是類型為w的s-項。

定義4(等式(Equation)) 條件等式e是一個三元組(τ,τ′,C)，其中τ和τ′是類型相同的s-項，C={(ci,di)|0≤i≤n}是條件集合，其中當i=0,1,…,n時，ci和di為類型相同的s-項。條件等式e=(τ,τ′,C)可以表示為(τ=τ′,C)，其語義是當C中所有條件ci=di(0≤i≤n)成立時，有τ=τ′。

定義5(公理集(Axiom Set)) 定義類子s上的公理集Axs是s中公理ax的有限集，公理ax是二元組(V,e)，e為條件等式，V={vs′|ss′}，vs′是公理e中的類型為s′的變量，集合V可為空。

定義6(系統(tǒng)規(guī)約(System Specification)) 系統(tǒng)規(guī)約用三元組(S,Σ,Ax)表示，其中(S,Σ)是系統(tǒng)基調(diào)，Ax={Axs|s∈St}是公理集Axs的有限集。

為提高代數(shù)規(guī)約的模塊化特性，在使用代數(shù)規(guī)約語言時，系統(tǒng)規(guī)約往往分解成一組規(guī)約單元，規(guī)約單元定義如下：

定義7(規(guī)約單元(Specification Unit)) 類子sn的規(guī)約單元是一個三元組(s,Σsn,Axsn)，其中，

(1)s=(sn,sn?,sn?)，sn是規(guī)約單元名，也稱類子名，sn?是sn上的使用關(guān)系集合；sn?是sn上的擴展關(guān)系集合；

(2)Σsn是類子sn的單元基調(diào)；

(3)Axsn是定義在類子sn上的有限公理集。

2.3 代數(shù)規(guī)約的語義

定義8(代數(shù)(Algebra)) 給定系統(tǒng)基調(diào)(S,Σ)，一個(S,Σ)代數(shù)A表示為(A,F)，其中，

(1)A={As|s∈St}是由s索引的載體集As組成的有限集；

定義9(代數(shù)中項的值(Evaluation of Terms in an Algebra)) 將項中的變量映射到A的賦值函數(shù)記為α。給定一個賦值函數(shù)α，(S,Σ)-代數(shù)A=(A,F)中項τ的值記作Evaα(τ)，其定義如下：

(1)Evaα(v)=α(v);

(2)Evaα(〈τ1,…,τn〉)=〈Evaα(τ1),…,Evaα(τn)〉;

(3)Evaα(τ#i)=ai,如果Evaα(τ)=〈a1,…,an〉,1≤i≤n;

(4)Evaα(φ(τ))=fA,φ(Evaα(τ))。

定義10(滿足性(Satisfaction)) 令ax是公理(V,e),e為條件等式τ=τ′，C,其中C={(ci,di)|0≤i≤n}。若對所有V的賦值函數(shù)α，當Evaα(ci)=Evaα(di),i=1,2,…,n成立時，有Evaα(τ)=Evaα(τ′)，則稱(S,Σ)-代數(shù)A=(A,F)滿足公理ax，記為A|=ax。令規(guī)約ε=(S,Σ,Ax)，若(S,Σ)-代數(shù)A=(A,F)滿足Ax中所有公理ax，則稱代數(shù)A滿足規(guī)約ε，記作A|=ε。

3 服務(wù)組合的代數(shù)規(guī)約方法

本節(jié)討論如何應(yīng)用代數(shù)規(guī)約方法描述服務(wù)的組合。首先引入“規(guī)約包”的概念，將一個服務(wù)的規(guī)約封裝在一個包中，以便對服務(wù)進行組合。

3.1 規(guī)約包

一個系統(tǒng)的代數(shù)規(guī)約通常包含許多規(guī)約單元，給人們書寫和理解規(guī)約帶來不便，也為代數(shù)規(guī)約的重用和組合帶來不便。為此，本文提出規(guī)約包機制，將面向服務(wù)系統(tǒng)的代數(shù)規(guī)約拆分封裝成若干個包，將關(guān)系較為密切的類子放在同一包中。一個包可以引用其他包。通過引用其它包，包中類子可以使用被引用包中的類子。令P、Q為兩個包，用P?Q表示包P引用包Q。包機制有以下特點：

(1) 同一包中的類子名不同，不同包中的類子名可以相同，因此包可以避免類子命名沖突；

(2) 關(guān)系緊密的類子放在同一包中，進一步增強了代數(shù)規(guī)約模塊化特性；

(3) 通過引用其他包,可以提高代數(shù)規(guī)約的重用性。

假設(shè)面向服務(wù)系統(tǒng)的代數(shù)規(guī)約是規(guī)約單元集合{U1,…,Un}，n>0,將關(guān)系密切的規(guī)約單元構(gòu)建為一個包，則系統(tǒng)規(guī)約劃分為包集合{P1,…,Pl},l>0，且

①對于任意Pi,1≤i≤l,Pi≠?；

③Pi∩Pj=?；

④若Pj?Pi,則允許Ub?Ua,其中Ub∈Pj,Ua∈Pi。

一個包P由一系列規(guī)約單元U1,…,Uk組成，有一個唯一的名稱IdP，并給出所引用的包P1,…,Pn的名稱IdP1,…,IdPn。即包是一個三元組P=(IdP,{IdP1,…,IdPn},{U1,…,Uk})。

定義11(包的語義(Semantics of Package)) 包P=(IdP,{IdP1,…,IdPn},{U1,…,Uk})的語義是一個規(guī)約(SP,ΣP,AxP)，其定義如下：

如果包P不引用任何其它包，即P=(IdP,{},{U1,…,Uk})，則：

(1)SP=({s1,…,sk},?P,?P),si是規(guī)約單元Ui的類子名，?P和?P分別是規(guī)約單元U1,…,Uk之間的使用和擴展關(guān)系；

(2)ΣP={Σs|s∈{s1,…,sk}}；

(3)AxP={Axs|s∈{s1,…,sk}}。

如果包P引用P1,…,Pn,n>0，令(Si,Σi,Axi)為包Pi所定義的規(guī)約，則：

□

假定服務(wù)CS需要通過其他調(diào)用服務(wù)S1,…,Sn(n>1)以實現(xiàn)其功能，即CS是由服務(wù)S1,…,Sn組合而成。服務(wù)CS可以用兩種不同的代數(shù)規(guī)約來定義：

(1)用代數(shù)規(guī)約抽象地定義服務(wù)的用戶接口和功能，稱這樣的代數(shù)規(guī)約為服務(wù)的抽象規(guī)約；

(2)用代數(shù)規(guī)約定義該服務(wù)由哪些其他服務(wù)組成，描述每個向用戶提供的服務(wù)如何轉(zhuǎn)化為對其他服務(wù)的調(diào)用等實現(xiàn)方式，如同用代數(shù)規(guī)約描述如何用已有的數(shù)據(jù)類型實現(xiàn)新的數(shù)據(jù)類型，稱這樣的代數(shù)規(guī)約為服務(wù)的實現(xiàn)規(guī)約。

服務(wù)組合的抽象規(guī)約描述服務(wù)組合所提供的抽象功能，描述用戶對所期待服務(wù)的功能需求，不涉及服務(wù)組合的具體實現(xiàn)細節(jié)，而服務(wù)組合的實現(xiàn)規(guī)約則描述組合服務(wù)CS如何調(diào)用其他服務(wù)S1,…,Sn來實現(xiàn)其功能。由此可見，一個完整的服務(wù)組合代數(shù)規(guī)約應(yīng)該包含三個層次：組合抽象層、組合實現(xiàn)層和被調(diào)用服務(wù)層。

規(guī)約語言的包機制可以有效地支持這樣的規(guī)約結(jié)構(gòu)。如圖1所示，可以將被調(diào)用服務(wù)的代數(shù)規(guī)約放在相應(yīng)包中，組合服務(wù)的抽象規(guī)約放在一個包(或幾個包)中，組合服務(wù)的實現(xiàn)規(guī)約放在另一個(或幾個包中)且申明引用被調(diào)用服務(wù)規(guī)約的包。圖1中包PIMP為組合服務(wù)CS的實現(xiàn)規(guī)約，被調(diào)用服務(wù)S1,…,Sn的代數(shù)規(guī)約分別定義在包PS1,…,PSn中，且PIMP?PS1,…,PSn，組合服務(wù)CS的抽象規(guī)約定義在包PABS中。

Figure 1 Algebraic specifications of web service composition圖1 服務(wù)組合代數(shù)規(guī)約的結(jié)構(gòu)

由包的語義定義可知,抽象規(guī)約包PABS相當于一個系統(tǒng)規(guī)約(ABS,ΣABS,AxABS)，其中，

(1)ABS=〈Abs,Abs?,Abs?〉，Abs是抽象組合服務(wù)類子的集合，Abs?和Abs?分別表示Abs上的使用和擴展關(guān)系；

(2)基調(diào)ΣABS描述組合服務(wù)的抽象接口；

(3)公理集AxABS描述ΣABS中服務(wù)操作的語義，需要注意的是，AxABS中的公理并不描述組合服務(wù)如何調(diào)用其他服務(wù)，而是將組合服務(wù)看成一個原子服務(wù)，描述其應(yīng)當滿足的特性。

實現(xiàn)規(guī)約包也是一個系統(tǒng)規(guī)約三元組(IMP,ΣIMP,AxIMP)，其中，

(1)IMP=〈Imp,Imp?,Imp?〉，Imp是組合實現(xiàn)中所涉及的類子名的集合，Imp?和Imp?為這些類子的使用和擴展關(guān)系。對于一個正確的實現(xiàn)規(guī)約，要求Abs?Imp，并且如果類子s是一個被組合的服務(wù)，s∈Imp。

(2)ΣIMP是所實現(xiàn)服務(wù)的接口。作為一個正確的實現(xiàn)，要求抽象規(guī)約中定義的服務(wù)操作都被實現(xiàn)了，即ΣABS?ΣIMP。

(3)公理集AxIMP中公理ax=(V,e)，描述如何通過調(diào)用其他服務(wù)來實現(xiàn)所需的服務(wù)操作。如果這些公理所描述的實現(xiàn)是正確的，那么應(yīng)該能保證那些在抽象規(guī)約中定義服務(wù)需求的公理是成立的。因此，要求能夠從這些公理以及被組合的服務(wù)規(guī)約公理推導出抽象規(guī)約中的公理。

根據(jù)如上分析，下一節(jié)定義代數(shù)規(guī)約之間的實現(xiàn)關(guān)系。

3.2 代數(shù)規(guī)約之間的實現(xiàn)關(guān)系

定義12(實現(xiàn)關(guān)系(Implementation Relation)) 令CSIMP=(S,Σ,Ax)和CSABS=(S′,Σ′,Ax′)分別為兩個代數(shù)系統(tǒng)規(guī)約。CSIMP是CSABS的正確實現(xiàn)，表示為CSIMP?CSABS,如果下述三個條件成立：

(1)St′?St；

(2)Σ′?Σ；

上述定義中，條件(1)要求所有在抽象規(guī)約中定義的軟件實體都在實現(xiàn)規(guī)約中實現(xiàn)了，條件(2)要求抽象規(guī)約中的操作都在實現(xiàn)規(guī)約中實現(xiàn)了，條件(3)要求抽象規(guī)約所具有的服務(wù)特性都被實現(xiàn)規(guī)約滿足了。因此，CSIMP正確地實現(xiàn)了CSABS所規(guī)約的系統(tǒng)。

定義13(模型(Model)) 給定代數(shù)系統(tǒng)規(guī)約ε=(S,Σ,Ax)，一個代數(shù)A是(S,Σ,Ax)的模型，如果A存在一個子代數(shù)A′滿足條件：(1)A′是一個(S,Σ)代數(shù);(2)A′|=ε，即A′滿足公理Ax。用Mod(ε)表示規(guī)約ε的模型的集合。

由模型的概念及代數(shù)規(guī)約的語義定義易證明下面的定理為真,證明從略.

定理1說明，如果一個組合服務(wù)系統(tǒng)滿足實現(xiàn)規(guī)約且實現(xiàn)規(guī)約相對于抽象規(guī)約是正確的，那么該組合服務(wù)系統(tǒng)一定滿足抽象規(guī)約，也就是一個相對于抽象規(guī)約的正確實現(xiàn)。

4 實例

本節(jié)以訂票組合服務(wù)TravelS為例，說明用代數(shù)規(guī)約語言SOFIA描述組合服務(wù)的方法。

該服務(wù)根據(jù)服務(wù)請求中包含的雇員信息和旅行信息，返回機票價格較低的訂票信息。它由如下服務(wù)組合而成：(1)雇員狀態(tài)服務(wù)EmployeeInfoS，根據(jù)雇員的姓名和員工號，提供雇員的職位等基本信息，并提供雇員所允許的旅行倉位(如經(jīng)濟艙、商務(wù)艙或頭等艙等)；(2)美國航空公司和達美航空公司提供的機票查詢服務(wù)AAFlightTicketS和DAFlightTicketS。訂票組合服務(wù)TravelS比較兩者的機票價格，返回適合旅行者身份的價格較低的訂票信息。

4.1 代數(shù)規(guī)約的總體結(jié)構(gòu)

三個被組合服務(wù)EmployeeInfoS、AAFlightTicketS、DAFlightTicketS的代數(shù)規(guī)約分別封裝在三個包中，組合服務(wù)的實現(xiàn)規(guī)約和抽象規(guī)約分別封裝在TravelSImp包和TravelS包中。此外,包AirTravel包含了機票服務(wù)有關(guān)的公共概念。包之間的引用關(guān)系如圖2所示。

Figure 2 Algebraic specifications of TravelS圖2 訂票組合服務(wù)代數(shù)規(guī)約的結(jié)構(gòu)

4.2 被組合服務(wù)的規(guī)約

下面是AAFlightTicketS的代數(shù)規(guī)約。

package AAFlightTicketS;

import AirTravel;

spec AAFlightTicketS;

uses TravelClass,FlightReq,Flight;

operation

ticketReq(TravelClass,FlightReq):Flight;

axiom

for allaa:AAFlightTicketS,tc:travelClass,f:FlightReq that

aa.ticketReq(tc,f).class=tc;

(1)

aa.ticketReq(tc,f).leavingFrom=f.leavingFrom;

aa.ticketReq(tc,f).destination=f.destination;

aa.ticketReq(tc,f).departDateTime.date=f.departDate;

(2)

aa.ticketReq(tc,f).returnDateTime.date=f.returnDate;

end

end

end

DAFlightTicketS的規(guī)約包類似，故省略。因篇幅限制，也略去EmployeeInfoS和AirTravel規(guī)約包的細節(jié)。

4.3 服務(wù)組合的抽象規(guī)約

訂票服務(wù)的抽象規(guī)約如下:

package TravelS;

import EmployeeInfoS,AAFlightTicketS,DAFlightTicketS;

spec TravelS;

uses Employee,FlightReq,Flight,EmployeeInfoS,AAFlightTicketS,DAFlightTicketS;

operation

travelReq(Employee,FlightReq):Flight;

axiom

for alle:Employee,f:FlightReq,ts:TravelS,es:EmployeeInfoS,aa:AAFlightTicketS,da:DAFlightTicketS

that

ts.travelReq(e,f).departDateTime.date=f.departDate;

(3)

ts.travelReq(e,f).returnDateTime.date=f.returnDate;

(4)

ts.travelReq(e,f).destination=f.destination;

(5)

ts.travelReq(e,f).leavingFrom=f.leavingFrom;

(6)

letc=es.empInfoReq(e) in

ts.travelReq(e,f).class=c;

(7)

ts.travelReq(e,f).price=min(aa.ticketReq(c,f).price,da.ticketReq(c,f).price);

(8)

end

end

end

end

訂票服務(wù)抽象規(guī)約單元TravelS定義了一個服務(wù)操作travelReq，用戶提供員工信息和旅行信息，服務(wù)返回與員工身份相符的旅行機票信息。公理(3)～公理(6)要求服務(wù)提供的機票信息的出發(fā)日期、返回日期、目的地和出發(fā)地與服務(wù)請求中的相應(yīng)信息是吻合的。公理(7)要求服務(wù)返回的機票的等級與旅行者的身份一致。公理(8)要求機票的價格是兩家航空公司相應(yīng)票價中的較低者。

4.4 組合實現(xiàn)的規(guī)約

訂票服務(wù)的實現(xiàn)規(guī)約如下:

package TravelSImp;

import EmployeeInfoS,AAFlightTicketS,DAFlightTicketS;

spec TravelS;

uses Employee,FlightReq,Flight,EmployeeInfoS,AAFlightTicketS,DAFlightTicketS;

attr

empInfoS:EmployeeInfoS;

aaTicketS:AAFlightTicketS;

daTicketS:DAFlightTicketS;

operation

travelReq(Employee,FlightReq):Flight;

axiom

for allts:TravelS,e:Employee,f:FlightReq that

let

c=ts.empInfoS.empInfoReq(e);

aaTicket=ts.aaTicketS.ticketReq(c,f);

(9)

daTicket=ts.daTicketS.ticketReq(c,f);

in

ts.travelReq(e,f)=aaTicket,ifaaTicket.price

(10)

ts.travelReq(e,f)=daTicket,ifaaTicket.price>=daTicket.price;

(11)

end

end

end

end

上述規(guī)約說明TravelS包含三個服務(wù)作為其成分：empInfoS是EmployeeInfoS服務(wù)，aaTicketS是AAFlightTicketS服務(wù)，daTicketS是DAFlightTicketS。其中公理(10)規(guī)定當AAFlightTicketS服務(wù)返回的票價低于DAFlightTicketS服務(wù)返回的票價時，選擇美聯(lián)航空公司的機票。公理(11)規(guī)定當AAFlightTicketS服務(wù)返回的票價等于或高于DAFlightTicketS服務(wù)返回的票價時，選擇達美航空公司的機票。值得注意的是，抽象規(guī)約沒有指定當兩家航空公司的票價一樣時選擇哪個。因此，實現(xiàn)規(guī)約和抽象規(guī)約并不完全一樣。

4.5 證明實現(xiàn)關(guān)系

本節(jié)證明TravelS的實現(xiàn)規(guī)約正確實現(xiàn)了其抽象規(guī)約。首先，TravelS規(guī)約包的類子集合與TravelSImp包的類子集合完全相同。其次，TravelS在抽象規(guī)約包TravelS中說明的操作是在TravelSImp規(guī)約包中說明的操作的子集，這是因為在TravelSImp規(guī)約包中比TravelS包中多了三個觀察操作：empInfoS:EmployeeInfoS，aaTicketS:AAFlightTicketS，daTicketS:DAFlightTicketS。因此，實現(xiàn)關(guān)系的條件(1)和(2)均滿足。下面證明條件(3)也滿足。

(1)證明抽象規(guī)約包TravelS中的公理(3)成立。

由實現(xiàn)規(guī)約包TravelSImp中的公理(9)和公理(10)可知，當aaTicket.price

ts.travelReq(e,f).departDateTime.date=aaTicket.departDateTime.date=ts.aaTicketS.ticketReq(c,f).departDateTime.date

又由被調(diào)用服務(wù)類子AAFlightTicketS中公理(2)可知

ts.travelReq(e,f).departDateTime.date=ts.aaTicketS.ticketReq(c,f).departDateTime.date=f.departDate

同理可證，當aaTicket.price>=daTicket.price時，有：

ts.travelReq(e,f).deparDateTime.date=ts.daTicketS.ticketReq(c,f).departDateTime.date=f.departDate

因此，TravelS包中的公理(3)成立。

類似地，可以證明抽象規(guī)約包中的公理(4)～公理(6)成立。

(2)證明抽象規(guī)約包TravelS中的公理(7)成立。

由實現(xiàn)規(guī)約包TravelSImp的公理(9)和公理(10)可知，當aaTicket.price

ts.travelReq(e,f).class=aaTicket.class=ts.aaTicketS.ticketReq(c,f).class

其中c=ts.empInfoS.empInfoReq(e)。

又由AAFlightTicketS規(guī)約中的公理(1)可知

ts.travelReq(e,f).class=ts.aaTicketS.ticketReq(c,f).class=c

同理可證，當aaTicket.price>=daTicket.price時，有

ts.travelReq(e,f).class=ts.daTicketS.ticketReq(c,f).class=c

因此，抽象規(guī)約包TravelS中的公理(7)成立。

(3)證明抽象規(guī)約包TravelS中的公理(8)成立。

由實現(xiàn)規(guī)約包TravelSImp中的公理(9)和公理(10)可知，當aaTicket.price

ts.travelReq(e,f).price=aaTicket.price=ts.aaTicketS.ticketReq(c,f).price

當aaTicket.price>=daTicket.price時，有

ts.travelReq(e,f).price=daTicket.price=ts.daTicketS.ticketReq(c,f).price

因此，抽象規(guī)約包TravelS中的公理(8)成立。

綜合上述結(jié)果，由定義12,TravelSImp是TravelS的一個正確實現(xiàn)。

□

5 討論

本文提出的服務(wù)組合的代數(shù)規(guī)約方法具有如下特性。

(1)抽象性：SOFIA作為一種代數(shù)規(guī)約語言，將服務(wù)系統(tǒng)中的實體都抽象為規(guī)約單元。在描述服務(wù)組合時，既可以給出組合服務(wù)的抽象描述，也可以描述其組合的實現(xiàn)。由于語言的抽象化特點，調(diào)用其他組合服務(wù)時，往往只需考慮被調(diào)用服務(wù)的抽象接口，而不用考慮多層組合服務(wù)的嵌套。

(2)表達力：服務(wù)組合中，多個被調(diào)用服務(wù)之間的調(diào)用關(guān)系可能是順序、選擇或者循環(huán)調(diào)用，其中循環(huán)組合可由遞歸等式描述。SOFIA語言書寫順序和選擇服務(wù)調(diào)用的公理形式如下。

①順序組合。

順序組合是指多個服務(wù)按順序依次執(zhí)行，前一個服務(wù)的輸出結(jié)果作為后一個服務(wù)的輸入?yún)?shù)。假定φ是組合服務(wù)CS的一個操作，其輸入的類子為R。如果服務(wù)操作φ的實現(xiàn)是依次調(diào)用服務(wù)sa的操作φ1和服務(wù)sb中的操作φ2，則公理的形式如下：

For allsc:CS,x:R that

sc.(x)=sc.sb.(sc.sa.(x));

End

②選擇組合。

如果組合服務(wù)的操作φ根據(jù)條件選擇要執(zhí)行的服務(wù)，例如當條件Con為真時，調(diào)用服務(wù)sa中操作φ1，否則調(diào)用服務(wù)sb中操作φ2，則公理的形式如下：

For allsc:SC,r:R that

sc.φ(r)=sc.sa.φ1(r),if Con;

sc.φ(r)=sc.sb.φ2(r),if not Con;

End

(3)可驗證性：若組合服務(wù)的抽象規(guī)約單元中的公理能夠由被調(diào)用服務(wù)規(guī)約的公理和組合實現(xiàn)規(guī)約中的公理證明得到，那么組合實現(xiàn)是正確的。上述訂購機票組合服務(wù)的例子說明，這樣的證明是可行的。

6 相關(guān)工作

目前，Web服務(wù)組合規(guī)范主要從工作流程的角度描述和定義參與服務(wù)組合的各個子服務(wù)之間的動態(tài)交互的邏輯順序，工業(yè)界廣泛采用的業(yè)務(wù)流程執(zhí)行規(guī)范BPEL(Business Process Execution Language)將服務(wù)組合調(diào)用動作視為一組活動，用控制流塊結(jié)構(gòu)組織這些活動，并提供服務(wù)組合的抽象行為和具體實現(xiàn)描述[16]，但這種方法缺乏形式化語義以及驗證機制來保證服務(wù)組合的質(zhì)量[17]。針對服務(wù)組合的可驗證性和可測試性這一問題，學者們基于Web服務(wù)組合規(guī)范建立形式化模型，以形式化方法定義和描述服務(wù)組合的各個子服務(wù)之間的動態(tài)交互，其中使用最多的三種形式化方法分別是有限自動機及其變體[18,19]、Petri網(wǎng)[20,21]和進程代數(shù)[22]。這些已有工作主要對服務(wù)和服務(wù)之間的交互行為建模，并支持組合的性質(zhì)如死鎖避免、數(shù)據(jù)類型一致性和動態(tài)行為匹配性的檢查和驗證。但是，這些方法著重關(guān)注服務(wù)組合調(diào)用行為的協(xié)調(diào)性，缺乏對服務(wù)功能的描述，因此難以支持對服務(wù)功能正確性的驗證和測試。

與上述三種形式化方法相比，代數(shù)規(guī)約[5]不僅能夠描述軟件行為，還能通過公理描述軟件功能。代數(shù)規(guī)約作為一種高度抽象的形式化方法，從20世紀70年代被提出發(fā)展至今，其理論基礎(chǔ)從初始代數(shù)發(fā)展到終代數(shù)、行為代數(shù)[7]和合代數(shù)[7 - 9]，描述對象從抽象數(shù)據(jù)類型擴展到并發(fā)系統(tǒng)、基于狀態(tài)的系統(tǒng)和軟件組件。在前期工作中，我們擴展了行為代數(shù)和合代數(shù)理論，提出設(shè)計并實現(xiàn)了面向服務(wù)系統(tǒng)的代數(shù)規(guī)約語言SOFIA[10]。對服務(wù)系統(tǒng)代數(shù)規(guī)約的實例研究表明，與其他形式化方法相比，代數(shù)規(guī)約具有表達力強、高度模塊化等特點，更適合描述服務(wù)系統(tǒng)[11 - 15]，但文獻中尚未見將代數(shù)規(guī)約技術(shù)用于描述服務(wù)組合的研究。本文在上述研究的基礎(chǔ)上，將包的概念引入到代數(shù)規(guī)約語言，進一步擴展了SOFIA語言，提高服務(wù)描述的模塊化特性，從而支持服務(wù)描述的重用和組合。包作為一個軟件語言設(shè)施已廣泛應(yīng)用于程序設(shè)計語言，但未見于代數(shù)規(guī)約語言。本文定義的代數(shù)規(guī)約之間的實現(xiàn)關(guān)系與傳統(tǒng)代數(shù)規(guī)約理論中的定義有所不同，傳統(tǒng)的定義要求兩個代數(shù)規(guī)約的基調(diào)完全相同[23]。但是，我們在描述組合服務(wù)的實例研究中發(fā)現(xiàn)，如同本文的例子所示，抽象規(guī)約和實現(xiàn)規(guī)約的基調(diào)可能不同，實現(xiàn)規(guī)約的基調(diào)可能包含額外的用于實現(xiàn)組合的操作，并可能使用抽象規(guī)約中無需指定的類子。相應(yīng)地，我們對規(guī)約的模型概念也作了修改。在定理1中我們證明了，對這些代數(shù)規(guī)約基本概念的修改保持了“實現(xiàn)規(guī)約的模型必須也是抽象規(guī)約的模型”這個重要性質(zhì)。本文給出的例子說明，證明實現(xiàn)規(guī)約與抽象規(guī)約之間的實現(xiàn)關(guān)系是可行的，為形式化驗證和測試服務(wù)組合描述的正確性奠定了基礎(chǔ)。

代數(shù)規(guī)約方法的一個主要特點是支持軟件測試的自動化，包括測試用例生成，測試執(zhí)行和測試結(jié)果正確性判斷，代表性的研究成果有：Bernot等[24]開發(fā)的測試過程程序的測試工具。針對面向?qū)ο筌浖?，Doong等[25]提出LOBAS規(guī)約語言并開發(fā)自動化測試工具ASTOOT，Hughe等[26]開發(fā)了DAISTISH。針對Java平臺軟件組件，Zhu等[14,15]提出CASOCC語言并開發(fā)CASCAT自動化測試工具。在前期工作中，我們設(shè)計并實現(xiàn)了以代數(shù)規(guī)約語言SOFIA為基礎(chǔ)的自動化測試工具，支持對單個服務(wù)進行自動化測試[11,12]。此外還提出了代數(shù)規(guī)約到語義本體的轉(zhuǎn)換方法[27]，并開發(fā)了轉(zhuǎn)換工具TrS2O[28]，將服務(wù)的代數(shù)規(guī)約轉(zhuǎn)換成本體語義描述，使得代數(shù)規(guī)約在機器可理解性和人工可讀性方面得到改善。

7 結(jié)束語

本文提出了基于代數(shù)規(guī)約的服務(wù)組合形式化規(guī)約方法，使驗證和測試服務(wù)組合的正確性成為可能。下一步的工作將進一步進行實例研究，總結(jié)服務(wù)組合的模式，設(shè)計并實現(xiàn)證明服務(wù)組合正確性的自動化推導工具，以及服務(wù)組合自動測試工具。

[1] Papazoglou M P,Heuvel W J.Service oriented architectures:Approaches,technologies and research issues[J].The VLDB Journal—The International Journal on Very Large Data Bases,2007,16(3):389-415.

[2] Bouguettaya A, Sheng Q Z, Daniel F.Web services foundations[M].New York:Springer,2014.

[3] Goguen J A,Thatcher J W,Wagner E G,et al.Initial algebra semantics and continuous algebras[J].Journal of the ACM (JACM),1977,24(1):68-95.

[4] Bartalos P,Bieliková M.Automatic dynamic web service composition:A survey and problem formalization[J].Computing and Informatics,2012,30(4):793-827.

[5] Charif Y,Sabouret N.An overview of semantic web services composition approaches[J].Electronic Notes in Theoretical Computer Science,2006,146(1):33-41.

[6] Goguen J,Malcolm G.A hidden agenda[J].Theoretical Computer Science,2000,245(1):55-101.

[7] Cirstea C.Coalgebra semantics for hidden algebra:Parameterised objects and inheritance[C]∥Proc of International Workshop on Algebraic Development Techniques,1997:174-189.

[8] Rutten J J M M.Universal coalgebra:A theory of systems[J].Theoretical Computer Science,2000,249(1):3-80.

[9] Bonchi F,Montanari U.A coalgebraic theory of reactive systems[J].Electronic Notes in Theoretical Computer Science,2008,209:201-215.

[10] Liu D,Zhu H,Bayley I.SOFIA:An algebraic specification language for developing services[C]∥Proc of 2014 IEEE 8th International Symposium on Service Oriented System Engineering (SOSE),2014:70-75.

[11] Liu D,Liu Y,Zhang X,et al.Automated testing of web services based on algebraic specifications[C]∥Proc of the International Workshop on Service-Oriented System Engineering,2015:143-152.

[12] Liu D,Wu X,Zhang X,et al.Monic testing of web services based on algebraic specifications[C]∥Proc of Service-Oriented System Engineering (SOSE),2016:24-33.

[13] Chen H Y,Tse T H,Chen T Y.TACCLE:A methodology for object-oriented software testing at the class and cluster levels[J].ACM Transactions on Software Engineering and Methodology (TOSEM),2001,10(1):56-109.

[14] Kong L,Zhu H,Zhou B.Automated testing EJB components based on algebraic specifications[C]∥Proc of the 31st Annual International Computer Software and Applications Conference(COMPSAC 2007),2007:717-722.

[15] Yu B, Kong L,Zhang Y,et al.Testing java components based on algebraic specifications[C]∥Proc of 2008 1st International Conference on Software Testing,Verification,and Validation,2008:190-199.

[16] Weske M.Business process management architectures[M]∥Business Process Management.Berlin:Springer Berlin Heidelberg,2012:333-371.

[17] Aalst W M P V D,Dumas M,Hofstede A H M T.Web service composition languages:Old wine in new bottles?[C]∥Proc of the 29th Conference on Euromicro,2003:298-305.

[18] Keum C S,Kang S,Ko I Y,et al.Generating test cases for web services using extended finite state machine[C]∥Proc of the 18th International Conference on Testing of Communicating Systems,2006:103-117.

[19] Ramollari E,Kourtesis D,Dranidis D,et al.Leveraging semantic web service descriptions for validation by automated functional testing[C]∥Proc of European Semantic Web Conference on the Semantic Web:Research and Applications,2009:593-607.

[20] Zhu H,He X.A methodology of testing high-level Petri nets[J].Information & Software Technology,2002,44(8):473-489.

[21] Xu D.A tool for automated test code generation from high-level Petri nets[C]∥Proc of International Conference on Applications and Theory of Petri Nets-,2011:308-317.

[22] Frantzen L, Huerta M D L N, Kis Z D,et al.On-the-fly model-based testing of web services with Jambition[C]∥Proc of Web Services and Formal Methods,2009:143-157.

[23] Sannella D,Tarlecki A.Foundations of algebraic specification and formal software development[M].Berlin:Springer,2012.

[24] Bernot G,Gaudel M C,Marre B.Software testing based on formal specifications:A theory and a tool[J].Software Engineering Journal,2010,6(6):387-405.

[25] Doong R K,Frankl P G.The ASTOOT approach to testing object-oriented programs[J].ACM Transactions on Software Engineering and Methodology(TOSEM),1994,32(2):101-130.

[26] Hughes M,Stotts D.Daistish:Systematic algebraic testing for OO programs in the presence of side-effects[C]∥Proc of the 1996 ACM SIGSOFT International Symposium on Software Testing and Analysis,1996:53-61.

[27] Liu D,Zhu H,Bayley I.From algebraic specification to ontological description of service semantics[C]∥Proc of IEEE,International Conference on Web Services,2013:579-586.

[28] Liu D,Zhu H,Bayley I.Transformation of algebraic specifications into ontological semantic descriptions of web services[J].International Journal of Services Computing,2014,2(1):58-71.