Abstract: To solve the modeling and formal verification problem of cloud manufacturing services composition,an eXtended Process Calculus for Cloud Manufacturing Service Composition (XPC4CMSC) by extending Quality of Service (QoS) information was proposed based on Calculus for Orchestration of Web Service(COWS),and the syntax and semantics of XPC4CMSC were given.The activity diagrams and XPC4CMSC descriptive models of sequence composition,parallel composition and choice composition were established,and the response time,implementation cost,reliability,availability,logistics time and cost for these three compositions were calculated.The formal verification schemes for QoS evaluation algorithms and service compositions were given.A flexible multi-shop scheduling problem was taken as an example to illustrate the verification process,and the case study showed that the proposed XPC4CMSC and formal verification approach were logical and feasible.

Key words: process calculus, cloud manufacturing, service composition, quality of service, formal verification

摘要： 为解决云制造服务组合建模与形式化验证问题,在Web服务编制演算的基础上提出一种扩展了服务质量信息的进程代数XPC4CMSC,给出了XPC4CMSC的语法、操作语义,建立了顺序组合、并发组合、选择组合的活动图与XPC4CMSC描述模型,计算了三种服务组合执行的响应时间、执行费用、可靠性、可用性、物流时间和物流费用。给出了服务质量评价算法与服务组合的形式化验证方案,通过一个柔性多车间调度问题展示了该方案的执行过程。示例研究表明,基于XPC4CMSC的云制造服务组合建模及形式化验证方案是可行的。

关键词: 进程代数, 云制造, 服务组合, 服务质量, 形式化验证