基于扩展进程代数的云制造服务组合建模与QoS评价

李永湘，姚锡凡，2＋，徐 川，张 洁，李 彬

（1．华南理工大学 机械与汽车工程学院，广东 广州 510640；2．吉林大学 汽车仿真与控制国家重点实验室，吉林 长春 130025）

0 引言

近年来，制造业与高新技术的融合变得愈加迅速和紧密。为提高企业的核心竞争力，加强企业对市场需求的快速响应能力，国内外学者对面向服务的制造进行了探索研究，形成了不同称谓的制造模式，如英国的产品服务系统（pr oduct service system）［1］、美国的基于服务制造（service－based manufacturing）［2］、澳大利亚的服务增强制造（ser vice enhanced manufacturing）［3］、日 本 的 面 向 服 务 制 造（ser vice－oriented manuf act uring）［4］，以 及 国 内 的“服务型制造”［5］。随着云计算的诞生与发展，中国工程院李伯虎院士等提出面向服务的网络化制造新模式——云制造［6］。

云制造是一种利用网络和云制造服务平台，按用户需求组织网上制造资源（制造云），为用户提供各类按需制造服务的一种网络化制造新模式［6］。云制造融合现有网络化制造和服务技术、云计算、云安全、物联网等技术，通过虚拟化技术，对各类制造资源（制造设备、设计、材料、数据等）进行虚拟化封装，发布为Web服务，进入云资源池，对云资源池Web服务进行选择、组合等操作，为客户提供所需制造服务［7］。单个Web服务往往不能满足客户需求，而需要由多个Web服务组合完成。由于网络传输的不同性能以及组合中服务本身的异构性等，使得Web服务组合变得复杂而易错［8］。为确保 Web组合服务能正常执行并满足服务组合的预期目标，需在组合服务正式执行前对其进行验证。

进程代数具有严密定义的形式化语义，能够将服务的动态行为与操作语义联系起来，并能对其性质进行验证，因此越来越多地被工业界和学术界用于基于流程组合服务的建模和验证。经典的进程代数有 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］等。文献［10］使用 Pi演算进行Web服务组合描述并使用验证工具MWB（mobile wor kbench）进行验证［10］。文献［13］在业务过程执行 语 言 （Business Process Execution Language，BPEL）和COWS之间建立映射，从而可以借助COWS的验证工具CMC（COWS model checker）对BPEL程序的正确性进行验证［13－14］。然而，这些运用进程代数进行Web服务的研究都集中在Web服务的功能建模和正确性验证方面，没有考虑到云制造Web服务的非功能性需求，如时间、费用等。而在云制造中，对非功能性进行建模以支持优化和决策正越来越受到关注，有必要对进程代数进行非功能性扩展研究。COWS综合并发展了π－演算等的结构和特征，例如异步交互、组合同步和模式匹配等，概念简洁、逻辑性强，可以满足Web服务描述要求［15－17］。本文在COWS的基础上，提出一种扩展了服务质量（Quality of Service，QoS）信息的进程代数XPC4CMSC（extended pr ocess calcul us f or cloud manuf act uring ser vice co mposition），使其能在对云制造服务组合进行描述和验证的同时，还能对组合的QoS进行分析，分析结果可以作为选择服务组合的参考依据。

1 扩展进程代数XPC4CMSC

1．1 QoS定义

首先讨论QoS在XPC4CMSC中的含义。XPC4CMSC中，QoS可用一个6维数组表示。

定义1 非功能属性模型QoS是一个6维数组，QoS＝（Te，Ce，Re，Ae，LTe，LCe）。其中：

Te是服务操作响应时间函数，其值为辅助工作（例如工件的装夹等）所需时间函数Tauxiliary与制造服务执行时间函数Texecution之和，Te＝Tauxiliary＋Texecution。

Ce是使用该服务操作应付费用函数，其值为服务提供者标出的服务收费Cprovider与第三方所要收取的认证服务等费用Cagent，Ce＝Cprovider＋Cagent。

Re是该服务操作的可靠性函数。高质量的云制造服务应当是稳定的、可靠的，拥有高的执行成功率。可靠性可表示被调用服务总次数Rinvoke中服务成功执行次数Rexecution所占百分比，Re＝Rexecution／Rinvoke。

Ae是该服务操作的可用性函数，是当用户需要时该服务即能工作的概率。

LTe是使用服务过程中的物流时间函数，由于云制造服务的特性，不仅服务执行时间比一般的Web服务执行时间长，而且往往受物流时间的制约，故有必要考虑物流时间因素对服务质量的影响。

LCe是使用服务过程中所要花费的物流费用函数。

XPC4CMSC中，以优化QoS为目标的服务组合方案选择问题为多目标问题。组合模型中第k个任务的候选服务（Sk，1，Sk，2，…，Sk，n）的 Q oS矩阵表示为

在模型中，Te，Ce，LTe与LCe是负向质量元素，即函数值越大，服务质量越差。Re与Ae是正向质量元素，即函数值越大，服务质量越好。为了统一6种质量元素的量纲与方向，在计算组合模型的综合质量之前，需要对QoS元素进行标准化处理。

对于正向质量元素，选择式（2）进行标准化处理［18］：

对于负向质量元素，选择式（3）进行标准化处理［18］：

式（2）、式（3）中：i表示云制造资源池中满足客户要求的候选服务序号，1≤i≤n；j表示质量元素序号，1≤j≤6。

根据式（2）、式（3）可求得式（1）的标准化矩阵Zk。将式（1）进行标准化处理，得组合模型中第k个任务候选服务的标准化QoS矩阵

可用式（4）计算每个候选服务Sk，i的QoS综合评价值

式中：λk，j为第k个任务中第j维质量元素的加权因相应质量元素对综合服务质量评价的影响程度。对式（5）作Max运算，可求得资源池中具有最优QoS综合评价值的服务。

1．2 XPC4CMSC语法简介

XPC4CMSC语法如表1所示，其基本要素是伙伴和操作［19－20］。伙伴名称用字母p，p′，…表示，操作名称用字母o，o′，…表示，通信节点由伙伴名称和操作名称组成。的优先级按由高到低的顺序规定如下：一元运算符、前缀运算符、选择运算符、并发组合运算符。

表1 COWS语法

1．3 XPC4CMSC操作语义简介

XPC4CMSC操作语义是根据结构等价规则和标签跃迁关系来定义的。如表2所示，结构等价规则是由一套公式所表达的最小等价关系，可识别两个语句结构不同而本质上代表相同服务的项式［20］。

表2 COWS结构等价规则

1． 4 典型Web服务组合结构的XPC4CMSC描述与QoS计算

定义2 Web服务组合的XPC4CMSC语义模型是一个5元组，MoSC＝（Endpoint，Activity，Tr ansition，Label，QoS）。其中：End point是 W eb服务节点，即由伙伴名称和操作名称组成的集合；Activity是调用活动、接收活动等的集合；Tr ansition是变迁函数；Label是标签函数；QoS是上面定义的Web服务的非功能属性模型。

用XPC4CMSC语言描述图1所示的服务模型如下：

1．4．1 Sequence组合

如图2所示，不同服务操作之间按照先后顺序依次执行，形成一条有序执行的串行链，后面服务操作需等其前面的Web服务执行完毕，并满足变迁触发条件时才能执行。图2所示的服务模型用XPC4CMSC语言描述如下：

1．4．2 Parallel组合

如图3所示，一组服务操作并发执行，只有当所有服务操作执行后，Parallel组合服务操作才算完成，变迁For k和Join起连接作用，只有当活动Activity1和Activity2全都执行完，才能触发变迁Join。图3所示的服务模型用XPC4CMSC语言描述如下：

Parallel组合服务响应时间为：TI MEparallel＝Max（Te（xi））；

1．4．3 Choice组合

如图4所示，在一组服务中任意选择一个执行，任意一个服务操作都有可能被选择执行，当被选操作执行完成，则说明Choice组合服务操作执行完成。图4所示的服务模型用XPC4CMSC语言描述如下：

Choice组合服务响应时间为：TI MEchoice＝

上述公式中，θi是Choice组合中第i个服务操示该服务操作必然被选择；θi＝0表示该服务操作必然不被选择。

2 服务组合的形式化验证方案

限于篇幅，有关服务组合的正确性验证、可达性验证等在此不进行阐述，仅对服务组合QoS一致性验证算法进行研究。验证服务组合QoS一致性的目的是保证组合方案中的组合服务在响应时间、执行费用、可靠性、可用性、物流时间、物流费用方面能够分别满足客户的需求，并使组合服务的标准化QoS综合评价值也能达到指定要求，从而得到基于QoS的最优服务组合方案。

2．1 服务组合QoS评价算法

根据上述建立的形式模型，编写服务组合QoS评价算法代码如下：LCe＿t hreshold分别对应响应时间、执行费用、可靠性、可用性、物流时间、物流费用；SCEV4 QOS＿t hreshold对应标准化QoS综合评价值。

（2）语句4是根据领域特征和实际情况，输入组合服务的QoS模型中每个非功能属性在综合质量中相应的权值，w1，w2，w3，w4，w5，w6分别对应响应时间、执行费用、可靠性、可用性、物流时间和物流费用的加权因子。

（3）语句5是满足组合规划功能的备选组合服务，依次进行验证。

（4）语句6是调用函数 QoSof Service Co mosition，得到组合服务QoS模型中的各非功能属性的值。

（5）语句7～18是根据客户输入的阈值，分别判断组合服务的各非功能属性是否满足客户的要求。

（6）语句19～44是求出各组合服务的各非功能属性的最大值和最小值，为QoS模型中各元素的标准化作准备。

（7）语句45～69是对QoS模型中各非功能元素进行标准化，并求出组合服务的综合质量评价值，判断是否达到客户提出的综合质量要求。

上述算法中，组合服务QoS模型中的各非功能属性值计算的时间复杂度为T1＝O（n）；语句5～69是循环语句，当服务组合规模足够大时，忽略其他低次幂项式，可得总的算法时间复杂度为T2＝O（n2）。

2．2 形式化验证方案

形式化验证方案如图5所示。CMC是针对Web服务编制进程代数语言开发的一种动态模型验证程序［21］，可验证XPC4CMSC指定服务性质。根据客户需求建立组合服务活动图，用XPC4CMSC语言描述服务组合的语义模型。然后将XPC4CMSC文件加载至CMC模型验证软件中进行形式化验证，捕捉组合服务的特殊性质，如可执行性、正确性、可靠性等。

3 用例分析

以两个车间的6台机器和10个待加工零件组合的柔性车间调度问题FT10为例，说明基于XPC4CMSC的服务组合形式化建模与验证过程。客户选择在两个车间的6台机器上加工10个零件，每个零件有3道工序，加工原材料从客户处发出，零件加工完后需运回客户处。10个零件的加工任务分别表示为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加工时间、加工费用、可靠性和可用性表

续表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单个零件的物流时间和物流费用表

建立上述零件加工组合服务的活动图，如图6所示。模型主要由10个服务即Sv＿01，Sv＿02，Sv＿03，Sv＿04，Sv＿05，Sv＿06，Sv＿07，Sv＿08，Sv＿09，Sv＿10并发组合而成。10个服务各由3个二代子服务顺序组合而成，例如Sv＿01由Sv＿0101，Sv＿0102，Sv＿0103顺序组合而成，根据零件工艺先后顺序分别调用Sv＿0101，Sv＿0102，Sv＿0103这3个服务，前面的服务成功执行完后才能执行排在其后的服务，即Sv＿0102的执行必须满足条件Sv＿0101 Answer＝yes，Sv＿0103的执行必须满足条件Sv＿0102 Ans wer＝yes。二代子服务又各由6个三代子服务组合而成，如图 7 所示，Sv＿0101 由 Sv＿010101，Sv＿010102，Sv＿010103，Sv＿010104，Sv＿010105，Sv＿010106经选择组合而成，根据防卫函数［guard］决定选择调用其中的一个服务执行。为使活动图清晰易读，图6和图7中省略了模型所包含的异常处理exception、事件处理event、补偿机制co mpensation等，这些处理机制可保证服务在执行过程中出现不正常情况时能做出相应的处理措施。根据活动图编写XPC4CMSC文件，部分编码如下：

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

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

｜t2＿08！〈Machine＿01Answer＝yes〉．e2＿08！〈guard2＿08〉）

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

｜t2＿09！〈Machine＿02 Ans wer＝yes〉．e2＿09！〈guard2＿09〉）

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

｜t2＿10！〈Machine＿03 Ans wer＝yes〉．e2＿10！〈guard2＿10〉）

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

｜t2＿11！〈Machine＿04Answer＝yes〉．e2＿11！〈guard2＿11〉）

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

｜t2＿12！〈Machine＿05Answer＝yes〉．e2＿12！〈guard2＿12〉）

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

｜t2＿13！〈Machine＿06Answer＝yes〉．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模型验证程序中进行形式化验证，如图8所示。给定QoS元素加权因子分别为0．3，0．3，0．1，0．1，0．1，0．1；阈值分别为40，165，0．7，0．7，105，55；标准化 QoS综合评价阈值为0．7。形式化验证结果如表5所示。

表5结果表明，组合服务1的响应时间和执行费用均未满足客户要求，如表5中的带下划线值；组合服务2的执行费用最高，严重超标；组合服务3具有较短的响应时间，但其物流时间和物流费用都没有达到客户要求；组合服务4与组合服务5的执行费用都未达到要求；组合服务6与组合服务8的物流时间都超标；组合服务7的响应时间偏长；组合服务9的综合评价不合格；组合服务10、组合服务11和组合服务12的六种质量元素都在阈值内，组合服务10有最短的响应时间，组合服务11有最高的可靠性，但组合服务12的执行费用、物流时间和物流费用都比前面二者好，故组合服务12的标准化QoS值最高，是最优的服务组合方案。图9为组合服务12的服务调度甘特图。上述结果也表明基于XPC4CMSC的云制造服务组合建模及形式化验证方案是可行的。

表5 形式化验证结果

4 相关服务组合方法比较

当前服务组合方法有多种，如文献［10］采用Pi演算进行Web服务组合建模与验证；文献［17］设计了基于统一建模语言（Unified Modeling Language，UML）的服务组合建模方法；文献［22］将云制造服务组合问题视为一个多目标规划问题，并利用自适应粒子群算法来解决该多目标规划问题。而本文考虑了响应时间、执行费用等6个属性因子，提出一种基于扩展进程代数XPC4CMSC的云制造服务组合建模与验证方法，该方法侧重于服务组合的描述、建模、形式化验证与属性分析，表6给出了该方法与其他服务组合方法的比较。从表中可以看出，XPC4CMSC满足服务组合的需求项数最多。

表6 服务组合方法比较

5 结束语

一个云制造组合服务由一组子服务组成，被组合的子服务彼此并发交互以完成客户请求，而彼此间的交互通过通信和交换信息来完成。云制造服务组合的重要问题之一是如何保证组合的正确性。解决该问题的重要手段就是为云制造服务组合提供一个形式化的模型以进行模型检查和验证。扩展进程代数可用来作为描述服务组合的形式化工具。本文提出的基于XPC4CMSC的云制造服务组合建模与形式化验证方案及QoS评价算法，是对进程代数非功能属性验证研究的有益补充，也为云制造服务组合的研究提供了一种新的视角和途径，后续研究将考虑如何动态处理云制造服务组合中QoS元素的加权因子以及算法优化等。

［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］．中国机械工程，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）．［李伯虎，张 霖，王时龙，等．云制造——面向服务的网络化制造新模式［J］．计算机集成制造系统，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）．［陶 飞，张霖，郭 华，等．云制造特征及云服务组合关键问题研究［J］．计算机集成制造系统，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）．［罗军舟，金嘉晖，宋爱波，等．云计算：体系架构与关键技术［J］．通信学报，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）．［刘卫宁，李一鸣，刘 波．基于自适应粒子群算法的制造云服务组合研究［J］．计算机应用，2012，32（10）：2869－2874，2878．］