Formal Verification of Cloud Manufacturing Service Composition and BPEL Codes Generation Based on Extended Process Calculus

作者：Li Yongxiang; Yao Xifan; Xu Xiangmin; Jin Hong; Tao Jin

来源：Information Technology Journal, 2014, 13(11): 1779-1785.

DOI：10.3923/itj.2014.1779.1785

• Process calculus
• Cloud manufacturing
• Service composition
• Formal verification
• BPEL

To solve the problem of the formal verification of cloud manufacturing services composition and generating corresponding BPEL codes, a new Extended Process Calculus for Cloud Manufacturing Service Composition (XPC4CMSC) was proposed based on the Calculus for Orchestration of Web Service (COWS) and QoS information. Its syntax and operational semantics were researched. For a typical service composition, activity diagram was established and formal model was built in XPC4CMSC. Six quality elements were calculated and standardized. Service composition formal verification scheme and BPEL code generation method were given. A flexible multi-shop scheduling problem was taken as an example to illustrate its application process. Case study showed that the proposed Cloud Manufacturing service composition formal verification scheme and BPEL code generation method were feasible and practical.

• 出版日期2014
• 单位华南理工大学