基于語義擴展類型論的云服務替換性判定研究

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

?

基于語義擴展類型論的云服務替換性判定研究

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

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

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

云服務；類型理論；會話類型；服務替換

1 引言

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

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

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

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

2 語義會話類型

2.1 會話類型及其語義擴展

會話類型是一種采用類型論通用方法構造的類型，常用于描述服務的動態行為，因其對動態行為描述的優勢，可用于高度動態的云服務的建模，且通過類型間的子類型判定，來推導會話間的子類型關系，進而基于子類型關系實現服務一致性和兼容性命題的推導，并最終完成可替換性判定。

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

SST對傳統會話類型的擴展內容如下

2.2 領域本體的構造

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

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

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

Ticket=

Address=

Vehicle=

Time=

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

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

2.3 消息類型的構造

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

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

{,}>,,}>}

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

并在前文Concept-S基礎上構造服務消息的子類型規則，子類型規則構造如下。

規則1 SimpleType-S簡單數據類型的子類型規則

規則2 ComplexType-S復雜數據類型的子類型規則

規則3 MsgBody-S消息體類型的子類型規則

規則4 Message-S服務類型的子類型規則

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

2.4 操作類型的構造

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

3 云服務QoS類型

3.1 云服務QoS類型的構造

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

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

QoS =

Price=

Reliability =

ServiceLevel=

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

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

3.2 QoST的子類型規則

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

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

規則5 QoS-(Reliability-lowerPrice)-N-S服務QoS協商規則

規則6 QoS-(ServiceLevel-lowerPrice)-N-S服務QoS協商規則

規則7 QoS-(Reliability-higherPrice)-N-S服務QoS協商規則

規則8 QoS-(ServiceLevel-higherPrice)-N-S服務QoS協商規則

規則9 QoS-all-N-S 服務QoS協商規則

4 基于SST和QoST的云服務建模

4.1 基于類型論的云服務建模

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

4.2 云服務類型的子類型規則

構造服務的子類型規則，需在QoST-S的基礎上，繼續構造SST所描述的服務功能類型的子類型規則。服務功能由多種類型構造而成，因此服務功能的子類型判定規則也需要多種子類型規則同時支持。引入會話類型的標準環境(well-formed environments)，參照傳統會話類型的子類型規則，構造如下SST中的子類型規則，如表1所示。

表1 SST的子類型規則

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

在服務QoST-S子類型命題證明的基礎上，構造服務的子類型規則（Service-S）。

5 云服務替換性判定

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

5.1 替換性命題構造與服務一致性判定

根據會話類型的相關定義，云服務替換性命題可以等價為云服務在類型理論體系中的子類型命題，由此依據類型論，服務替換性命題構造如下

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

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

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

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

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

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

前提條件為

兼容性判定規則為

目標命題證明為

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

前提條件為

兼容性判定規則為

目標命題證明

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

5.3 面向云服務組合的服務替換

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

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

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

6 應用實例及其效果分析

6.1 服務替換性判定實例

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

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}}

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

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

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

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

以1)和3)為例：

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

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

6.2 面向服務組合的應用效果分析

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

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

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

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

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

7 結束語

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

[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 服務發現[J]. 計算機學報, 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] 常亮, 史忠植, 陳立民, 等.一類擴展的動態描述邏輯[J].軟件學報, 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服務組合的描述和驗證[J]. 計算機學報, 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] 印瑩, 張斌, 張錫哲. 面向組合服務動態自適應的事務級主動伺機服務替換算法[J].計算機學報, 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] 王海艷,李思瑞. 基于組合上下文的服務替換方法[J]. 通信學報,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] 劉方方, 史玉良, 張亮, 等.基于進程代數的Web服務合成的替換分析[J]. 計算機學報, 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 服務行為一致性與相容性判定[J]. 電子學報, 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

國家自然科學基金資助項目(No.61370229, No.61370178)；國家科技支撐計劃基金資助項目(No.2013BAH72B01)；教育部-中國移動基金資助項目（No.MCM20130651）；廣東省自然科學基金資助項目（No.S2013010015178）；廣東省科技計劃基金資助項目（No.2014B010103004, No.2014B010117007, No.2015A030401087, No.2015B010110002）；廣東省教育廳科技創新基金資助項目（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-），男，湖南臨澧人，廣東科學技術職業學院副教授，主要研究方向為云服務、計算機應用技術、多媒體技術等。

黃昌勤（1972-），男，湖南常德人，華南師范大學教授、博士生導師，主要研究方向為可信云服務、語義智能、大數據技術及其教育應用等。

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

聶瑞華（1963-），男，江西樟樹人，華南師范大學教授，主要研究方向為計算機網絡及應用、云計算與大數據等。

湯庸（1964-），男，湖南張家界人，華南師范大學教授、博士生導師，主要研究方向為社交網絡與大數據應用、時態數據與知識工程、協同計算等。

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