Web 服務(wù)交互過程建模與驗證研究

包 力

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

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

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

1 相關(guān)研究

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

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

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

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

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

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

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

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

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

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

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

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

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

Process是進程的集合;

Operation是操作的集合;

T表示操作序列的集合;

Message表示出入進程的消息的集合;

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

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

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

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

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

4 案例研究

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

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

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

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

下面是基于Pi-演算的單個Web 服務(wù)的行為及服務(wù)交互的描述（表達式中的! 符號表示發(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)時，在位移較大時，角鋼微微被掀起。當(dāng)加載到4%rad(50.92 mm)循環(huán)期間，接近位移極值時，角鋼被拉起但角鋼和梁翼緣為見明顯變形。

Car = Request.Interactionloop2

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

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

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

Vehicle = GetPartInfo. ! PartInfo.Vehicle

Financial=GetPaymentInfo.! PaymentInfo.Financial

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

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

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

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

定義2 弱遷移（Weak Transitions）。

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

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

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

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

定義3 觀察等價（Observational Equivalence）。

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

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

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

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

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

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

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

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

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

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

5 結(jié)論與展望

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

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