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

?

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

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

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

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

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

1 引言

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

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

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

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

2 語(yǔ)義會(huì)話類型

2.1 會(huì)話類型及其語(yǔ)義擴(kuò)展

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

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

SST對(duì)傳統(tǒng)會(huì)話類型的擴(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ù)常見(jiàn)的消息概念抽取出來(lái)，將其完整建立在旅行服務(wù)本體中（如圖1所示）；對(duì)于Op類型構(gòu)造，將領(lǐng)域本體中概念的常用的操作動(dòng)作進(jìn)行抽取，形成旅行服務(wù)操作動(dòng)作的枚舉集合Action={Cancel,Book,Refund,…}set。

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

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

Ticket=

Address=

Vehicle=

Time=

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

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

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

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

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

{,}>,,}>}

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

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

規(guī)則1 SimpleType-S簡(jiǎn)單數(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ò)規(guī)則推導(dǎo)得出消息之間的準(zhǔn)確子類型關(guān)系。

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

操作類型Op表達(dá)原子服務(wù)對(duì)外發(fā)起調(diào)用、或受到外界調(diào)用時(shí)的操作語(yǔ)義，通常作為成員出現(xiàn)在Selection類型和Branching類型中。一個(gè)操作的語(yǔ)義通常包括{發(fā)起者，動(dòng)作，對(duì)象}3部分，發(fā)起者對(duì)本研究SST的操作語(yǔ)義沒(méi)有影響，在構(gòu)造中省略。因此，本研究將Op構(gòu)造為動(dòng)作與對(duì)象的笛氏積，其中，動(dòng)作由動(dòng)作集合中元素描述，而對(duì)象則利用本體中的概念描述。構(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)，在高度動(dòng)態(tài)的云計(jì)算環(huán)境下尤顯重要。與第2節(jié)類似，建立QoS本體，以便利用類型論建模QoS，支持服務(wù)替換命題的證明。云服務(wù)具有資源綁定高度動(dòng)態(tài)、宿居環(huán)境多樣、按需付費(fèi)等特性，需選取相應(yīng)的特征性指標(biāo)來(lái)建模云服務(wù)QoS。本文參照已有研究，僅選取價(jià)格、可靠性和云服務(wù)等級(jí)3項(xiàng)指標(biāo)做針對(duì)性地分析與建模。

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

QoS =

Price=

Reliability =

ServiceLevel=

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

前提條件為

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

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

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

前提條件為

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

目標(biāo)命題證明

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

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

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

鑒于云計(jì)算環(huán)境的特殊性，在云服務(wù)組合中服務(wù)替換改變依據(jù)傳統(tǒng)服務(wù)檢查等常規(guī)觸發(fā)方法，將以云服務(wù)上下文變化為觸發(fā)事件；同時(shí)在替換判定中，應(yīng)用前述基于類型論的行為功能語(yǔ)義、QoS及功能兼容性判定，必要時(shí)啟用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ù)檢測(cè)事件；3) IF檢測(cè)到組合服務(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)用實(shí)例及其效果分析

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

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

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個(gè)子判定命題。其中，QoS部分為數(shù)值比較，此處不作展開(kāi)。1<:2命題的證明思路如下。

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

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

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

以1)和3)為例：

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

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

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

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

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

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

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

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

7 結(jié)束語(yǔ)

云服務(wù)選擇與替換對(duì)云應(yīng)用至關(guān)重要，其中，對(duì)云服務(wù)動(dòng)態(tài)行為功能與QoS進(jìn)行準(zhǔn)確描述，是判斷服務(wù)行為可替換性的前提條件，也是云服務(wù)快速自動(dòng)和可靠組合的重要基礎(chǔ)。本文提出擴(kuò)展后的語(yǔ)義會(huì)話類型SST，并對(duì)云服務(wù)QoS進(jìn)行分析與建模，構(gòu)造QoST類型，設(shè)計(jì)SST與QoST的子類型規(guī)則，以此實(shí)現(xiàn)云服務(wù)特征化描述，最終完成基于子類型規(guī)則的替換性命題和兼容性命題判定。實(shí)例分析和實(shí)驗(yàn)測(cè)試表明，該云服務(wù)替換性判定方法具有良好可行性，不僅能完成對(duì)服務(wù)替換性兼容性的有效驗(yàn)證，也能較好提高組合服務(wù)的執(zhí)行成功率。后續(xù)將本文方法運(yùn)用到服務(wù)組合方案的制定中，并對(duì)原子服務(wù)間一對(duì)多、多對(duì)多的替換方法進(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] 吳健, 吳朝暉, 李瑩, 等. 基于本體論和詞匯語(yǔ)義相似度的 Web 服務(wù)發(fā)現(xiàn)[J]. 計(jì)算機(jī)學(xué)報(bào), 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ò)展的動(dòng)態(tài)描述邏輯[J].軟件學(xué)報(bào), 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ù)組合的描述和驗(yàn)證[J]. 計(jì)算機(jī)學(xué)報(bào), 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ù)動(dòng)態(tài)自適應(yīng)的事務(wù)級(jí)主動(dòng)伺機(jī)服務(wù)替換算法[J].計(jì)算機(jī)學(xué)報(bào), 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é)報(bào),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ì)算機(jī)學(xué)報(bào), 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é)報(bào), 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

國(guó)家自然科學(xué)基金資助項(xiàng)目(No.61370229, No.61370178)；國(guó)家科技支撐計(jì)劃基金資助項(xiàng)目(No.2013BAH72B01)；教育部-中國(guó)移動(dòng)基金資助項(xiàng)目（No.MCM20130651）；廣東省自然科學(xué)基金資助項(xiàng)目（No.S2013010015178）；廣東省科技計(jì)劃基金資助項(xiàng)目（No.2014B010103004, No.2014B010117007, No.2015A030401087, No.2015B010110002）；廣東省教育廳科技創(chuàng)新基金資助項(xiàng)目（No.2012KJCX0037）；廣州市科技基金資助項(xiàng)目（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é)院副教授，主要研究方向?yàn)樵品?wù)、計(jì)算機(jī)應(yīng)用技術(shù)、多媒體技術(shù)等。

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

羅旋（1990-），男，湖南常德人，華南師范大學(xué)碩士生，主要研究方向?yàn)榉?wù)計(jì)算、云計(jì)算等。

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

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

梅曉勇（1974-），男，湖南常德人，博士，主要研究方向?yàn)榉?wù)計(jì)算、Petri網(wǎng)技術(shù)與可信計(jì)算等。