基于擴展進(jìn)程代數(shù)的云制造服務(wù)組合建模與QoS評價

李永湘，姚錫凡，2＋，徐 川，張 潔，李 彬

（1．華南理工大學(xué) 機械與汽車工程學(xué)院，廣東 廣州 510640；2．吉林大學(xué) 汽車仿真與控制國家重點實驗室，吉林 長春 130025）

0 引言

近年來，制造業(yè)與高新技術(shù)的融合變得愈加迅速和緊密。為提高企業(yè)的核心競爭力，加強企業(yè)對市場需求的快速響應(yīng)能力，國內(nèi)外學(xué)者對面向服務(wù)的制造進(jìn)行了探索研究，形成了不同稱謂的制造模式，如英國的產(chǎn)品服務(wù)系統(tǒng)（pr oduct service system）［1］、美國的基于服務(wù)制造（service－based manufacturing）［2］、澳大利亞的服務(wù)增強制造（ser vice enhanced manufacturing）［3］、日 本 的 面 向 服 務(wù) 制 造（ser vice－oriented manuf act uring）［4］，以 及 國 內(nèi) 的“服務(wù)型制造”［5］。隨著云計算的誕生與發(fā)展，中國工程院李伯虎院士等提出面向服務(wù)的網(wǎng)絡(luò)化制造新模式——云制造［6］。

云制造是一種利用網(wǎng)絡(luò)和云制造服務(wù)平臺，按用戶需求組織網(wǎng)上制造資源（制造云），為用戶提供各類按需制造服務(wù)的一種網(wǎng)絡(luò)化制造新模式［6］。云制造融合現(xiàn)有網(wǎng)絡(luò)化制造和服務(wù)技術(shù)、云計算、云安全、物聯(lián)網(wǎng)等技術(shù)，通過虛擬化技術(shù)，對各類制造資源（制造設(shè)備、設(shè)計、材料、數(shù)據(jù)等）進(jìn)行虛擬化封裝，發(fā)布為Web服務(wù)，進(jìn)入云資源池，對云資源池Web服務(wù)進(jìn)行選擇、組合等操作，為客戶提供所需制造服務(wù)［7］。單個Web服務(wù)往往不能滿足客戶需求，而需要由多個Web服務(wù)組合完成。由于網(wǎng)絡(luò)傳輸?shù)牟煌阅芤约敖M合中服務(wù)本身的異構(gòu)性等，使得Web服務(wù)組合變得復(fù)雜而易錯［8］。為確保 Web組合服務(wù)能正常執(zhí)行并滿足服務(wù)組合的預(yù)期目標(biāo)，需在組合服務(wù)正式執(zhí)行前對其進(jìn)行驗證。

進(jìn)程代數(shù)具有嚴(yán)密定義的形式化語義，能夠?qū)⒎?wù)的動態(tài)行為與操作語義聯(lián)系起來，并能對其性質(zhì)進(jìn)行驗證，因此越來越多地被工業(yè)界和學(xué)術(shù)界用于基于流程組合服務(wù)的建模和驗證。經(jīng)典的進(jìn)程代數(shù)有 CCS（calcul us of communication system）［9］，COWS（calculus f or orchestration of Web service），π－演算 （Pi calcul us）［10］，CSP （communicating sequential processes）［11］，ACP （algebra of communicating process）［12］等。文獻(xiàn)［10］使用 Pi演算進(jìn)行Web服務(wù)組合描述并使用驗證工具M(jìn)WB（mobile wor kbench）進(jìn)行驗證［10］。文獻(xiàn)［13］在業(yè)務(wù)過程執(zhí)行 語 言 （Business Process Execution Language，BPEL）和COWS之間建立映射，從而可以借助COWS的驗證工具CMC（COWS model checker）對BPEL程序的正確性進(jìn)行驗證［13－14］。然而，這些運用進(jìn)程代數(shù)進(jìn)行Web服務(wù)的研究都集中在Web服務(wù)的功能建模和正確性驗證方面，沒有考慮到云制造Web服務(wù)的非功能性需求，如時間、費用等。而在云制造中，對非功能性進(jìn)行建模以支持優(yōu)化和決策正越來越受到關(guān)注，有必要對進(jìn)程代數(shù)進(jìn)行非功能性擴展研究。COWS綜合并發(fā)展了π－演算等的結(jié)構(gòu)和特征，例如異步交互、組合同步和模式匹配等，概念簡潔、邏輯性強，可以滿足Web服務(wù)描述要求［15－17］。本文在COWS的基礎(chǔ)上，提出一種擴展了服務(wù)質(zhì)量（Quality of Service，QoS）信息的進(jìn)程代數(shù)XPC4CMSC（extended pr ocess calcul us f or cloud manuf act uring ser vice co mposition），使其能在對云制造服務(wù)組合進(jìn)行描述和驗證的同時，還能對組合的QoS進(jìn)行分析，分析結(jié)果可以作為選擇服務(wù)組合的參考依據(jù)。

1 擴展進(jìn)程代數(shù)XPC4CMSC

1．1 QoS定義

首先討論QoS在XPC4CMSC中的含義。XPC4CMSC中，QoS可用一個6維數(shù)組表示。

定義1 非功能屬性模型QoS是一個6維數(shù)組，QoS＝（Te，Ce，Re，Ae，LTe，LCe）。其中：

Te是服務(wù)操作響應(yīng)時間函數(shù)，其值為輔助工作（例如工件的裝夾等）所需時間函數(shù)Tauxiliary與制造服務(wù)執(zhí)行時間函數(shù)Texecution之和，Te＝Tauxiliary＋Texecution。

Ce是使用該服務(wù)操作應(yīng)付費用函數(shù)，其值為服務(wù)提供者標(biāo)出的服務(wù)收費Cprovider與第三方所要收取的認(rèn)證服務(wù)等費用Cagent，Ce＝Cprovider＋Cagent。

Re是該服務(wù)操作的可靠性函數(shù)。高質(zhì)量的云制造服務(wù)應(yīng)當(dāng)是穩(wěn)定的、可靠的，擁有高的執(zhí)行成功率。可靠性可表示被調(diào)用服務(wù)總次數(shù)Rinvoke中服務(wù)成功執(zhí)行次數(shù)Rexecution所占百分比，Re＝Rexecution／Rinvoke。

Ae是該服務(wù)操作的可用性函數(shù)，是當(dāng)用戶需要時該服務(wù)即能工作的概率。

LTe是使用服務(wù)過程中的物流時間函數(shù)，由于云制造服務(wù)的特性，不僅服務(wù)執(zhí)行時間比一般的Web服務(wù)執(zhí)行時間長，而且往往受物流時間的制約，故有必要考慮物流時間因素對服務(wù)質(zhì)量的影響。

LCe是使用服務(wù)過程中所要花費的物流費用函數(shù)。

XPC4CMSC中，以優(yōu)化QoS為目標(biāo)的服務(wù)組合方案選擇問題為多目標(biāo)問題。組合模型中第k個任務(wù)的候選服務(wù)（Sk，1，Sk，2，…，Sk，n）的 Q oS矩陣表示為

在模型中，Te，Ce，LTe與LCe是負(fù)向質(zhì)量元素，即函數(shù)值越大，服務(wù)質(zhì)量越差。Re與Ae是正向質(zhì)量元素，即函數(shù)值越大，服務(wù)質(zhì)量越好。為了統(tǒng)一6種質(zhì)量元素的量綱與方向，在計算組合模型的綜合質(zhì)量之前，需要對QoS元素進(jìn)行標(biāo)準(zhǔn)化處理。

對于正向質(zhì)量元素，選擇式（2）進(jìn)行標(biāo)準(zhǔn)化處理［18］：

對于負(fù)向質(zhì)量元素，選擇式（3）進(jìn)行標(biāo)準(zhǔn)化處理［18］：

式（2）、式（3）中：i表示云制造資源池中滿足客戶要求的候選服務(wù)序號，1≤i≤n；j表示質(zhì)量元素序號，1≤j≤6。

根據(jù)式（2）、式（3）可求得式（1）的標(biāo)準(zhǔn)化矩陣Zk。將式（1）進(jìn)行標(biāo)準(zhǔn)化處理，得組合模型中第k個任務(wù)候選服務(wù)的標(biāo)準(zhǔn)化QoS矩陣

可用式（4）計算每個候選服務(wù)Sk，i的QoS綜合評價值

式中：λk，j為第k個任務(wù)中第j維質(zhì)量元素的加權(quán)因相應(yīng)質(zhì)量元素對綜合服務(wù)質(zhì)量評價的影響程度。對式（5）作Max運算，可求得資源池中具有最優(yōu)QoS綜合評價值的服務(wù)。

1．2 XPC4CMSC語法簡介

XPC4CMSC語法如表1所示，其基本要素是伙伴和操作［19－20］?；锇槊Q用字母p，p′，…表示，操作名稱用字母o，o′，…表示，通信節(jié)點由伙伴名稱和操作名稱組成。的優(yōu)先級按由高到低的順序規(guī)定如下：一元運算符、前綴運算符、選擇運算符、并發(fā)組合運算符。

表1 COWS語法

1．3 XPC4CMSC操作語義簡介

XPC4CMSC操作語義是根據(jù)結(jié)構(gòu)等價規(guī)則和標(biāo)簽躍遷關(guān)系來定義的。如表2所示，結(jié)構(gòu)等價規(guī)則是由一套公式所表達(dá)的最小等價關(guān)系，可識別兩個語句結(jié)構(gòu)不同而本質(zhì)上代表相同服務(wù)的項式［20］。

表2 COWS結(jié)構(gòu)等價規(guī)則

1． 4 典型Web服務(wù)組合結(jié)構(gòu)的XPC4CMSC描述與QoS計算

定義2 Web服務(wù)組合的XPC4CMSC語義模型是一個5元組，MoSC＝（Endpoint，Activity，Tr ansition，Label，QoS）。其中：End point是 W eb服務(wù)節(jié)點，即由伙伴名稱和操作名稱組成的集合；Activity是調(diào)用活動、接收活動等的集合；Tr ansition是變遷函數(shù)；Label是標(biāo)簽函數(shù)；QoS是上面定義的Web服務(wù)的非功能屬性模型。

用XPC4CMSC語言描述圖1所示的服務(wù)模型如下：

1．4．1 Sequence組合

如圖2所示，不同服務(wù)操作之間按照先后順序依次執(zhí)行，形成一條有序執(zhí)行的串行鏈，后面服務(wù)操作需等其前面的Web服務(wù)執(zhí)行完畢，并滿足變遷觸發(fā)條件時才能執(zhí)行。圖2所示的服務(wù)模型用XPC4CMSC語言描述如下：

1．4．2 Parallel組合

如圖3所示，一組服務(wù)操作并發(fā)執(zhí)行，只有當(dāng)所有服務(wù)操作執(zhí)行后，Parallel組合服務(wù)操作才算完成，變遷For k和Join起連接作用，只有當(dāng)活動Activity1和Activity2全都執(zhí)行完，才能觸發(fā)變遷Join。圖3所示的服務(wù)模型用XPC4CMSC語言描述如下：

Parallel組合服務(wù)響應(yīng)時間為：TI MEparallel＝Max（Te（xi））；

1．4．3 Choice組合

如圖4所示，在一組服務(wù)中任意選擇一個執(zhí)行，任意一個服務(wù)操作都有可能被選擇執(zhí)行，當(dāng)被選操作執(zhí)行完成，則說明Choice組合服務(wù)操作執(zhí)行完成。圖4所示的服務(wù)模型用XPC4CMSC語言描述如下：

Choice組合服務(wù)響應(yīng)時間為：TI MEchoice＝

上述公式中，θi是Choice組合中第i個服務(wù)操示該服務(wù)操作必然被選擇；θi＝0表示該服務(wù)操作必然不被選擇。

2 服務(wù)組合的形式化驗證方案

限于篇幅，有關(guān)服務(wù)組合的正確性驗證、可達(dá)性驗證等在此不進(jìn)行闡述，僅對服務(wù)組合QoS一致性驗證算法進(jìn)行研究。驗證服務(wù)組合QoS一致性的目的是保證組合方案中的組合服務(wù)在響應(yīng)時間、執(zhí)行費用、可靠性、可用性、物流時間、物流費用方面能夠分別滿足客戶的需求，并使組合服務(wù)的標(biāo)準(zhǔn)化QoS綜合評價值也能達(dá)到指定要求，從而得到基于QoS的最優(yōu)服務(wù)組合方案。

2．1 服務(wù)組合QoS評價算法

根據(jù)上述建立的形式模型，編寫服務(wù)組合QoS評價算法代碼如下：LCe＿t hreshold分別對應(yīng)響應(yīng)時間、執(zhí)行費用、可靠性、可用性、物流時間、物流費用；SCEV4 QOS＿t hreshold對應(yīng)標(biāo)準(zhǔn)化QoS綜合評價值。

（2）語句4是根據(jù)領(lǐng)域特征和實際情況，輸入組合服務(wù)的QoS模型中每個非功能屬性在綜合質(zhì)量中相應(yīng)的權(quán)值，w1，w2，w3，w4，w5，w6分別對應(yīng)響應(yīng)時間、執(zhí)行費用、可靠性、可用性、物流時間和物流費用的加權(quán)因子。

（3）語句5是滿足組合規(guī)劃功能的備選組合服務(wù)，依次進(jìn)行驗證。

（4）語句6是調(diào)用函數(shù) QoSof Service Co mosition，得到組合服務(wù)QoS模型中的各非功能屬性的值。

（5）語句7～18是根據(jù)客戶輸入的閾值，分別判斷組合服務(wù)的各非功能屬性是否滿足客戶的要求。

（6）語句19～44是求出各組合服務(wù)的各非功能屬性的最大值和最小值，為QoS模型中各元素的標(biāo)準(zhǔn)化作準(zhǔn)備。

（7）語句45～69是對QoS模型中各非功能元素進(jìn)行標(biāo)準(zhǔn)化，并求出組合服務(wù)的綜合質(zhì)量評價值，判斷是否達(dá)到客戶提出的綜合質(zhì)量要求。

上述算法中，組合服務(wù)QoS模型中的各非功能屬性值計算的時間復(fù)雜度為T1＝O（n）；語句5～69是循環(huán)語句，當(dāng)服務(wù)組合規(guī)模足夠大時，忽略其他低次冪項式，可得總的算法時間復(fù)雜度為T2＝O（n2）。

2．2 形式化驗證方案

形式化驗證方案如圖5所示。CMC是針對Web服務(wù)編制進(jìn)程代數(shù)語言開發(fā)的一種動態(tài)模型驗證程序［21］，可驗證XPC4CMSC指定服務(wù)性質(zhì)。根據(jù)客戶需求建立組合服務(wù)活動圖，用XPC4CMSC語言描述服務(wù)組合的語義模型。然后將XPC4CMSC文件加載至CMC模型驗證軟件中進(jìn)行形式化驗證，捕捉組合服務(wù)的特殊性質(zhì)，如可執(zhí)行性、正確性、可靠性等。

3 用例分析

以兩個車間的6臺機器和10個待加工零件組合的柔性車間調(diào)度問題FT10為例，說明基于XPC4CMSC的服務(wù)組合形式化建模與驗證過程。客戶選擇在兩個車間的6臺機器上加工10個零件，每個零件有3道工序，加工原材料從客戶處發(fā)出，零件加工完后需運回客戶處。10個零件的加工任務(wù)分別表示為Job＿01，Job＿02，Job＿03，Job＿04，Job＿05，Job＿06，Job＿07，Job＿08，Job＿09，Job＿10，6 臺 機器分別稱為 Machine＿01，Machine＿02，Machine＿03，Machine＿04，Machine＿05，Machine＿06，其加工時間、費用、可靠性和可用性如表3所示，單個零件運送的物流時間、物流費用如表4所示。

表3 FT10加工時間、加工費用、可靠性和可用性表

續(xù)表3 J 4 O42 （6，9，1，1） （4，4，0．98，0．98） （5，6，1，0．98） （7，11，1，1） （5，5，0．98，0．98） （6，7，0．98，1）J 4 O43 （1，4，1，1） （3，3，0．98，0．98） （3，4，1，0．98） （2，3，1，1） （4，4，0．98，0．98） （4，5，0．98，1）J 5 O51 （3，5，1，1） （4，4，0．98，0．98） （5，6，1，0．98） （2，3，1，1） （3，2，0．98，0．98） （4，6，0．98，1）J 5 O52 （3，4，1，1） （2，1，0．98，0．98） （3，4，1，0．98） （3，4，1，1） （2，1，0．98，0．98） （4，6，0．98，1）J 5 O53 （2，3，1，1） （5，5，0．98，0．98） （4，6，1，0．98） （1，3，1，1） （4，2，0．98，0．98） （5，7，0．98，1）J 6 O61 （2，5，1，1） （4，4，0．98，0．98） （1，2，1，0．98） （3，4，1，1） （5，3，0．98，0．98） （2，4，0．98，1）J 6 O62 （5，8，1，1） （4，4，0．98，0．98） （7，8，1，0．98） （4，6，1，1） （3，1，0．98，0．98） （6，8，0．98，1）J 6 O63 （3，7，1，1） （6，6，0．98，0．98）（10，11，1，0．98） （4，5，1，1） （7，5，0．98，0．98）（11，13，0．98，1）J 7 O71 （4，8，1，1） （5，5，0．98，0．98） （3，5，1，0．98） （5，8，1，1） （6，4，0．98，0．98） （5，7，0．98，1）J 7 O72 （5，9，1，1） （4，4，0．98，0．98） （6，7，1，0．98） （4，7，1，1） （3，1，0．98，0．98） （5，7，0．98，1）J 7 O73 （12，18，1，1） （8，8，0．98，0．98）（10，12，1，0．98） （13，18，1，1） （9，7，0．98，0．98）（12，14，0．98，1）J 8 O81 （10，14，1，1） （8，8，0．98，0．98）（9，11，1，0．98） （9，12，1，1） （7，6，0．98，0．98） （9，11，0．98，1）J 8 O82 （5，9，1，1） （3，3，0．98，0．98） （4，5，1，0．98） （6，9，1，1） （4，4，0．98，0．98） （5，6，0．98，1）J 8 O83 （2，3，1，1） （4，4，0．98，0．98） （4，5，1，0．98） （2，1，1，1） （3，3，0．98，0．98） （3，4，0．98，1）J 9 O91 （4，7，1，1） （3，5，0．98，0．98） （5，5，1，0．98） （3，6，1，1） （3，8，0．98，0．98） （6，5，0．98，1）J 9 O92 （4，7，1，1） （4，6，0．98，0．98） （4，4，1，0．98） （5，8 1，1） （2，7，0．98，0．98） （3，2，0．98，1）J 9 O93 （11，14，1，1） （9，9，0．98，0．98） （8，8，1，0．98） （10，13，1，1） （9，9，0．98，0．98） （9，8，0．98，1）J 10 O101 （8，11，1，1） （9，9，0．98，0．98） （8，8，1，0．98） （9，12，1，1） （7，9，0．98，0．98） （7，8，0．98，1）J 10 O102 （4，6，1，1） （4，6，0．98，0．98） （3，3，1，0．98） （3，6，1，1） （4，7，0．98，0．98） （4，5，0．98，1）J 10 O103 （2，4，1，1） （2，1，0．98，0．98） （4，4，1，0．98） （3，5，1，1） （2，1，0．98，0．98） （3，4，0．98，1）

表4 FT10單個零件的物流時間和物流費用表

建立上述零件加工組合服務(wù)的活動圖，如圖6所示。模型主要由10個服務(wù)即Sv＿01，Sv＿02，Sv＿03，Sv＿04，Sv＿05，Sv＿06，Sv＿07，Sv＿08，Sv＿09，Sv＿10并發(fā)組合而成。10個服務(wù)各由3個二代子服務(wù)順序組合而成，例如Sv＿01由Sv＿0101，Sv＿0102，Sv＿0103順序組合而成，根據(jù)零件工藝先后順序分別調(diào)用Sv＿0101，Sv＿0102，Sv＿0103這3個服務(wù)，前面的服務(wù)成功執(zhí)行完后才能執(zhí)行排在其后的服務(wù)，即Sv＿0102的執(zhí)行必須滿足條件Sv＿0101 Answer＝y(tǒng)es，Sv＿0103的執(zhí)行必須滿足條件Sv＿0102 Ans wer＝y(tǒng)es。二代子服務(wù)又各由6個三代子服務(wù)組合而成，如圖 7 所示，Sv＿0101 由 Sv＿010101，Sv＿010102，Sv＿010103，Sv＿010104，Sv＿010105，Sv＿010106經(jīng)選擇組合而成，根據(jù)防衛(wèi)函數(shù)［guard］決定選擇調(diào)用其中的一個服務(wù)執(zhí)行。為使活動圖清晰易讀，圖6和圖7中省略了模型所包含的異常處理exception、事件處理event、補償機制co mpensation等，這些處理機制可保證服務(wù)在執(zhí)行過程中出現(xiàn)不正常情況時能做出相應(yīng)的處理措施。根據(jù)活動圖編寫XPC4CMSC文件，部分編碼如下：

．e2＿06！〈true〉＋ e2＿07〈true〉．e2＿07！〈tr ue〉））

．（（e2＿02？〈true〉．［t2＿08］（［Sv＿010101］

｜t2＿08！〈Machine＿01Answer＝y(tǒng)es〉．e2＿08！〈guard2＿08〉）

＋ （e2＿03？〈true〉．［t2＿09］（［Sv＿010102］

｜t2＿09！〈Machine＿02 Ans wer＝y(tǒng)es〉．e2＿09！〈guard2＿09〉）

＋ （e2＿04？〈tr ue〉．［t2＿10］（［Sv＿010103］

｜t2＿10！〈Machine＿03 Ans wer＝y(tǒng)es〉．e2＿10！〈guard2＿10〉）

＋ （e2＿05？〈true〉．［t2＿11］（［Sv＿010104］

｜t2＿11！〈Machine＿04Answer＝y(tǒng)es〉．e2＿11！〈guard2＿11〉）

＋ （e2＿06？〈true〉．［t2＿12］（［Sv＿010105］

｜t2＿12！〈Machine＿05Answer＝y(tǒng)es〉．e2＿12！〈guard2＿12〉）

＋ （e2＿07？〈true〉．［t2＿13］（［Sv＿010106］

｜t2＿13！〈Machine＿06Answer＝y(tǒng)es〉．e2＿13！〈guard2＿13〉））

．e2＿08？〈tr ue〉．e2＿14！〈guar d2＿14〉

＋e2＿09？〈true〉．e2＿14！〈guard2＿14〉

＋e2＿10？〈true〉．e2＿14！〈guard2＿14〉

＋e2＿11？〈true〉．e2＿14！〈guard2＿14〉

＋e2＿12？〈tr ue〉．e2＿14！〈guar d2＿14〉

＋e2＿13？〈true〉．e2＿14！〈guard2＿14〉

……

最后，將XPC4CMSC文件加載至CMC模型驗證程序中進(jìn)行形式化驗證，如圖8所示。給定QoS元素加權(quán)因子分別為0．3，0．3，0．1，0．1，0．1，0．1；閾值分別為40，165，0．7，0．7，105，55；標(biāo)準(zhǔn)化 QoS綜合評價閾值為0．7。形式化驗證結(jié)果如表5所示。

表5結(jié)果表明，組合服務(wù)1的響應(yīng)時間和執(zhí)行費用均未滿足客戶要求，如表5中的帶下劃線值；組合服務(wù)2的執(zhí)行費用最高，嚴(yán)重超標(biāo)；組合服務(wù)3具有較短的響應(yīng)時間，但其物流時間和物流費用都沒有達(dá)到客戶要求；組合服務(wù)4與組合服務(wù)5的執(zhí)行費用都未達(dá)到要求；組合服務(wù)6與組合服務(wù)8的物流時間都超標(biāo)；組合服務(wù)7的響應(yīng)時間偏長；組合服務(wù)9的綜合評價不合格；組合服務(wù)10、組合服務(wù)11和組合服務(wù)12的六種質(zhì)量元素都在閾值內(nèi)，組合服務(wù)10有最短的響應(yīng)時間，組合服務(wù)11有最高的可靠性，但組合服務(wù)12的執(zhí)行費用、物流時間和物流費用都比前面二者好，故組合服務(wù)12的標(biāo)準(zhǔn)化QoS值最高，是最優(yōu)的服務(wù)組合方案。圖9為組合服務(wù)12的服務(wù)調(diào)度甘特圖。上述結(jié)果也表明基于XPC4CMSC的云制造服務(wù)組合建模及形式化驗證方案是可行的。

表5 形式化驗證結(jié)果

4 相關(guān)服務(wù)組合方法比較

當(dāng)前服務(wù)組合方法有多種，如文獻(xiàn)［10］采用Pi演算進(jìn)行Web服務(wù)組合建模與驗證；文獻(xiàn)［17］設(shè)計了基于統(tǒng)一建模語言（Unified Modeling Language，UML）的服務(wù)組合建模方法；文獻(xiàn)［22］將云制造服務(wù)組合問題視為一個多目標(biāo)規(guī)劃問題，并利用自適應(yīng)粒子群算法來解決該多目標(biāo)規(guī)劃問題。而本文考慮了響應(yīng)時間、執(zhí)行費用等6個屬性因子，提出一種基于擴展進(jìn)程代數(shù)XPC4CMSC的云制造服務(wù)組合建模與驗證方法，該方法側(cè)重于服務(wù)組合的描述、建模、形式化驗證與屬性分析，表6給出了該方法與其他服務(wù)組合方法的比較。從表中可以看出，XPC4CMSC滿足服務(wù)組合的需求項數(shù)最多。

表6 服務(wù)組合方法比較

5 結(jié)束語

一個云制造組合服務(wù)由一組子服務(wù)組成，被組合的子服務(wù)彼此并發(fā)交互以完成客戶請求，而彼此間的交互通過通信和交換信息來完成。云制造服務(wù)組合的重要問題之一是如何保證組合的正確性。解決該問題的重要手段就是為云制造服務(wù)組合提供一個形式化的模型以進(jìn)行模型檢查和驗證。擴展進(jìn)程代數(shù)可用來作為描述服務(wù)組合的形式化工具。本文提出的基于XPC4CMSC的云制造服務(wù)組合建模與形式化驗證方案及QoS評價算法，是對進(jìn)程代數(shù)非功能屬性驗證研究的有益補充，也為云制造服務(wù)組合的研究提供了一種新的視角和途徑，后續(xù)研究將考慮如何動態(tài)處理云制造服務(wù)組合中QoS元素的加權(quán)因子以及算法優(yōu)化等。

［1］ GOTTBERG A，LONGHURST P J，COOK M B．Exploring the potential of product service systems to achieve household waste prevention on new housing developments in the UK［J］．Waste Management ＆Research，2010，28（3）：228－235．

［2］ LEE M，YOON H，SHIN H，et al．Intelligent dynamic workflow support for a ubiquitous Web service－based manufacturing environment［J］．Journal of Intelligent Manufacturing，2009，20（3）：295－302．

［3］ TO C K，LEUNG C S．Service－enhanced manufacturing：a study of perceived service quality of apparel manufacturers［J］．Journal of Fashion Marketing and Management，2001，5（4）：313－323．

［4］ FUJIMOTO J，UMEDA Y，TAMURA T，et al．Development of service－oriented products based on the inverse manufacturing concept［J］．Enviromental Science Technology，2003，37（2）：5398－5406．

［5］ SUN Linyan，LI Gang，JIANG Zhibin，et al．Service－embedded manufacturing：advanced manufacturing paradigm in 21st century［J］．China Mechanical Engineering，2007，18（19）：2307－2312（in Chinese）．［孫林巖，李 剛，江志斌，等．21世紀(jì)的先進(jìn)制造模式——服務(wù)型制造［J］．中國機械工程，2007，18（19）：2307－2312．］

［6］ LI Bohu，ZHANG Lin，WANG Shilong，et al．Cloud manufacturing：a new service－oriented manufacturing model［J］．Computer Integrated Manufacturing Systems，2010，16（1）：1－7，16（in Chinese）．［李伯虎，張 霖，王時龍，等．云制造——面向服務(wù)的網(wǎng)絡(luò)化制造新模式［J］．計算機集成制造系統(tǒng)，2010，16（1）：1－7，16．］

［7］ TAO Fei，ZHANG Lin，GUO Hua，et al．Typical characteristics of cloud manufacturing and several key issues of cloud service composition［J］．Computer Integrated Manufacturing Systems，2011，17（3）：477－486（in Chinese）．［陶 飛，張霖，郭 華，等．云制造特征及云服務(wù)組合關(guān)鍵問題研究［J］．計算機集成制造系統(tǒng)，2011，17（3）：477－486．］

［8］ LUO Junzhou，JIN Jiahui，SONG Aibo，et al．Cloud computing：architecture and key technologies［J］．Journal on Communications，2011，32（7）：3－21（in Chinese）．［羅軍舟，金嘉暉，宋愛波，等．云計算：體系架構(gòu)與關(guān)鍵技術(shù)［J］．通信學(xué)報，2011，32（7）：3－21．］

［9］ LIU C H，CHEN S L，KUO J Y，et al．A flow graph－based test model for OWL－S Web Services［C］／／Proceedings of International Conference on Machine Learning and Cybernetics．Washington，D．C．，USA：IEEE，2011：897－902．

［10］ HLAOUI Y B，BENAYED L J．A model transformation approach based on homomorphic mappings between UML activity diagrams and BPEL4WS specifications of grid service workflows［C］／／Proceedings of International Computer Software and Applications Conference．Washington，D．C．，USA：IEEE，2011：243－248．

［11］ MA Z M，ZHANG F，YAN L，et al．Representing and reasoning on fuzzy UML models：a description logic approach［J］．Expert Systems with Applications，2011，38（3）：2536－2549．

［12］ ZHANG X G，LIU H B．Formal verification for CCML based Web service composition［J］．Information Technology Journal，2011，10（9）：1692－1700．

［13］ NIELSON H R，NIELSON F．A monotone framework for CCS［J］．Computer Languages，Systems and Structures，2009，35（4）：365－394．

［14］ VIRY P．Parallel and distributed programming extensions for mainstream languages based on pi－calculus［C］／／Proceedings of the Annual ACM Symposium on Principles of Distributed Computing．New York，N．Y．，USA：ACM，2011：343－344．

［15］ MANZONETTO G，SALIBRA，A．Applying universal algebra to lambda calculus［J］．Journal of Logic and Computation，2010，20（4）：877－915．

［16］ LANGE R，MANCORIDIS S．Thr2csp：toward transforming threads into communicating sequential processes［C］／／Proceedings of the 9th IEEE International Working Conference on Source Code Analysis and Manipulation．Washington，D．C．，USA：IEEE，2009：3－12．

［17］ CHIMISLIU V，WOTAWA F．Abstracting timing information in UML state charts via temporal ordering and LOTOS［C］／／Proceedings of International Conference on Software Engineering．New York，N．Y．，USA：ACM，2011：8－14．

［18］ LAPAFULA A，PUGLIESE R，TIEZZI F．A calculus for orchestration of web services［J］．Lecture Notes in Computer Science，2007，4421：33－47．

［19］ LAPADULA A，PUGLIESE R，TIEZZI F．COWS：a timed service－oriented calculus［J］．Lecture Notes in Computer Science，2007，4711：275－290．

［20］ CAPPELLO I，QUAGLIA P．A tool for checking probabilistic properties of COWS services［J］．Lecture Notes in Computer Science，2010，6084：364－378．

［21］ LAPADULA A，PUGLIESE R，TIEZZI F．Service discovery and negotiation with COWS［J］．Electronic Notes in Theoretical Computer Science，2008，200（3）：133－154．

［22］ LIU Weining，LI Yiming，LIU Bo．Service composition in cloud manufacturing based on adaptive mutation particle swarm optimization［J］．Journal of Computer Applications，2012，32（10）：2869－2874，2878（in Chinese）．［劉衛(wèi)寧，李一鳴，劉 波．基于自適應(yīng)粒子群算法的制造云服務(wù)組合研究［J］．計算機應(yīng)用，2012，32（10）：2869－2874，2878．］