包 力

（內(nèi)蒙古工業(yè)大學(xué)，呼和浩特 010080）

隨著現(xiàn)代經(jīng)濟(jì)社會(huì)全面進(jìn)入服務(wù)經(jīng)濟(jì)時(shí)代，現(xiàn)代服務(wù)業(yè)已經(jīng)成為了現(xiàn)代經(jīng)濟(jì)社會(huì)持續(xù)發(fā)展的新動(dòng)力[1]。Web 服務(wù)即用戶根據(jù)實(shí)際的生產(chǎn)需求可彈性獲取，由云提供商提供的、可擴(kuò)展的計(jì)算資源。然而，單一Web服務(wù)只能提供有限的計(jì)算資源。比如，糖尿病患者需要關(guān)于如何控制餐后血糖進(jìn)行信息咨詢，這樣的信息咨詢將在減緩病情發(fā)展方面發(fā)揮積極作用。影響糖尿病患者餐后血糖的因素有很多，比如胰島素劑量、每餐熱量攝入、日常鍛煉等常見(jiàn)因素都可能影響餐后血糖。如果糖尿病患者想預(yù)測(cè)并干預(yù)餐后血糖，就需要這些方面的數(shù)據(jù)?？捎糜谑占嚓P(guān)數(shù)據(jù)的常見(jiàn)軟件服務(wù)有記步服務(wù)、熱量攝入記錄服務(wù)、醫(yī)療數(shù)據(jù)分析服務(wù)等分屬不同的云平臺(tái)，顯然，單一的軟件服務(wù)無(wú)法滿足上述需求，需要組合血糖控制咨詢服務(wù)（負(fù)責(zé)回答患者問(wèn)題并提供建議）、記步服務(wù)（負(fù)責(zé)記錄患者燃燒的熱量）及數(shù)據(jù)分析服務(wù)（負(fù)責(zé)處理和分析數(shù)據(jù)）。由這些服務(wù)構(gòu)成的服務(wù)組合，將為糖尿病患者提供關(guān)于血糖方面的信息咨詢。Web 服務(wù)組合（以下簡(jiǎn)稱“服務(wù)組合”）就是根據(jù)客戶需求的變化動(dòng)態(tài)增加或釋放所需的資源，將跨越不同服務(wù)提供商的Web 服務(wù)進(jìn)行整合，為用戶提供增值服務(wù)并實(shí)現(xiàn)更加復(fù)雜的功能。服務(wù)組合旨在有效選擇、整合來(lái)自不同云平臺(tái)的服務(wù)，將跨越云平臺(tái)邊界的服務(wù)進(jìn)行深度整合并實(shí)現(xiàn)其功能的擴(kuò)展與創(chuàng)新，使得這些服務(wù)協(xié)同工作，為用戶提供更加全面、更高質(zhì)量的功能?？缭品?wù)組合技術(shù)將為現(xiàn)代服務(wù)業(yè)的發(fā)展注入新動(dòng)力。

本文組織如下：第1 節(jié)介紹相關(guān)研究工作，第2 節(jié)介紹Web 服務(wù)交互模型，第3 節(jié)給出Web 服務(wù)交互模型的行為語(yǔ)義，第4 節(jié)提供了一個(gè)案例研究，最后是結(jié)論和展望。

1 相關(guān)研究

Web 服務(wù)組合（Web Service Company）是以業(yè)務(wù)流程和規(guī)則為基礎(chǔ)，將若干組件式服務(wù)組合成粒度更大的、服務(wù)的過(guò)程。服務(wù)組合方法大體上可分為基于業(yè)務(wù)流程驅(qū)動(dòng)的服務(wù)組合和基于即時(shí)任務(wù)解決的服務(wù)組合兩大類。一是基于業(yè)務(wù)流程驅(qū)動(dòng)的服務(wù)組合，二是基于即時(shí)任務(wù)解決的服務(wù)組合。

在面向Web 服務(wù)的自動(dòng)化組合方面有許多研究成果。文獻(xiàn)[2]研究了云制造中的服務(wù)重構(gòu)與供需銜接問(wèn)題，提出了面向云制造的自主性導(dǎo)向（autonomy-oriented）服務(wù)組合與優(yōu)化選擇方法。為了提高服務(wù)選擇的準(zhǔn)確性，研究者給出了帶有波動(dòng)率分析功能的、基于模糊集的決策方法。針對(duì)利用語(yǔ)義web 服務(wù)發(fā)現(xiàn)機(jī)制發(fā)現(xiàn)并選擇最合適的候選服務(wù)問(wèn)題，文獻(xiàn)[3]給出一種由5 個(gè)階段構(gòu)成的多級(jí)工作流編排框架。該框架采用功能屬性描述候選服務(wù)的行為，并可滿足用戶目標(biāo)的動(dòng)態(tài)變化。文獻(xiàn)[4]提出了一種混合Web 服務(wù)自動(dòng)組合方法，旨在生成具有最佳端到端QoS 的基于語(yǔ)義輸入輸出的服務(wù)組合，并使參與組合的服務(wù)數(shù)量最小化。為了使開(kāi)發(fā)者能夠高效地進(jìn)行服務(wù)組合，文獻(xiàn)[5]給出了一種可視化的REST 服務(wù)建?？蚣埽摽蚣苡煽梢暬?wù)組合建模工具和服務(wù)開(kāi)發(fā)平臺(tái)組成。為了提高Web 服務(wù)組合測(cè)試用例的質(zhì)量并找出哪條路徑導(dǎo)致服務(wù)組合失敗的概率最大，文獻(xiàn)[6]采用啟發(fā)式測(cè)試用例生成法以獲得最優(yōu)測(cè)試路徑。

2 交互Web 服務(wù)網(wǎng)絡(luò)

2.1 Kahn 過(guò)程網(wǎng)絡(luò)

Kahn 過(guò)程網(wǎng)絡(luò)（KPN）[7]是一種基于數(shù)據(jù)流的計(jì)算模型，該模型的優(yōu)點(diǎn)之一是可以在分布式結(jié)構(gòu)上實(shí)現(xiàn)進(jìn)程的并發(fā)通信和執(zhí)行，這一特點(diǎn)使得KPN 非常適合于建模Web 服務(wù)交互行為。在KPN 模型中，并發(fā)過(guò)程使用節(jié)點(diǎn)表示，有序的數(shù)據(jù)序列使用弧表示（數(shù)據(jù)序列也稱為令牌）。進(jìn)程通過(guò)先進(jìn)先出的通道相互通信，在KPN 中，使用數(shù)據(jù)令牌隊(duì)列表示這些通道。啟動(dòng)FIFO通道的讀取操作需要通信通道中至少存在一個(gè)令牌。由于FIFO 通道的大小是無(wú)限的，因此寫入操作是非阻塞的。KPN 模型采用異步通信，并且KPN 計(jì)算的輸出結(jié)果與其執(zhí)行順序無(wú)關(guān)，即進(jìn)程并發(fā)過(guò)程中先執(zhí)行哪個(gè)進(jìn)程對(duì)計(jì)算結(jié)果不產(chǎn)生影響。

2.2 Web 服務(wù)交互網(wǎng)絡(luò)IWSN

在IWSN 模型中，Web 服務(wù)被建模為KPN 中的計(jì)算進(jìn)程，Web 服務(wù)組合被建模為進(jìn)程的并發(fā)自治網(wǎng)絡(luò)。進(jìn)程間通過(guò)先進(jìn)先出的通道進(jìn)行通信。網(wǎng)絡(luò)中的每個(gè)進(jìn)程都對(duì)消息序列進(jìn)行自主控制，并且每個(gè)進(jìn)程執(zhí)行的操作與其他進(jìn)程的操作并發(fā)執(zhí)行。對(duì)于單個(gè)進(jìn)程（服務(wù)），其行為建模為其執(zhí)行的操作。Trace（記錄）用于建模進(jìn)程之間的交互行為，IWSN 模型如圖1 所示。

圖1 Web 服務(wù)交互網(wǎng)絡(luò)

2.3 交互Web 服務(wù)網(wǎng)絡(luò)的定義

由于操作是Web 服務(wù)功能的基本單元，IWSN 中Web 服務(wù)調(diào)用被建模為操作的調(diào)用過(guò)程，這里使用集合Operation表示。IWSN 中，使用進(jìn)程（Process）建模服務(wù)順序執(zhí)行操作的集合，即Process集合中的一個(gè)元素是操作的線性串聯(lián)。如果一個(gè)操作op1的輸出消息是另一操作op2的輸入消息，那么在op1和op2之間存在對(duì)應(yīng)關(guān)系，這里引入二進(jìn)制關(guān)系Ro來(lái)表示這種類型的關(guān)系。在IWSN 中，符號(hào)T用來(lái)表示進(jìn)程（Web 服務(wù)）的交互記錄。

定義1（交互Web 服務(wù)網(wǎng)絡(luò)）。

一個(gè)交互Web 服務(wù)網(wǎng)絡(luò)是一個(gè)6-元組，在這里

Service是Web 服務(wù)的集合;

Process是進(jìn)程的集合;

Operation是操作的集合;

T表示操作序列的集合;

Message表示出入進(jìn)程的消息的集合;

Ro?Operation×Operation是Operation集合上的二元關(guān)系。

3 交互Web 服務(wù)網(wǎng)絡(luò)的形式化語(yǔ)義

本節(jié)給出Web 服務(wù)交互網(wǎng)絡(luò)的行為語(yǔ)義定義，該語(yǔ)義基于Pi-演算及其公理化操作語(yǔ)義[8]。行為語(yǔ)義由2 部分構(gòu)成，語(yǔ)義轉(zhuǎn)換域和轉(zhuǎn)換函數(shù)。首先引入Pi-演算作為語(yǔ)義轉(zhuǎn)換域，然后給出轉(zhuǎn)換函數(shù)定義和轉(zhuǎn)換算法，將IWSN 模型語(yǔ)義轉(zhuǎn)換為Pi-演算表達(dá)式。

設(shè)存在可數(shù)無(wú)限集N，在Pi-演算中進(jìn)程（Process）使用N中的元素P，Q，R……（大寫字母）表示，進(jìn)程執(zhí)行的動(dòng)作使用N中的元素u，v，w，x，y，z……（小寫字母）表示。Pi-演算表達(dá)式使用下面的語(yǔ)法構(gòu)造

式中：使用數(shù)字0 表示空進(jìn)程，空進(jìn)程已經(jīng)結(jié)束，不執(zhí)行動(dòng)作;符號(hào)∑表示非確定性選擇，例如，R+P表達(dá)式表示執(zhí)行進(jìn)程R或P中的一個(gè); 進(jìn)程順序執(zhí)行的表達(dá)式為cx.P，其中P是進(jìn)程，c是通道名，x是動(dòng)作名稱，cx.P從通道c讀入動(dòng)作x，然后執(zhí)行P；表達(dá)式P1|…|Pn表示并行執(zhí)行進(jìn)程P1，P2，…，Pn；表達(dá)式[x=y]P表示當(dāng)通道名稱x與通道名稱y相等時(shí)，進(jìn)程[x=y]P的行為與進(jìn)程P相同，否則[x=y]P為空進(jìn)程。

4 案例研究

4.1 車輛保養(yǎng)維修服務(wù)案例

本節(jié)通過(guò)汽車保養(yǎng)維修服務(wù)案例展示如何應(yīng)用IWSN 模型建模和驗(yàn)證Web 服務(wù)組合的案例，因?yàn)橹攸c(diǎn)建模的服務(wù)交互行為，所以服務(wù)組合涉及的其他方面的技術(shù)細(xì)節(jié)沒(méi)有建模。通過(guò)這個(gè)案例可以看出，即使相對(duì)簡(jiǎn)單的服務(wù)組合也會(huì)包含復(fù)雜的交互行為。

業(yè)務(wù)流程簡(jiǎn)介如下：汽車保養(yǎng)維修服務(wù)（Car Maintenance Providing Service）接受客戶服務(wù)（Client Service）的請(qǐng)求，并根據(jù)汽車零部件供應(yīng)商服務(wù)（Vehicle Parts Providing Service）和在線金融服務(wù)（On-line Financial Service）的響應(yīng)，檢查該請(qǐng)求是否能夠得到滿足。在這2個(gè)服務(wù)確認(rèn)后，其向客戶服務(wù)發(fā)送一個(gè)付款請(qǐng)求。在客戶支付了汽車維護(hù)費(fèi)用后，然后將確認(rèn)消息發(fā)送回客戶代理。部分消息的含義解釋介紹見(jiàn)表1（在每個(gè)含義解釋的末尾為每條消息定義了縮寫）。

表1 部分服務(wù)消息含義

下面是基于Pi-演算的單個(gè)Web 服務(wù)的行為及服務(wù)交互的描述（表達(dá)式中的! 符號(hào)表示發(fā)出消息）。

客戶服務(wù)Client 的行為描述：

Client = ! Request.Interactionloop1

Interactionloop1 = AskInfo.! Pro.Interactionloop1+（Refusal.Client + Accept.! Con.Client）

汽車保養(yǎng)維修服務(wù)的行為描述：

當(dāng)加載到3%rad(38.19 mm)循環(huán)時(shí)，在位移較大時(shí)，角鋼微微被掀起。當(dāng)加載到4%rad(50.92 mm)循環(huán)期間，接近位移極值時(shí)，角鋼被拉起但角鋼和梁翼緣為見(jiàn)明顯變形。

Car = Request.Interactionloop2

Interactionloop2 = ! AskInfo.ProvInfo.Interactionloop2 + ! GetPartInfo.PartInfo.Interactionloop2 + !GetPaymentInfo. PaymentInfo

Interactionloop2 +τ.（! Refusal.Tour + ! Accept.Con.Tour）

以下表達(dá)式分別是車輛零部件供應(yīng)商服務(wù)和在線金融服務(wù)的行為描述：

Vehicle = GetPartInfo. ! PartInfo.Vehicle

Financial=GetPaymentInfo.! PaymentInfo.Financial

汽車保養(yǎng)維修組合服務(wù)的行為描述：

其中，消息集合{GetPartInfo，PartInfo，GetPaymentInfo，PaymentInfo } 是一組內(nèi)部消息，需要使用符號(hào)τ 來(lái)表示發(fā)送和接收操作。

4.2 車輛保養(yǎng)維修服務(wù)的形式化驗(yàn)證

為了驗(yàn)證服務(wù)兼容性，首先需要給出觀察等價(jià)（Observational Equivalence）的定義。觀察等價(jià)的定義是判定2 個(gè)服務(wù)是否兼容的數(shù)學(xué)基礎(chǔ)，同時(shí)，觀察等價(jià)也可用于驗(yàn)證一個(gè)服務(wù)是否可以替代另一個(gè)服務(wù)。

定義2 弱遷移（Weak Transitions）。

如果q=q0→τq1→τ…→τqn，那么q?εq’，當(dāng)n≥0，其中，τ 外部不可見(jiàn)動(dòng)作的遷移標(biāo)簽；

如果q?εq’，那么q?τq’；

如果q?εq1→aq2?εq’，那么q?aq’（a≠τ）；

如果q?aq’，那么從q到q’是一個(gè)弱遷移。

定義3 觀察等價(jià)（Observational Equivalence）。

令R?Q×Q，那么當(dāng)關(guān)系R是一個(gè)弱等價(jià)，如果任何時(shí)候t1Rt2都存在如下遷移關(guān)系：

如果t1→at1’，即意味著存在某個(gè)t2’并且t2?at2’，從而t1’Rt2’；

如果t2→at2’，即意味著存在某個(gè)t1’并且t1?at1’，從而t1’Rt2’；

如果在遷移t1和t2上存在一個(gè)弱等價(jià)關(guān)系，即t1Rt2，那么t1和t2是觀察等價(jià)關(guān)系，或弱等價(jià)關(guān)系。

定義4 行為兼容（Behavior Compatibility）。

2 個(gè)服務(wù)p和q是行為兼容的，記作compatible（p，q），如果服務(wù)p與q觀察等價(jià)。

根據(jù)這個(gè)定義，當(dāng)服務(wù)發(fā)生交互時(shí)，外部觀察者不可能區(qū)分2 個(gè)過(guò)程p和q，并且2 個(gè)服務(wù)p和q行為兼容意味著其存在相反的行為記錄。在本案例中，雖然客戶端服務(wù)也被認(rèn)為是一個(gè)進(jìn)程，但是客戶端進(jìn)程不包括在Web 服務(wù)組合中。系統(tǒng)的設(shè)計(jì)目標(biāo)是按照業(yè)務(wù)流程生成需求規(guī)格，也就是開(kāi)發(fā)的系統(tǒng)需要滿足客戶的要求，即需要驗(yàn)證車輛保養(yǎng)維修服務(wù)是否滿足需求規(guī)格。因此，服務(wù)組合應(yīng)該與客戶端服務(wù)在行為上觀察等價(jià)?？蛻舴?wù)和車輛維修保養(yǎng)服務(wù)應(yīng)該有相反的行為?？蛻舳朔?wù)的相反行為是

消息集合{GetPart Info，PartInfo，GetPayment Info，Payment Info} 中定義的是外部不可見(jiàn)的內(nèi)部操作。此時(shí)，忽略ServiceSystem中的內(nèi)部操作。將得到了一個(gè)系統(tǒng)（這里使用表示），該系統(tǒng)與Reverse－Client觀察等價(jià)。

這里對(duì)汽車保養(yǎng)維修服務(wù)進(jìn)行可達(dá)性分析，通過(guò)可達(dá)性分析，可能會(huì)發(fā)現(xiàn)不正確的系統(tǒng)設(shè)計(jì)，如死鎖和關(guān)鍵功能不能滿足需求。使用分支時(shí)間邏輯計(jì)算樹(shù)邏輯（Computation Tree Logic，CTL）[9]來(lái)驗(yàn)證軟件系統(tǒng)是否具有預(yù)期屬性。首先定義一個(gè)邏輯公式來(lái)描述系統(tǒng)永遠(yuǎn)不應(yīng)該達(dá)到的狀態(tài)，并使用should_receive來(lái)表示這種狀態(tài)。對(duì)該狀態(tài)的解釋如下。

如果在有限數(shù)量（可能為0）的內(nèi)部執(zhí)行步驟之后，在客戶服務(wù)發(fā)送請(qǐng)求消息（Req）后，服務(wù)客戶一定會(huì)從汽車保養(yǎng)維修服務(wù)接收到響應(yīng)消息，則系統(tǒng)的should _receive值為true，使用CTL 描述的系統(tǒng)屬性

5 結(jié)論與展望

本文提出了一種基于Kahn 過(guò)程網(wǎng)絡(luò)的交互Web服務(wù)模型（IWSN），旨在解決Web 服務(wù)正確的交互問(wèn)題，同時(shí)保證Web 服務(wù)交互過(guò)程中的行為兼容性。在介紹Pi-演算定義的基礎(chǔ)上，給出了IWSN 模型的形式化語(yǔ)義，并給出了IWSN 模型語(yǔ)義轉(zhuǎn)換算法。在車輛保養(yǎng)維修服務(wù)案例中，應(yīng)用IWSN 模型描述了業(yè)務(wù)流程，并給出了服務(wù)行為兼容的定義。案例的實(shí)驗(yàn)結(jié)果證明了提出的方法是可行和適用的。

綜上所述，基于KPN 的交互Web 服務(wù)網(wǎng)絡(luò)具有并發(fā)通信機(jī)制、可組合性、可執(zhí)行性等特點(diǎn)，適合于對(duì)Web 服務(wù)組合過(guò)程中的服務(wù)交互進(jìn)行建模。我們未來(lái)的工作是實(shí)現(xiàn)Web 服務(wù)交互網(wǎng)絡(luò)的原型系統(tǒng)，為相關(guān)技術(shù)的市場(chǎng)推廣奠定基礎(chǔ)。