基于語義擴(kuò)展類型論的云服務(wù)替換性判定研究

王先清，黃昌勤，羅旋，聶瑞華，湯庸，梅曉勇

?

基于語義擴(kuò)展類型論的云服務(wù)替換性判定研究

王先清1, 2，黃昌勤1, 3，羅旋1，聶瑞華1，湯庸1，梅曉勇1

（1. 華南師范大學(xué)教育信息技術(shù)學(xué)院，廣東廣州 510631； 2. 廣東科學(xué)技術(shù)職業(yè)學(xué)院藝術(shù)設(shè)計學(xué)院，廣東廣州 510640；3. 浙江大學(xué)電子服務(wù)研究中心，浙江杭州310027）

云計算環(huán)境下服務(wù)的動態(tài)性和易失效性是云應(yīng)用的重要挑戰(zhàn)，服務(wù)替換是其主要對策和關(guān)鍵研究問題。在類型論的支持下提出了一種新的云服務(wù)替換判定方法，該方法首先對會話類型論進(jìn)行語義擴(kuò)展以建模云服務(wù)行為，設(shè)計了典型云服務(wù)QoS類型實現(xiàn)服務(wù)質(zhì)量判斷，然后構(gòu)造了語義會話類型和QoS類型的各子類型規(guī)則，最后以此完成了服務(wù)一致性和上下文兼容性命題判定與實施。通過應(yīng)用判定實例展示和實驗效果分析，表明該判定方法可行，并能為組合服務(wù)應(yīng)用帶來更高的執(zhí)行成功率。

云服務(wù)；類型理論；會話類型；服務(wù)替換

1 引言

在云計算環(huán)境下，服務(wù)作為一種基本的計算實體在云應(yīng)用中起著至關(guān)重要的作用[1]。在實際的業(yè)務(wù)應(yīng)用中，由于云平臺及應(yīng)用的可伸縮性、可移動云服務(wù)本身的不確定性，導(dǎo)致服務(wù)呈現(xiàn)高度動態(tài)性，服務(wù)QoS變化甚至服務(wù)失效成為云應(yīng)用面臨的嚴(yán)峻挑戰(zhàn)[2]；同時，在市場機(jī)制激勵下云服務(wù)數(shù)量不斷增加、功能演進(jìn)，服務(wù)存在版本更新需求。為了提高云服務(wù)應(yīng)用（尤其是組合云服務(wù)）的正確性、及時性和可靠性，服務(wù)動態(tài)替換成為領(lǐng)域關(guān)注的焦點問題之一。

服務(wù)替換的核心在于服務(wù)選擇與語義驗證，主要包括服務(wù)描述、服務(wù)選擇和替換驗證。在服務(wù)描述方面，傳統(tǒng)方法基于UDDI技術(shù)，通過輸入輸出參數(shù)格式與關(guān)鍵字來描述服務(wù)的語法信息，后續(xù)研究在關(guān)鍵詞匹配的基礎(chǔ)上引入本體論進(jìn)行描述，以彌補(bǔ)了語義描述方面的缺陷，但對服務(wù)行為的考慮仍存不足[3]。一些研究將形式化的方法運(yùn)用于服務(wù)建模，使用Petri網(wǎng)、擴(kuò)展的動態(tài)描述邏輯EDDL(X)、π演算等對服務(wù)進(jìn)行形式化建模，并借助動作過程斷言等來刻畫動作的執(zhí)行過程[4~6]。該類形式化方法能夠較好刻畫服務(wù)的行為，但對服務(wù)QoS約束的考慮存在不足，不能較好地支持服務(wù)在動態(tài)與全局環(huán)境下的替換。在服務(wù)選擇方面，較早的服務(wù)選擇多以靜態(tài)的服務(wù)功能需求為目標(biāo)，通過參數(shù)格式匹配進(jìn)行語法級別的服務(wù)選擇，后續(xù)研究嘗試將語義信息匹配引入選擇過程，如基于聯(lián)接本體、事務(wù)級別、著色Petri網(wǎng)模型等，它們或設(shè)計選擇機(jī)制或提出選擇算法，并多支持語義的推理與匹配[7~9]。上述研究雖提高了服務(wù)選擇的準(zhǔn)確率，但在語義信息不足的情況下，會出現(xiàn)較大的不確定性。在服務(wù)的替換性驗證方面，目前研究主要利用進(jìn)程代數(shù)、π演算等理論，驗證內(nèi)容涵蓋上下文兼容性、行為的一致性等方面，相關(guān)研究有的基于形式化工具，有的借助自定義的消解規(guī)則或自動機(jī)[10~13]。這些方法因使用了完備的理論方法，可以較好地保障服務(wù)替換的準(zhǔn)確性，然而驗證的復(fù)雜度很高，在服務(wù)較多的應(yīng)用場景下可用性明顯受限，且較難實現(xiàn)驗證的自動化。云計算環(huán)境下，云服務(wù)數(shù)量巨大且高度動態(tài)，需要尋找新方法支持高效、準(zhǔn)確和自動化的服務(wù)替換。

類型論的形式化系統(tǒng)完備，能有效支持服務(wù)的語法和語義描述，且具備相對較低的計算復(fù)雜度。在現(xiàn)有研究中，典型情況是擴(kuò)展馬丁洛夫類型理論，補(bǔ)充新類型，從而對云服務(wù)的交互行為進(jìn)行有效表征[14~16]。部分研究基于擴(kuò)展會話類型實現(xiàn)服務(wù)建模，以此為基礎(chǔ)完成服務(wù)等價性驗證[17,18]。由此可見，現(xiàn)有相關(guān)研究主要考慮服務(wù)的語法部分，但描述精確度有待提高，同時，同一形式化體系中尚未見對云服務(wù)多維QoS關(guān)注的服務(wù)替換研究成果。

綜上，傳統(tǒng)形式化方法在描述和判定方面，要么因異常復(fù)雜而失效，要么存在不能兼顧服務(wù)行為功能和非功能需求。鑒于類型論對服務(wù)相關(guān)語法和語義等具有良好的描述能力，本文對其進(jìn)行語義拓展和規(guī)則設(shè)計以有效解決云服務(wù)替換性判定。

2 語義會話類型

2.1 會話類型及其語義擴(kuò)展

會話類型是一種采用類型論通用方法構(gòu)造的類型，常用于描述服務(wù)的動態(tài)行為，因其對動態(tài)行為描述的優(yōu)勢，可用于高度動態(tài)的云服務(wù)的建模，且通過類型間的子類型判定，來推導(dǎo)會話間的子類型關(guān)系，進(jìn)而基于子類型關(guān)系實現(xiàn)服務(wù)一致性和兼容性命題的推導(dǎo)，并最終完成可替換性判定。

傳統(tǒng)的會話類型在服務(wù)調(diào)用參數(shù)的構(gòu)造上，多基于語法而未考慮語義，因而在Reception類型（接收類型，表示服務(wù)接收其他服務(wù)消息的接口）和Sending類型（發(fā)送類型，表示服務(wù)向其他服務(wù)發(fā)送消息的接口）的子類型判定上存在不足，易導(dǎo)致替換性方案查全率的降低；同時，在Branching類型（分支類型，表示服務(wù)的內(nèi)部流程分支，接受其他服務(wù)對分支的選擇）和Selection類型（選擇類型，表示服務(wù)對外的選擇操作，該選擇對應(yīng)其他服務(wù)相應(yīng)的分支）的操作語義標(biāo)簽上語義描述較為模糊。本文構(gòu)造領(lǐng)域本體，利用本體的語義推理和匹配優(yōu)勢完成服務(wù)消息的語義級支持。不失一般性，本研究將操作語義歸為“動作”和“對象”2個部分，利用本體支持下的服務(wù)操作語義進(jìn)行類型論擴(kuò)展，以改變傳統(tǒng)類型論中的簡單語義標(biāo)簽狀況，其基本策略是：將Selection/Branching中的語義標(biāo)簽替換成構(gòu)造類型Op，將Reception/Sending中的消息類型Message進(jìn)行構(gòu)造，形成語義會話類型（簡稱SST），從而基于精確語義促使服務(wù)替換性得以更加可靠的驗證。

SST對傳統(tǒng)會話類型的擴(kuò)展內(nèi)容如下

2.2 領(lǐng)域本體的構(gòu)造

領(lǐng)域本體由領(lǐng)域內(nèi)的共享概念及概念間關(guān)系組成，因此，將領(lǐng)域本體定義為二元組Ontology= {Concepts×Relationships}set。為了有效構(gòu)造Message類型，擬將旅行服務(wù)常見的消息概念抽取出來，將其完整建立在旅行服務(wù)本體中（如圖1所示）；對于Op類型構(gòu)造，將領(lǐng)域本體中概念的常用的操作動作進(jìn)行抽取，形成旅行服務(wù)操作動作的枚舉集合Action={Cancel,Book,Refund,…}set。

根據(jù)已有研究，引入依賴記錄類型[19](DRT，dependent record type)對本體進(jìn)行描述。DRT的表現(xiàn)形式為<1:1,2:2,…,l:T>，.用于選取標(biāo)簽為的記錄。

以旅行服務(wù)本體中的Ticket概念為例，利用DRT對其描述如下

Ticket=

Address=

Vehicle=

Time=

通過選取操作可獲取Ticket中的某個屬性或子概念，例如Ticket.fare=Integer。通過遞歸使用DRT的選取操作，可得Ticket.vehicle.kind =String。為后續(xù)消息間子類型的判定，需要構(gòu)造概念間子類型關(guān)系。分析可知，服務(wù)消息中的參數(shù)可能屬于某個概念的范疇，但不一定包含該概念在本體樹中所有的子節(jié)點。以Vehicle范疇為例，若、都屬于Vehicle范疇，=，=，可知具備的所有語義信息，且更多，則可判定。利用形式化方法表述該概念類型的子類型規(guī)則為

若1、2均為本體中的某個概念，2中的每個標(biāo)簽都能在1中找到對應(yīng)標(biāo)簽，且利用相同標(biāo)簽取出的類型中，2取出的類型是1取出類型的子類型或相等類型。更具體地，即1包含2的所有語義，要么12完全一樣，要么1更寬泛2更具體。例如“火車票”是“票”的子類型，因為“火車票”相比“票”至少多Ticket.vehicle.kind語義。顯然，當(dāng)用戶請求的是無種類限制的票時，火車票也能滿足用戶的需求。對于旅行業(yè)務(wù)中的其他概念，也可以建立類似的子類型規(guī)則，最終形成本體內(nèi)的子類型規(guī)則庫，以支持概念實體間的子類型判定。為了一致性需要，將概念實體間的子類型規(guī)則統(tǒng)稱為concept-subtyping rules，簡稱Concept-S。

2.3 消息類型的構(gòu)造

服務(wù)消息即服務(wù)的輸入與輸出（也稱IO），即WSDL中的Message。在最典型應(yīng)用場境——服務(wù)組合中，原子服務(wù)之間的交互，以及組合服務(wù)與用戶間的交互，都可以看做消息的傳遞。在類型論的服務(wù)支持中，對服務(wù)消息進(jìn)行類型論建模，是服務(wù)組合方案搜索、服務(wù)替換等相關(guān)操作的基礎(chǔ)。基于MLTT(馬丁洛夫類型理論)中無序列表類型、迪氏積類型、枚舉類型的構(gòu)造方法，消息類型的構(gòu)造如下

在實際使用中，MsgBody類型的實例中可能存在概念相同的元素。為避免在比較中混淆，可將其父節(jié)點加入命名。例如將Hotel中的Place標(biāo)記為Hotel-Place以避免與其他Place混淆。旅行業(yè)務(wù)中的一個有關(guān)Hotel的消息類型可能表達(dá)如下

{,}>,,}>}

引入笛氏積集合的選取子和，方便在推導(dǎo)中取出笛氏積集合典則元的各個部分，(<,>)=，(<,>)=。為支持后續(xù)的子類型命題的證明，定義笛氏積子類型規(guī)則（Decare-S）為

并在前文Concept-S基礎(chǔ)上構(gòu)造服務(wù)消息的子類型規(guī)則，子類型規(guī)則構(gòu)造如下。

規(guī)則1 SimpleType-S簡單數(shù)據(jù)類型的子類型規(guī)則

規(guī)則2 ComplexType-S復(fù)雜數(shù)據(jù)類型的子類型規(guī)則

規(guī)則3 MsgBody-S消息體類型的子類型規(guī)則

規(guī)則4 Message-S服務(wù)類型的子類型規(guī)則

規(guī)則1中，所使用的XSD-C為基本數(shù)據(jù)類型間的強(qiáng)制轉(zhuǎn)換規(guī)則。根據(jù)XSD標(biāo)準(zhǔn)數(shù)據(jù)類型的定義，如果數(shù)據(jù)類型可以強(qiáng)制轉(zhuǎn)換為數(shù)據(jù)類型，且不丟失精度不改變意義，則記為。例如Integer可以轉(zhuǎn)化為Float類型，XML可以轉(zhuǎn)化為String類型，且不丟失其精確度，則。由上述規(guī)則可知，只要有充足的概念子類型規(guī)則支持，即可通過規(guī)則推導(dǎo)得出消息之間的準(zhǔn)確子類型關(guān)系。

2.4 操作類型的構(gòu)造

操作類型Op表達(dá)原子服務(wù)對外發(fā)起調(diào)用、或受到外界調(diào)用時的操作語義，通常作為成員出現(xiàn)在Selection類型和Branching類型中。一個操作的語義通常包括{發(fā)起者，動作，對象}3部分，發(fā)起者對本研究SST的操作語義沒有影響，在構(gòu)造中省略。因此，本研究將Op構(gòu)造為動作與對象的笛氏積，其中，動作由動作集合中元素描述，而對象則利用本體中的概念描述。構(gòu)造set則Op類型的子類型規(guī)則Op-S定義如下

3 云服務(wù)QoS類型

3.1 云服務(wù)QoS類型的構(gòu)造

云服務(wù)QoS是云服務(wù)的非功能性因素，亦即服務(wù)質(zhì)量，是服務(wù)能否滿足云應(yīng)用需求的重要標(biāo)準(zhǔn)，在高度動態(tài)的云計算環(huán)境下尤顯重要。與第2節(jié)類似，建立QoS本體，以便利用類型論建模QoS，支持服務(wù)替換命題的證明。云服務(wù)具有資源綁定高度動態(tài)、宿居環(huán)境多樣、按需付費(fèi)等特性，需選取相應(yīng)的特征性指標(biāo)來建模云服務(wù)QoS。本文參照已有研究，僅選取價格、可靠性和云服務(wù)等級3項指標(biāo)做針對性地分析與建模。

與第2節(jié)中類似，對QoS類型（后稱QoST）使用DRT進(jìn)行描述，如圖2所示。

QoS =

Price=

Reliability =

ServiceLevel=

其中，Price為服務(wù)調(diào)用需要支付的費(fèi)用，ServiceLevel為云提供商的評級，兩者以數(shù)值方式參與后續(xù)QoS計算。價格由服務(wù)提供商提供，包括調(diào)用服務(wù)的最低價格和最高價格，對調(diào)用者來說，通常只有報價可見。云服務(wù)的評級則由用戶的評分累積計算形成。價格與服務(wù)評級為云服務(wù)的特征性因素，獲取較為簡單，此處不做詳細(xì)探討，將重點分析云服務(wù)可靠性的計算方法。

云服務(wù)環(huán)境中，原子服務(wù)在可靠性方面具有不確定性，它由服務(wù)宿居硬件可靠性、自身軟體可靠性以及涉外通信鏈路的可靠性共同決定。在一般假設(shè)前提下（即原子服務(wù)宿居節(jié)點的各硬件、宿居的軟件體、基于鏈路的對外數(shù)據(jù)交換的故障、失效等事件相互獨立，宿居節(jié)點各硬件和通信鏈路上的故障或失效過程服從齊次泊松分布等），用sr(cpu)、sr(mem)、sr()和sr(),分別表示服務(wù)宿居節(jié)點的CPU、內(nèi)存、網(wǎng)絡(luò)通信和軟體本身的可靠性，則原子服務(wù)的可靠性計算為sr(cpu)sr(mem)sr()sr()。在可移動環(huán)境中，sr()較為復(fù)雜，如果用Int表示原子服務(wù)宿居設(shè)備節(jié)點與對外通信節(jié)點間的通信鏈路的失效強(qiáng)度，用表示通信平均時長，sr()= exp(?Int.)。

3.2 QoST的子類型規(guī)則

考慮應(yīng)用需求，在服務(wù)替換中存在服務(wù)選擇與計算過程，其中，服務(wù)QoS各分量存在大小關(guān)系，將用于數(shù)量比較。根據(jù)可靠性、價格、服務(wù)評級等因素對服務(wù)替換的影響，定義如下子類型基本判定規(guī)則——QoST子類型規(guī)則(QoST-S)。

在服務(wù)QoS比較的應(yīng)用場景中，經(jīng)常出現(xiàn)某個服務(wù)的某些QoS指標(biāo)較高，而其他QoS指標(biāo)較低，但綜合QoS仍舊較高的情況。因此QoS類型的子類型應(yīng)具備指標(biāo)間協(xié)商的功能。實際應(yīng)用場景中，如果根據(jù)用戶需求可以進(jìn)行某些QoS指標(biāo)的協(xié)商，則可將相應(yīng)協(xié)商規(guī)則加入QoST-S規(guī)則中，參與服務(wù)子類型的推導(dǎo)。本文考慮到云服務(wù)按需付費(fèi)的特征性因素，針對價格可協(xié)商的特性，定義了協(xié)商表達(dá)式，并構(gòu)造了如下QoS協(xié)商規(guī)則。其中，協(xié)商表達(dá)式含義為，對進(jìn)行次協(xié)商，每次協(xié)商使的屬性下降（若箭頭為則為上升）Δ（步長），并最終返回協(xié)商完成（各項指標(biāo)發(fā)生相應(yīng)變化）之后的。

規(guī)則5 QoS-(Reliability-lowerPrice)-N-S服務(wù)QoS協(xié)商規(guī)則

規(guī)則6 QoS-(ServiceLevel-lowerPrice)-N-S服務(wù)QoS協(xié)商規(guī)則

規(guī)則7 QoS-(Reliability-higherPrice)-N-S服務(wù)QoS協(xié)商規(guī)則

規(guī)則8 QoS-(ServiceLevel-higherPrice)-N-S服務(wù)QoS協(xié)商規(guī)則

規(guī)則9 QoS-all-N-S 服務(wù)QoS協(xié)商規(guī)則

4 基于SST和QoST的云服務(wù)建模

4.1 基于類型論的云服務(wù)建模

從替換的視角來看，云服務(wù)由服務(wù)的QoS及服務(wù)的功能構(gòu)成，基于語義會話類型SST與QoST，將云服務(wù)建模為QoS與服務(wù)功能的笛氏積set。其典則元（云服務(wù)實例）包含2部分，分別為QoST的實例與SST描述的實例。

4.2 云服務(wù)類型的子類型規(guī)則

構(gòu)造服務(wù)的子類型規(guī)則，需在QoST-S的基礎(chǔ)上，繼續(xù)構(gòu)造SST所描述的服務(wù)功能類型的子類型規(guī)則。服務(wù)功能由多種類型構(gòu)造而成，因此服務(wù)功能的子類型判定規(guī)則也需要多種子類型規(guī)則同時支持。引入會話類型的標(biāo)準(zhǔn)環(huán)境(well-formed environments)，參照傳統(tǒng)會話類型的子類型規(guī)則，構(gòu)造如下SST中的子類型規(guī)則，如表1所示。

表1 SST的子類型規(guī)則

分析上述子類型規(guī)則可發(fā)現(xiàn)，子類型在接收消息時，需要的消息在語義范圍上更?。辉诎l(fā)送消息時，發(fā)出的消息在語義涵蓋范圍上更大；在向外發(fā)出選擇時，選擇更多且該選擇的語義涵蓋更大；自己提供的分支更少，且分支的語義涵蓋更精確。當(dāng)會話子類型在替換原會話時，接受消息和分支操作的接口語義涵蓋更廣，意味著在被調(diào)用時能夠保證原功能的實現(xiàn)；發(fā)送消息和選擇操作則語義涵蓋范圍更窄，意味著在調(diào)用其他服務(wù)時，也能保證其他服務(wù)功能的實現(xiàn)。因此子類型在功能上可以安全的替換父類型。

在服務(wù)QoST-S子類型命題證明的基礎(chǔ)上，構(gòu)造服務(wù)的子類型規(guī)則（Service-S）。

5 云服務(wù)替換性判定

在動態(tài)化的云計算環(huán)境中，服務(wù)替換是一個涉及行為功能語義、服務(wù)QoS及其上下文等因素的復(fù)雜過程，這也導(dǎo)致了服務(wù)替換性判定具有挑戰(zhàn)性。由于類型論對服務(wù)相關(guān)語法和語義等具有良好的描述能力，可成為服務(wù)替換性判定的支持工具。本研究將基于上述擴(kuò)展類型論支持下的云服務(wù)模型及相關(guān)規(guī)則，解決其云服務(wù)替換判定。

5.1 替換性命題構(gòu)造與服務(wù)一致性判定

根據(jù)會話類型的相關(guān)定義，云服務(wù)替換性命題可以等價為云服務(wù)在類型理論體系中的子類型命題，由此依據(jù)類型論，服務(wù)替換性命題構(gòu)造如下

服務(wù)一致性和上下文兼容性是云服務(wù)替換的可靠保障。服務(wù)一致性判定指從行為功能和QoS這2個方面進(jìn)行比較，以判定原服務(wù)能否被新服務(wù)替換進(jìn)行業(yè)務(wù)操作。根據(jù)前述云服務(wù)描述，顯然可將服務(wù)一致性判定分解為行為功能和QoS這2部分的子類型判定命題。基于會話類型論，本研究將利用各子類型規(guī)則對命題進(jìn)行判定（或稱證明）。對于服務(wù)QoS部分命題（即()與()間子類型命題），由于云環(huán)境下具有波動的可靠性問題、價格等多重因素，采用基本判定和協(xié)商判定并存的策略。基本判定利用QoST-S規(guī)則進(jìn)行，協(xié)商判定則可將相應(yīng)協(xié)商規(guī)則加入判定過程。服務(wù)行為功能的子類型命題（即()與()間子類型命題）可據(jù)SST子類型判定規(guī)則，將原命題分解為各個不同成員類型之間的子類型命題進(jìn)行判定。命題分解證明（判定）方法如下

綜上所述，基于類型論完成替換性命題構(gòu)造，可為替換性判定帶來形式化支持，其中，服務(wù)一致性命題判定完全可利用本研究定義的子類型規(guī)則、按照上述方法得到遞歸式證明（判定）。

5.2 替換性命題的功能兼容性判定

由于云服務(wù)依據(jù)服務(wù)上下文而動態(tài)變化，在云服務(wù)替換中服務(wù)的上下文兼容尤顯重要。因此，替換性命題需要其兼容性的判定支持。由于服務(wù)QoS不具有兼容性特性，因此在替換性命題的兼容性判定中，僅需要判定服務(wù)行為功能的兼容性即可。

因此，服務(wù)功能兼容性判定需藉助各子類型規(guī)則支持，最終證明上式成立。根據(jù)會話類型中鏡像類型可知，判定過程中必須處理兼容性成員類型為Sending、Reception、Selection、Branching，前兩者包含消息收發(fā)的兼容性，后兩者包含流程分支的兼容性。根據(jù)會話類型的語法和語義，可分別構(gòu)造兼容性的判定規(guī)則，然后實施規(guī)則推導(dǎo)，最終完成命題判定。限于篇幅，僅以2個例子說明判定過程。

1) Sending-Reception中reception類型的替換

前提條件為

兼容性判定規(guī)則為

目標(biāo)命題證明為

2) Selection-Branching中branching類型的替換

前提條件為

兼容性判定規(guī)則為

目標(biāo)命題證明

對于其他兼容性成員類型，可采用類似子類型規(guī)則予以判定。由此，在服務(wù)行為功能的兼容性可得保證。

5.3 面向云服務(wù)組合的服務(wù)替換

在云環(huán)境中，服務(wù)組合是服務(wù)完成業(yè)務(wù)邏輯流程編制的基本形式。受上下文影響，云服務(wù)失效、低QoS檢出等成為常態(tài)；同時，基于市場競爭機(jī)制的云服務(wù)演進(jìn)，使得服務(wù)版本的判定與置換也成必然。因此，為了有效實現(xiàn)組合服務(wù)的云應(yīng)用，必須解決云服務(wù)替換這個核心問題。本研究以云服務(wù)組合為背景考察云服務(wù)替換的具體實施。

鑒于云計算環(huán)境的特殊性，在云服務(wù)組合中服務(wù)替換改變依據(jù)傳統(tǒng)服務(wù)檢查等常規(guī)觸發(fā)方法，將以云服務(wù)上下文變化為觸發(fā)事件；同時在替換判定中，應(yīng)用前述基于類型論的行為功能語義、QoS及功能兼容性判定，必要時啟用QoS協(xié)商。候選置換服務(wù)獲取算法如圖3所示。

算法：候選置換服務(wù)集的獲取算法Replacement_Algorithm輸入：需要進(jìn)行替換的服務(wù)WS和可用云服務(wù)UDDI輸出：備選的新服務(wù)組合List(WSr)Replacement_Algorithm(WSa)Begin1) While云服務(wù)上下文變化Do2) 觸發(fā)到服務(wù)檢測事件；3) IF檢測到組合服務(wù)中某WS失效OR其QoS指標(biāo)<預(yù)期閾值Then//進(jìn)入替換判定4) Flag=0；5) For WS in UDDI，利用SST規(guī)則系統(tǒng)和QoST基本規(guī)則系統(tǒng)，從一致性及其兼容性判定WS<:WSa命題；6) 如果推導(dǎo)得出WS<:WSa，則將WS作為WSr加入組合服務(wù)候選集List(WSr)7) End For;8) IF |List(WSr)|=Φ AND Flag=0 Then //進(jìn)入QoS協(xié)商9) Flag=1；10) QoST協(xié)商規(guī)則系統(tǒng)->QoST基本規(guī)則系統(tǒng)11) Goto 5)；12) End IF； //結(jié)束QoS協(xié)商13) 返回List(WSr)；14) End IF //進(jìn)入替換判定15) End WhileEnd

6 應(yīng)用實例及其效果分析

6.1 服務(wù)替換性判定實例

本文以旅行服務(wù)中最常見的交通票務(wù)預(yù)訂服務(wù)為例，分析SST與QoST支持的服務(wù)描述與替換性證明過程?，F(xiàn)有2個預(yù)訂服務(wù)BOOKING1和BOOKING2，通過上文所述方法，判定前者是后者的子類型，則前者可以安全地替換后者。限于篇幅，對部分服務(wù)描述不作詳細(xì)展開。

BOOKING1= 1= &{1:1;1}

1={Book,{, ,, }>, }

1=?({,, ,}>})

1=+{{Cancel,ticket1}:end|{Pay,ticket2}:!(msg1);&{{Pay,ticket3}:?(msg2)|{Cancel,ticket4}:end}|{Change,ticket5}:ChangeTicket}

BOOKING2=2=&{2:2;S2}

2={Book,{, , ,}>}}

2=?({,, ,,}>})

2=+{{Cancel,ticket6}:end|{Pay,ticket7}:!(msg3);&{{Pay,ticket8}:?(msg4)|{Cancel,ticket9}:end}}

依照前文所述方法，可將目標(biāo)命題拆分為1<:2與1<:2這2個子判定命題。其中，QoS部分為數(shù)值比較，此處不作展開。1<:2命題的證明思路如下。

1)1、2均為Branching類型實例，根據(jù)Branching-S將命題拆分為1<:2、1;1<:2;2這2個命題。

2)利用Op-S證明1<:2。

3)1;1、2;2均為Reception類型實例，根據(jù)Reception-S將命題拆分為1<:2、1<:2。

以1)和3)為例：

觀察可知，1與2的Reception實例中的消息實例有如下關(guān)系：二者總體相似，但1中的消息無Vehicle.Name語義，可推斷1<:2。

4)類似3)，照命題中需判定的對象所屬的類型，選取對應(yīng)規(guī)則進(jìn)行拆分與證明。若全部拆解完成，且都能得到證明，則整體替換性命題得證。

6.2 面向服務(wù)組合的應(yīng)用效果分析

為考察本研究提出的替換方法面向?qū)嶋H應(yīng)用的能力，本文選取Apache軟件基金會的ODE作為BPEL引擎以支持服務(wù)組合，選取Cloudstack作為IaaS框架以搭建云環(huán)境，構(gòu)建了以下試驗環(huán)境：1臺IBM x3500M4服務(wù)器（24核2 GHz處理器、16 GB內(nèi)存和Ubuntu12.04.4LTS操作系統(tǒng)），1臺IBM x3650M4服務(wù)器（24核2 GHz處理器、32 GB內(nèi)存和Ubuntu12.04.4LTS操作系統(tǒng)）。基于Cloudstack4.2.0的云環(huán)境，建立30臺虛擬服務(wù)器（1 GHz處理器、1 GB內(nèi)存和Ubuntu12.04.4LTS操作系統(tǒng)）以模擬云服務(wù)場景，建立1臺虛擬服務(wù)器（4 GHz處理器、4 GB內(nèi)存和Ubuntu12.04.4LTS操作系統(tǒng)）以運(yùn)行ODE引擎，通過6臺客戶機(jī)（Intel Core i5 3.2 GHz，4 GB RAM和Windows7 64 bit Ultimate操作系統(tǒng)）以模擬云服務(wù)請求。編寫插件集成于ODE，以實現(xiàn)規(guī)則庫支持的推導(dǎo)演算。

鑒于旅游業(yè)務(wù)包含各類典型原子服務(wù)，可獲得云平臺的良好部署和應(yīng)用支持，本文選擇此業(yè)務(wù)進(jìn)行理論驗證?？紤]到云服務(wù)替換中的現(xiàn)實復(fù)雜性（云服務(wù)類型和數(shù)量眾多），本實驗選取該業(yè)務(wù)中10個常用服務(wù)和大量服務(wù)數(shù)進(jìn)行比較研究。所選常用服務(wù)涉及各項業(yè)務(wù)功能，皆用會話類型描述，具有驗證代表性，它們包括行程規(guī)劃、機(jī)票預(yù)訂、火車票預(yù)訂、酒店預(yù)訂、租車、門票預(yù)訂、在線第三方支付、銀行結(jié)算、運(yùn)營商短信、快遞等，在此基礎(chǔ)上對10個服務(wù)進(jìn)行修改和擴(kuò)展形成500個服務(wù)的集合，隨機(jī)放入30臺虛擬服務(wù)器中。通過模擬服務(wù)組合中原子服務(wù)失效的場景，并選取傳統(tǒng)的基于關(guān)鍵詞的匹配與替換（本文簡稱KSCM）、支持早期預(yù)測的服務(wù)替換算法（見文獻(xiàn)[8]，本文簡稱為EPSSM）、考慮組合上下文的服務(wù)替換（見文獻(xiàn)[9]，本文簡稱LDBSSM）和本文中基于類型論的服務(wù)替換方法（簡稱STBM）進(jìn)行對比實驗。由于云服務(wù)的QoS高度動態(tài)，無法確定滿足要求的服務(wù)數(shù)量，因此本文不選用查全率作為考察指標(biāo)；在查準(zhǔn)率的考察方面，考慮到在云服務(wù)組合中，判斷單個服務(wù)查找是否準(zhǔn)確存在困難。從應(yīng)用視角出發(fā)，采用替換后組合服務(wù)的執(zhí)行成功率作為指標(biāo)具備可操作性，且能夠反映替換方法的準(zhǔn)確度；另將服務(wù)數(shù)量擴(kuò)展至3 500個，以對比4種方案的查找耗時，考察4種方法的效率。情況如圖4和圖5所示。

圖4反映了不同服務(wù)數(shù)量情況下，4種方法獲取替換方案的耗時。可以看出，4種方法均隨候選服務(wù)集的增大耗時增多。EPSSM、STBM與LDBSSM使用預(yù)測、上下文檢測、形式化等方法，初始耗時相對較長。其中，STBM由于初始規(guī)則較多，在開始階段耗時較長，但隨著服務(wù)增多，由于STBM的規(guī)則不會出現(xiàn)大幅增加，因此耗時增長速度放緩。LDBSSM因上下文檢測的對象快速增加，計算耗時快速增大。證明STBM方法可擴(kuò)展性相對較強(qiáng)，在面對服務(wù)數(shù)量劇增時能兼顧效率。

圖5反映了不同服務(wù)數(shù)量下，4種方法在應(yīng)用場景中的成功率。可以看出，STBM、EPSSM、LDBSSM總體上明顯優(yōu)于KSCM，尤其是在備選服務(wù)較少的情況下。其中，KSCM在服務(wù)較少情況下替換成功率較低，隨著服務(wù)增多成功率逐漸提高，但最終穩(wěn)定在60%左右。STBM隨服務(wù)數(shù)量增多成功率逐步提高，但提高過程存在小幅波動。EPSSM在服務(wù)較少情況下成功率最高，但隨著服務(wù)增多有小幅度下降。LDBSSM則呈現(xiàn)先上升后小幅下降的趨勢。分析可知，KSCM在備選服務(wù)較少時可能無法通過關(guān)鍵字選取到合適的服務(wù)，因而替換的執(zhí)行成功率較低。而STBM、EPSSM、LDBSSM由于具備上下文、語義信息采集能力，因此在備選服務(wù)較少時，有更大幾率獲取到關(guān)鍵字不匹配但功能相容的服務(wù)，因此成功率較高。EPSSM因其未使用系統(tǒng)的形式化方法，服務(wù)表達(dá)存在一定模糊性，因而在服務(wù)數(shù)量較多的情況下成功率有所下降。LDBSSM與STBM使用形式化方法，在服務(wù)數(shù)量增加時成功率上升，但LDBSSM使用的Petri網(wǎng)形式化方法存在驗證上的復(fù)雜性，因而在服務(wù)數(shù)量較大的情況下可能給出不可靠的結(jié)果導(dǎo)致成功率有所下降。實驗證明，STBM在大規(guī)模服務(wù)場景下有較好的可適用性。

綜上，本文提出的方法有效提高了小范圍內(nèi)的服務(wù)替換成功率，且在服務(wù)集規(guī)模增大過程中，依舊保持了較高的替換成功率，具備較好的擴(kuò)展性。在效率方面，本文方法避免了計算復(fù)雜度的爆炸式增長，提高替換成功率的同時，付出了較小的時間代價。如實驗對象選擇時所述，旅游業(yè)務(wù)包含了多種類多數(shù)量的云服務(wù)，具有一般組合服務(wù)業(yè)務(wù)的典型特征，同時鑒于會話類型在服務(wù)描述方面代價較低，因此，以會話類型為基礎(chǔ)的該云服務(wù)替換性判斷方法具有較好的通用性，尤其在涉及高可信性需求的云服務(wù)應(yīng)用中將表現(xiàn)出良好的現(xiàn)實價值。

7 結(jié)束語

云服務(wù)選擇與替換對云應(yīng)用至關(guān)重要，其中，對云服務(wù)動態(tài)行為功能與QoS進(jìn)行準(zhǔn)確描述，是判斷服務(wù)行為可替換性的前提條件，也是云服務(wù)快速自動和可靠組合的重要基礎(chǔ)。本文提出擴(kuò)展后的語義會話類型SST，并對云服務(wù)QoS進(jìn)行分析與建模，構(gòu)造QoST類型，設(shè)計SST與QoST的子類型規(guī)則，以此實現(xiàn)云服務(wù)特征化描述，最終完成基于子類型規(guī)則的替換性命題和兼容性命題判定。實例分析和實驗測試表明，該云服務(wù)替換性判定方法具有良好可行性，不僅能完成對服務(wù)替換性兼容性的有效驗證，也能較好提高組合服務(wù)的執(zhí)行成功率。后續(xù)將本文方法運(yùn)用到服務(wù)組合方案的制定中，并對原子服務(wù)間一對多、多對多的替換方法進(jìn)行探究，是后續(xù)研究的可能方向。

[1] TAO F, LAILI Y, XU L, et al. FC-PACO-RM: a parallel method for service composition optimal-selection in cloud manufacturing system[J].IEEE Tran on Industrial Informatics, 2013, 9(4): 2023-2033.

[2] AMIN J, ELANKOVAN S, ZALINDA O. Cloud computing service composition: a systematic literature review[J]. Expert System with Applications, 2014,41(8): 3809-3824.

[3] 吳健, 吳朝暉, 李瑩, 等. 基于本體論和詞匯語義相似度的 Web 服務(wù)發(fā)現(xiàn)[J]. 計算機(jī)學(xué)報, 2005, 28(4): 595-602.

WU J, WU Z H, LI Y, et al. Web service discovery based on ontology and similarity of words[J]. Chinese Journal of Computers, 2005, 28(4): 595-602.

[4] JUAN C V, MANUEL L, ALBERTO B. Toward the use of petri nets for the formalization of OWL-S choreographies [J]. Knowledge and Information Systems, 2012, 32(3): 629-665.

[5] 常亮, 史忠植, 陳立民, 等.一類擴(kuò)展的動態(tài)描述邏輯[J].軟件學(xué)報, 2010,21(1):1-13.

CHANG L, SHI Z Z, CHEN L M, et al. Family of extended dynamic description logics[J]. Journal of Software, 2010,21(1):1-13.

[6] 廖軍, 譚浩, 劉錦德. 基于Pi-演算的Web服務(wù)組合的描述和驗證[J]. 計算機(jī)學(xué)報, 2005,28(4):635-643.

LIAO J, TAN H, LIU J D. Describing and verifying Web service using Pi-calculus[J]. Chinese Journal of Computers, 2005, 28(4): 635-643.

[7] HE K, WANG J, LIANG P. Semantic interoperability aggregation in service requirements refinement[J]. Journal of Computer Science and Technology, 2010,25(6):1103-1117.

[8] 印瑩, 張斌, 張錫哲. 面向組合服務(wù)動態(tài)自適應(yīng)的事務(wù)級主動伺機(jī)服務(wù)替換算法[J].計算機(jī)學(xué)報, 2010, 33(11): 2147-2162.

YIN Y, ZHANG B, ZHANG X Z. An active and opportunistic service replacement algorithm orienting transactional composite service dynamic adaptation[J]. Chinese Journal of Computers, 2010, 33(11): 2147-2162.

[9] 王海艷,李思瑞. 基于組合上下文的服務(wù)替換方法[J]. 通信學(xué)報,2014,35(9):57-67.

WANG H Y, LI S R. Service substitution method based on composition context[J]. Journal on Communications, 2014,35(9):57-67.

[10] KUANG L, XIA Y, DENG S, et al. Analyzing behavioral substitution of Web services based on π-Calculus[C]//2010 IEEE International Conference on Web Services. Florida, USA, c2010:441-448.

[11] BOUROUZ S, ZEGHIB N. Verifying Web services substitutability using open colored nets reduction techniques[C]//The 5th International Conference on Modeling, Simulation and Applied Optimization. Hammamet, Tunisia, c2013: 1-5.

[12] 劉方方, 史玉良, 張亮, 等.基于進(jìn)程代數(shù)的Web服務(wù)合成的替換分析[J]. 計算機(jī)學(xué)報, 2007,30(11):2033-2039.

LIU F F, SHI Y L, ZHANG L, et al. Substitution analysis of web service composition via process algebra[J]. Chinese Journal of Computers, 2007,30(11):2033-2039.

[13] REN H, LIU J. Service substitutability analysis based on behavior automata[J]. Innovations in Systems and Software Engineering, 2012, 8(4): 301-308.

[14] YIN Y, YIN J, LI Y, et al. Verifying consistency of web services behavior using type theory[C]// 2008 IEEE Aisa-Pacific Services Computing Conference. Yilan, China, c2008:1560-1566.

[15] YIN Y, DENG S. Analysing and determining substitutability of different granularity Web services[J]. International Journal of Computer Mathematics, 2013,90(11):2201-2220.

[16] 殷昱煜, 李瑩, 鄧水光, 等. Web 服務(wù)行為一致性與相容性判定[J]. 電子學(xué)報, 2009,37(3):433-439.

YIN Y Y, LI Y, DENG S G, et al. Determining on consistency and compatibility of Web services behavior[J]. Acta Electronica Sinica, 2009,37(3):433-439.

[17] ANTONIO V, VASCO T. V, ANTONIO R. Typing the behavior of software components using session types[J]. Fundamenta Information, 2006, 73(4): 583-598.

[18] PIERRE-MALO D, NOBUKO Y, ANDI B, et al. Parameterised multiparty session types[J].Logic Method in Computer Science, 2012, 8(4:6):1-46.

[19] DAPOIGNY R, BARLATIER P. Towards a conceptual structure based on type theory[C]//The Int’l Conference on Computational Science. Krakow, Poland, c2008:1-8.

Determining substitutability of cloud services supported by semantically extended type theory

WANG Xian-qing1,2, HUANG Chang-qin1,3, LUO Xuan1, NIE Rui-hua1,TANG Yong1, MEI Xiao-yong1

(1. School of Information & Technology in Education, South China Normal University, Guangzhou 510631, China; 2. School of Art & Design, Guangdong Institute of Science & Technology, Guangzhou 510640, China; 3. E-Service Research Center, Zhejiang University, Hangzhou 310027, China)

In cloud environments, the high dynamics and more service failures were great obstacles to cloud applications, service substitution was a key research issue and also was a main solution to these challenges. A method of determining substitutability of cloud services was proposed using type theory, in which session types were semantically extended for modeling the behaviors of cloud service, QoS such as price, reliability were introduced as QoS type, and a series of subtyping rules were constructed for SST and QoST. After that, determining consistency and context compatibility of services were put into practice. The method was proved feasibly by a case determining, and the experimental results show that it brings higher success rate of execution.

cloud service, type theory, session types, service substitution

TP393

A

10.11959/j.issn.1000-436x.2016026

2015-03-09；

2015-12-15

黃昌勤，cqhuang@zju.edu.cn

國家自然科學(xué)基金資助項目(No.61370229, No.61370178)；國家科技支撐計劃基金資助項目(No.2013BAH72B01)；教育部-中國移動基金資助項目（No.MCM20130651）；廣東省自然科學(xué)基金資助項目（No.S2013010015178）；廣東省科技計劃基金資助項目（No.2014B010103004, No.2014B010117007, No.2015A030401087, No.2015B010110002）；廣東省教育廳科技創(chuàng)新基金資助項目（No.2012KJCX0037）；廣州市科技基金資助項目（No.2014Y2-00006）

The National Natural Science Foundation of China (No.61370229, No.61370178), The National Key Technology R&D Program of China(No.2013BAH72B01), The MOE-CMCC Research Fund(No.MCM20130651), The Natural Science Foundation of Guangdong Province (No.S2013010015178), The S&T Projects of Guangdong Province (No.2014B010103004, No.2014B010117007, No.2015A030401087, No.2015B010110002), The S&T Project of DEGP (No.2012KJCX0037), The S&T Project of Guangzhou Municipality (No.2014Y2-00006)

王先清（1966-），男，湖南臨澧人，廣東科學(xué)技術(shù)職業(yè)學(xué)院副教授，主要研究方向為云服務(wù)、計算機(jī)應(yīng)用技術(shù)、多媒體技術(shù)等。

黃昌勤（1972-），男，湖南常德人，華南師范大學(xué)教授、博士生導(dǎo)師，主要研究方向為可信云服務(wù)、語義智能、大數(shù)據(jù)技術(shù)及其教育應(yīng)用等。

羅旋（1990-），男，湖南常德人，華南師范大學(xué)碩士生，主要研究方向為服務(wù)計算、云計算等。

聶瑞華（1963-），男，江西樟樹人，華南師范大學(xué)教授，主要研究方向為計算機(jī)網(wǎng)絡(luò)及應(yīng)用、云計算與大數(shù)據(jù)等。

湯庸（1964-），男，湖南張家界人，華南師范大學(xué)教授、博士生導(dǎo)師，主要研究方向為社交網(wǎng)絡(luò)與大數(shù)據(jù)應(yīng)用、時態(tài)數(shù)據(jù)與知識工程、協(xié)同計算等。

梅曉勇（1974-），男，湖南常德人，博士，主要研究方向為服務(wù)計算、Petri網(wǎng)技術(shù)與可信計算等。