Cloud manufacturing service composition and formal verification based on extended process calculus

Abstract

Cloud manufacturing is an emerging service-oriented model to solve existing problems in manufacturing. This study proposes a process calculus–based approach to formally model cloud manufacturing service composition that is composed of description model, interaction scenario model, and composition process formal model, in which the semantics of process calculus to describe the quality of service (QoS) information of service composition is extended, and an intelligent service composition method is put forward based on the extended process calculus. Then, a platform architecture for implementing the proposed approach is addressed. The integrated development environment for the platform is set up with selection of free software tools. Thus, a prototype of the platform is developed. Finally, automated guided vehicle processing service composition and the open integrated manufacturing system service composition are taken as examples to illustrate the application of the proposed service composition method. The main attributes of the formal models for the application cases are verified. Case study results show that the proposed service composition and formal verification method based on the extended process calculus is feasible. Compared with other approaches for service composition, the proposed intelligent service composition method meets the most requirements for service composition.

Keywords

Cloud manufacturing service composition process calculus formal verification prototype platform

Introduction

In view of the severe situation of domestic industrial structure imbalance, rising manufacturing costs, and the weakness of traditional manufacturing competitive advantage, in 2015, the Chinese government launched the “China manufacturing 2025,”¹ combining the entity manufacturing industry with cloud computing,² big data,³ and other virtual network technology,⁴ to promote the transformation of industrial structure to the high end.⁵ Cloud manufacturing promotes the transformation of China’s manufacturing from traditional production to service-oriented and customized production. Cloud manufacturing⁶ is a new manufacturing mode to realize the integration of manufacturing industry and virtual network technology.⁷ It provides a direction for the integration of distributed manufacturing resources⁸ to solve the current manufacturing “information islands” and other problems.⁹ Machining with high processing precision, high production efficiency, quality and stability, and other characteristics is more suitable for highly customized multi-variety small and medium batch production.¹⁰ A single cloud service often fails to meet customer’s need. It is necessary to combine multiple cloud services to complete the manufacturing task. Because of the different performances of network transmission and the heterogeneity of the cloud service, the cloud service composition becomes complicated and error prone.¹¹ To ensure that composite services can be executed normally and meet their expected goals, the properties of the composite services must be verified before they are formally executed.

Process calculus has a strict definition of formal semantics. It can link the dynamic behavior of the cloud service to the operating semantics, and can verify its properties. The classical process calculus includes CCS (Calculus of Communication System),¹² COWS (Calculus for Orchestration of Web Services),¹³π-Calculus (Pi Calculus),¹⁴ CSP (Communicating Sequential Processes),¹⁵ ACP (Algebra of Communicating Process),¹⁶ and so on. Lapadula et al.¹³ built a mapping between BPEL (Business Process Execution Language) and COWS, so that the correctness of BPEL program could be verified by CMC (COWS Model Checker).¹³ Viry¹⁴ used Pi calculus to describe web service composition and verified it with validation tool MWB (Mobile Workbench).¹⁴ However, the above research works focused on the functional modeling and correctness verification of web services, without considering the non-functional requirements of cloud manufacturing services, such as time, cost, and other non-functional attributes. In the process of cloud manufacturing service composition, modeling non-functional attributes of cloud manufacturing services to support optimization and decision is paid more and more attention. It is necessary to extend process calculus to model non-functional attributes. The paper extends the semantics of process calculus to describe the quality of service (QoS) information of service composition. An intelligent service composition (ISC) method based on extended process calculus, business intelligence, and cloud entropy genetic algorithm is proposed. It can describe and verify the cloud manufacturing service composition and analyze the QoS of service composition. The result of analysis can be used as a reference basis for selecting service composition. Based on ISC, the architecture, design, and implementation technologies of cloud manufacturing service composition platform are studied. Cloud manufacturing service composition system prototype is developed, and its application case is given.

Literature review

Machining is a complex dynamic system. Throughout the current development of China’s machining industry, there are mainly the following problems: (1) the ability of quickly responding to market demand is poor,^17,18 (2) the manufacturing cost has no competitive advantage,¹⁹ (3) the innovation ability is insufficient,²⁰ and (4) the industrial structure is unreasonable, and the resource allocation is improper. On one hand, enterprise homogeneity is serious; on the other hand, due to the influence of geography, information, and other factors, the communication between enterprises or enterprise and customer is poor, resulting in “isolated island phenomenon.”²¹

In view of the above problems, under the condition of limited manufacturing resources, in order to obtain the market competition advantage and win the maximum profit, machining enterprises need the support of the cloud manufacturing service composition platform,^22,23 thus to achieve the following: (1) improving the transparency and visibility of enterprises, quickly responding to market demand; (2) strengthening exchange and cooperation between enterprises in market, logistics,^24,25 product development, design, manufacturing, and so on; and (3) promoting the transformation of the industrial structure, optimizing the allocation of resources, and making full use of limited resources to get the maximum profit.²⁶ Xu et al.²⁷ proposed a set of service domain–oriented artificial bee colony algorithms based on the optimization mechanism of artificial bee colony method for solving concurrent service selection and service composition problem. Wang et al.²⁸ developed an automatic weight calculation approach based on rough set theory and a fuzzy analytic hierarchy process and studied a two-phase optimization process to achieve an optimal service composition, where local optimization chose services based on creditable QoS assessment and global optimization tackled a multi-objective problem using cuckoo search algorithm. Li et al.²⁹ studied an autonomy-oriented method for service composition and optimal selection in cloud manufacturing. Lu and Xu³⁰ utilized distributed knowledge for ISC and adaptive resource planning and proposed a service composition method for facilitating easy mapping between service requests and manufacturing resources based on restrictive rule sets in the cloud and availability information about a resource. Navimipour and Vakili³¹ studied and compared several important techniques of cloud service composition and outlined key areas for the improvement of service composition methods in the future research. Entezari-Maleki et al.³² proposed a model based on timed colored Petri nets to evaluate the service composition in multicloud environments while minimizing the number of clouds involved in serving a composite service request. Gabrel et al.³³ proposed an approach for solving more efficiently polynomial cases based on a scheduling formulation with AND/OR constraints, using a directed graph structure. Cardinale et al.³⁴ proposed an approach to measure the fuzzy atomicity and gave a model allowing to self-adapt the composite service execution, taking into account the state of the composite service execution and user preferences. Rodriguez-Mier et al.³⁵ proposed a hybrid approach for automatic composition of web services that generated semantic input–output matching compositions minimizing the number of services and optimizing the global QoS. Faruk et al.³⁶ proposed an adaptive non-uniform mutation approach for QoS-aware cloud service composition to attain the best particle globally to boost the population assortment on the motivation of conquering the prematurity level of genetic particle swarm optimization algorithm. The above research works focus on the optimization of service composition, having service quality support function, but they lack semantic support function, having poor service composition connectivity, and being difficult to verify the attributes of service composition. However, extended process calculus can meet such needs.

Model and approach

Cloud service composition modeling based on extended process calculus

Formal model for cloud manufacturing service composition (FM4CMSC) is defined as follows.

Definition 1

FM4CMSC is a three-tuple set {CMSDM, FM4CMSIS, FM4CMSCP}, where CMSDM is Cloud Manufacturing Service Description Model, FM4CMSIS is Formal Model for Cloud Manufacturing Service Interactive Scenario, and FM4CMSCP is Formal Model for Cloud Manufacturing Service Composition Progress.

CMSDM is a model of cloud manufacturing service based on web service description language, which is mainly used to describe the static properties of cloud manufacturing service composition, including service quality of cloud manufacturing service, operation type, interface, message, mapping relationship, and so on. FM4CMSCP and FM4CMSIS, respectively, describe the interaction process and the composition relationship between the cloud manufacturing services by process calculus. The former focuses on the inner performance of the service composition and describes the interaction process of the resource flow and the information flow between the cloud services in a micro-perspective. The latter focuses on the external performance of the service composition and describes the business logic relationship of the cloud services in a macro-perspective.

Definition 2

FM4CMSIS is a six-tuple set {Endpoint, Process, Activity, Label, Message, Relation}, where Endpoint is the set of cloud manufacturing service nodes, Process is the set of process, Activity is the set of activity, Message is the set of message, Label is the label function, and Relation is the set of two meta-relationships between two activities.

Cloud Manufacturing Service Interaction Scenario is a sequence of adjacent service operations, which are defined by boundary elements such as interface and operation nodes in the cloud manufacturing service composition.

Definition 3

FM4CMSCP is a five-tuple set {Endpoint, Activity, Transition, Label, QoS}, where Endpoint is the set of cloud manufacturing service nodes; consisting of partner name and operation name; Activity is the set of invoke activity, receive activity, and so on; Transition represents transition function; Label represents label function; and QoS represents the quality of service of the cloud manufacturing service.²¹

According to Definition 3, the service composition model in Figure 1 is described in process calculus³⁷ as follows

\begin{matrix} [e_{1}, e_{2}, Te (x), Ce (x), Re (x), Ae (x), LTe (x), LCe (x)] \\ (Start \cdot Endpoint . End) \\ Start \overset{Δ}{=} e_{1}! 〈 ε_{guar d_{1}} 〉 \\ Endpoint \overset{Δ}{=} e_{1} ? 〈 true 〉 \cdot [t_{2}] ([[Activity]] {| t}_{2}! 〈 〉 \cdot e_{2}! 〈 ε_{guar d_{2}} 〉) \\ End \overset{Δ}{=} e_{2} ? 〈 true 〉 \cdot (kill (k_{t_{2}}) | {| t_{2}! 〈 〉 |}) \end{matrix}

where e₁ and e₂ are labels and Te (x), Ce (x), Re (x), Ae (x), LTe (x), and LCe (x) are response time, execution costs, reliability, availability, logistics time, and logistics costs, respectively. All of them are service quality elements defined in QoS.

Figure 1.

Process calculus semantic model of cloud manufacturing service composition.

There are mainly four kinds of service composition models: sequence composition, parallel composition, choice composition, and cycle composition.

Sequence composition

Different services are executed in accordance with the order of the sequence and form a serial chain. The latter service can be executed after the former service is completed and the transition trigger conditions meet. The service composition model in Figure 2 is described in process calculus as follows

\begin{matrix} [e_{1}, e_{2}, e_{3}, Te (x), Ce (x), Re (x), Ae (x), LTe (x), LCe (x)] \\ (Start \cdot Endpoin t_{1} \cdot Endpoin t_{2} \cdot End) \\ Start \overset{Δ}{=} e_{1}! 〈 ε_{guar d_{1}} 〉 \\ Endpoin t_{1} \overset{Δ}{=} e_{1} ? 〈 true 〉 \cdot [t_{2}] ([[Activit y_{1}]] {| t}_{2}! 〈 〉 \cdot e_{2}! 〈 ε_{guar d_{2}} 〉) \\ Endpoin t_{2} \overset{Δ}{=} e_{2} ? 〈 true 〉 \cdot [t_{3}] ([[Activit y_{2}]] {| t}_{3}! 〈 〉 \cdot e_{3}! 〈 ε_{guar d_{3}} 〉) \\ End \overset{Δ}{=} e_{3} ? 〈 true 〉 \cdot (kill (k_{t_{3}}) | {| t_{3}! 〈 〉 |}) \end{matrix}

where e₁, e₂, and e₃ are labels and Te (x), Ce (x), Re (x), Ae (x), LTe (x), and LCe (x) are response time, execution costs, reliability, availability, logistics time, and logistics costs, respectively. All of them are service quality elements defined in QoS. The QoS elements and service comprehensive evaluation value are calculated as follows

\begin{matrix} TIM E_{sequence} = \sum Te (x_{i}) \\ COS T_{sequence} = \sum Ce (x_{i}) \\ RELIABILIT Y_{sequence} = Π Re (x_{i}) \\ AVAILABILIT Y_{sequence} = Π Ae (x_{i}) \\ LOGISTICSTIM E_{sequence} = \sum LTe (x_{i}) \\ LOGISTICSCOS T_{sequence} = \sum LCe (x_{i}) \\ SCEV 4 QO S_{sequence} = M_{1}^{Te} \cdot λ_{1} + M_{2}^{Ce} \cdot λ_{2} + M_{3}^{Re} \cdot λ_{3} \\ + M_{4}^{Ae} \cdot λ_{4} + M_{5}^{LTe} \cdot λ_{5} + M_{6}^{LCe} \cdot λ_{6} = \sum_{j = 1}^{6} M_{j} \cdot λ_{j} \end{matrix}

where M_j is the weight coefficient and $SCEV 4 QO S_{sequence}$ is the service comprehensive evaluation value of sequence composition.

Figure 2.

Semantic model of sequence service composition.

Parallel composition

When a set of service operations are concurrently executed, the parallel composite service operation is not considered completed until all of the service operations are executed successfully. Transition Fork and Join play connection roles. Only when both Activity₁ and Activity₂ are finished, transition Join could be triggered. Parallel composition, as shown in Figure 3, can be described in process calculus as follows

\begin{array}{l} [e_{1}, e_{2}, e_{3}, e_{4}, e_{5}, e_{6}, T e (x), C e (x), R e (x), A e (x), L T e (x), L C e (x)] \\ (S t a r t \cdot F o r k \cdot (E n d p o i n t_{1} E n d p o i n t_{2}) \cdot J o i n \cdot E n d) \\ S t a r t \overset{Δ}{=} e_{1}! 〈 ε_{g u a r d_{1}} 〉 \\ F o r k \overset{Δ}{=} e_{1} ? 〈 t r u e 〉 \cdot (e_{2}! 〈 ε_{g u a r d_{2}} 〉 | e_{3}! 〈 ε_{g u a r d_{3}} 〉) \\ E n d p o i n t_{1} \overset{Δ}{=} e_{2} ? 〈 t r u e 〉 \cdot [t_{4}] (〚 A c t i v i t y_{1} 〛 {| t}_{4}! 〈 〉 \cdot e_{4}! 〈 ε_{g u a r d_{4}} 〉) \\ E n d p o i n t_{2} \overset{Δ}{=} e_{3} ? 〈 t r u e 〉 \cdot [t_{5}] (〚 A c t i v i t y_{2} 〛 | t_{5}! 〈 〉 \cdot e_{5}! 〈 ε_{g u a r d_{5}} 〉) \\ J o i n \overset{Δ}{=} e_{4} ? 〈 t r u e 〉 \cdot e_{5} ? 〈 t r u e 〉 \cdot e_{6}! 〈 ε_{g u a r d_{6}} 〉 \\ E n d \overset{Δ}{=} e_{6} ? 〈 t r u e 〉 \cdot (k i l l (k_{t_{6}}) | {| t_{6}! 〈 〉 |}) \\ T I M E_{p a r a l l e l} = M a x (T e (x_{i})) \\ C O S T_{p a r a l l e l} = \sum C e (x_{i}) \\ R E L I A B I L I T Y_{p a r a l l e l} = \prod R e (x_{i}) \\ A V A I L A B I L I T Y_{p a r a l l e l} = \prod A e (x_{i}) \\ L O G I S T I C S T I M E_{p a r a l l e l} = M a x (L T e (x_{i})) \\ L O G I S T I C S C O S T_{p a r a l l e l} = \sum L C e (x_{i}) \\ S C E V 4 Q O S_{p a r a l l e l} = \sum_{j = 1}^{6} M_{j} \cdot λ_{j} \end{array}

Figure 3.

Semantic model of parallel service composition.

Choice composition

As shown in Figure 4, in a set of services, any one of them is likely to be selected to perform. As long as the selected service is completed, the execution of the choice composition is completed

\begin{array}{l} [e_{1}, e_{2}, e_{3}, e_{4}, e_{5}, e_{6}, T e (x), C e (x), R e (x), A e (x), L T e (x), L C e (x)] \\ (S t a r t \cdot D e c i s i o n \cdot (E n d p o i n t_{1} + E n d p o i n t_{2}) \cdot M e r g e \cdot E n d) \\ S t a r t \overset{Δ}{=} e_{1}! 〈 ε_{g u a r d_{1}} 〉 \\ D e c i s i o n \overset{Δ}{=} e_{1} ? 〈 t r u e 〉 \cdot [e_{2}, e_{3}] \\ (e_{2}! 〈 ε_{g u a r d_{2}} 〉 | e_{3}! 〈 ε_{g u a r d_{3}} 〉 | (e_{2} ? 〈 t r u e 〉 \cdot e_{2}! 〈 t r u e 〉 + e_{3} ? 〈 t r u e 〉 \cdot e_{3}! 〈 t r u e 〉)) \\ E n d p o i n t_{1} \overset{Δ}{=} e_{2} ? 〈 t r u e 〉 \cdot [t_{4}] (〚 A c t i v i t y 1 〛 {| t}_{4}! 〈 〉 \cdot e_{4}! 〈 ε_{g u a r d_{4}} 〉) \\ E n d p o i n t_{2} \overset{Δ}{=} e_{3} ? 〈 t r u e 〉 \cdot [t_{5}] (〚 A c t i v i t y_{2} 〛 | t_{5}! 〈 〉 \cdot e_{5}! 〈 ε_{g u a r d_{5}} 〉) \\ M e r g e \overset{Δ}{=} e_{4} ? 〈 t r u e 〉 \cdot e_{6}! 〈 ε_{g u a r d_{6}} 〉 + e_{5} ? 〈 t r u e 〉 \cdot e_{6}! 〈 ε_{g u a r d_{6}} 〉 \\ E n d \overset{Δ}{=} e_{6} ? 〈 t r u e 〉 \cdot (k i l l (k_{t_{6}}) | {| t_{6}! 〈 〉 |}) \\ T I M E_{c h o i c e} = \sum (θ_{i} \cdot T e (x_{i})) \\ C O S T_{c h o i c e} = \sum (θ_{i} \cdot C e (x_{i})) \\ R E L I A B I L I T Y_{c h o i c e} = \sum (θ_{i} \cdot R e (x_{i})) \\ A V A I L A B I L I T Y_{c h o i c e} = \sum (θ_{i} \cdot A e (x_{i})) \\ L O G I S T I C S T I M E_{c h o i c e} = \sum (θ_{i} \cdot L T e (x_{i})) \\ L O G I S T I C S C O S T_{c h o i c e} = \sum (θ_{i} \cdot L C e (x_{i})) \\ S C E V 4 Q O S_{c h o i c e} = \sum_{j = 1}^{6} M_{j} \cdot λ_{j} \end{array}

where $θ_{i}$ is the probability factor of the i-th service operation in the choice composition, and $\sum θ_{i} = 1$ . $θ_{i} = 1$ indicates that the service operation is bound to be selected. $θ_{i} = 0$ indicates that the service operation must not be selected.

Figure 4.

Semantic model of choice service composition.

Cycle composition

As shown in Figure 5, the same service is repeatedly executed until the implementation condition is false, and thus the cycle composition is completed. Cycle is the operator of cycle composition. Cycle(n) {Activity} indicates that while the implementation condition is true, Activity is repeatedly executed

\begin{array}{l} [e_{1}, e_{2}, T e (x), C e (x), R e (x), A e (x), L T e (x), L C e (x)] \\ (S t a r t . C y c l e (n) {E n d p o i n t_{1}} \cdot E n d) \\ S t a r t \overset{Δ}{=} e_{1}! 〈 ε_{g u a r d_{1}} 〉 \\ C y c l e \overset{Δ}{=} n ? 〈 t r u e 〉 \cdot [e_{1}, e_{2}] (e_{1}! 〈 ε_{g u a r d_{1}} 〉 | e_{2}! 〈 ε_{g u a r d_{2}} 〉 | (e_{1} ? 〈 t r u e 〉 \cdot e_{1}! 〈 t r u e 〉 + e_{2} ? 〈 t r u e 〉 \cdot e_{2}! 〈 t r u e 〉)) \\ E n d p o i n t_{1} \overset{Δ}{=} e_{1} ? 〈 t r u e 〉 \cdot [t_{2}] (〚 A c t i v i t y 〛 {| t}_{2}! 〈 〉 \cdot e_{2}! 〈 ε_{g u a r d_{2}} 〉) \\ E n d \overset{Δ}{=} e_{2} ? 〈 t r u e 〉 \cdot (k i l l (k_{t_{2}}) | {| t_{2}! 〈 〉 |}) \\ T I M E_{c y c l e} = n \cdot T e (x_{i}) \\ C O S T_{c y c l e} = n \cdot C e (x_{i}) \\ R E L I A B I L I T Y_{c y c l e} = R e {(x_{i})}^{n} \\ A V A I L A B I L I T Y_{c y c l e} = A e {(x_{i})}^{n} \\ L O G I S T I C S T I M E_{c y c l e} = n \cdot L T e (x_{i}) \\ L O G I S T I C S C O S T_{c y c l e} = n \cdot L C e (x_{i}) \\ S C E V 4 Q O S_{c y c l e} = \sum_{j = 1}^{6} M_{j} \cdot λ_{j} \end{array}

Figure 5.

Semantic model of cycle service composition.

ISC method

The platform architecture for cloud manufacturing service composition is put forward as shown in Figure 6. It mainly consists of six layers. (1) Manufacturing resource layer provides a variety of distributed cloud manufacturing resources, which include CNC machine tools, mold, design and simulation analysis software, manufacturing engineering calculation, storage, product model, and so on. (2) Virtual resource layer is responsible for the realization of manufacturing resource services, providing the implementation tools for on-demand supply of cloud manufacturing services and bridging the gap between manufacturing resources and cloud manufacturing service platform. The various manufacturing resources needed by the whole life cycle of products are connected to the cloud manufacturing service platform through the corresponding servitization mode and tools, which enables centralized management of distributed manufacturing resources, on-demand access, and paid use. (3) Service information layer is responsible for the management and storage of all kinds of information, data and knowledge generated in the operation of the cloud manufacturing service platform, in which cloud manufacturing services and user information are classified, sorted, registered, deleted, updated, and so on. (4) Core function layer is in charge of the specific operation of cloud manufacturing services, including many functional modules such as service search and service matching, process arrangement and service scheduling, business intelligence and service composition, service modeling and service verification, and service trade and service evaluation. (5) Terminal application layer is responsible for human–computer interaction between users and the cloud manufacturing service platform, providing a web-based user interface, providing registration and login account, checking information, user service transaction constraints expression, service query, service creation, service composition modeling and verification, service transaction, and evaluation. The layer supports the users to access the various services provided by the cloud manufacturing service platform with the same platform configuration conditions and user rights in different locations and terminal operation environment. The user can access to the cloud manufacturing service platform through smartphones, laptop, PC and other terminal equipments, and applications provided by the platform. (6) Service operation layer provides functions such as system security, service monitoring, and service bus, to provide support for service registration, query, binding, scheduling, combination, and so on. The contents of the above six layers constitute an organic whole. The manufacturing resource layer is the cornerstone of cloud manufacturing service platform, which provides hematopoietic functionality for cloud manufacturing service platform and a steady stream of manufacturing resources. Table 1 gives the hierarchical architecture of cloud manufacturing service composition platform from the point of view of technical implementation. For the development of cloud manufacturing service composition platform, Apache Tomcat 6.0 is selected as the web server. MyEclipse7.0 which supports Java EE specification is selected to build integrated development environment. Table 1 lists the tools used to develop the cloud manufacturing service platform. Figure 7 is service category management interface of the cloud manufacturing service composition platform.

Figure 6.

Platform architecture for cloud service composition.

Table 1.

Architecture of cloud machining service composition system and its implementation technology.

Function layer	Implementation techniques and tools
Terminal application layer	Porta, JSP, JSF, Ajax
Core function layer	Java EE platform, MyEclipse, Tomcat, MVC, BPEL, SSH
Service information layer	Oracle, MySQL, XML
Virtual resource layer	Sensor, RFID, GPS, Xfire
Manufacturing resource layer	Manufacturing equipment, parts and components, manufacturing knowledge
Service operation layer	Hadoop, Esper, ESB

Figure 7.

Service category management interface.

Cloud manufacturing services are different from general web services. They not only need to consider service interface, data input, and output but also need to consider logistics, address, equipment, and other physical factors. According to the characteristics and objectives of cloud manufacturing service composition and the needs of cloud manufacturing service platform, ISC is put forward based on extended process calculus, multi-objective optimization algorithm,³⁸ and business intelligence.

As shown in Figure 8, the basic steps of ISC approach are as follows: (1) customers build their own service needs; (2) customers describe the service needs, business processes, and query-related services through the cloud manufacturing terminal application interface in the cloud manufacturing service platform; (3) customer selects service composition mode; (4) cloud manufacturing service platform parses the customer service needs, starting composition optimization and business intelligence functions, automatically searching, matching, composing, and verifying services, recommending component cloud services or composite cloud services for customer; (5) customer checks and selects the recommended cloud manufacturing services and chooses the appropriate composite cloud services or component cloud services to construct a new composite cloud service; (6) cloud manufacturing service platform monitors the customer’s service composition operations, starting the service composition formal verification mechanism to verify the composite cloud service and providing its QoS information for customers. The error messages and amendment suggestions will be given if the composite cloud service does not meet the customer’s needs and business processes. (7) Repeat the above steps until the customer gets the satisfactory composite cloud services; (8) service invocation and execution.

Figure 8.

Basic principle of the ISC approach.

In the ISC, the formal verification based on process calculus can verify whether the service composition scheme meets the customer’s needs and business processes, finds the mistakes, gives amendment suggestions, and provides reference for service composition of the platform.

Case study

Formal modeling and verification case

Formal modeling of the interaction scenarios

In order to improve the level of automation and information and the flexibility and the openness of manufacturing, an enterprise intends to transform three ordinary machine tools into computerized numerical control ones and develops a set of open computerized numerical control system. The system needs to achieve online order, generation of machine processing order, machine tool scheduling, monitoring process, cutting tool path simulation, control of machine processing and operation, and other functions. Taking into account its own limited capacity, the company decided to seek cloud manufacturing service platform to provide related services. On the cloud manufacturing service composition platform, the company initially selected an integrated manufacturing system development service which is composed of a number of sub-services to build an Open Integrated Manufacturing System Based on Cloud Manufacturing Services (OIMSBMCS), as shown in Figures 9 and 10. The company searches for cloud manufacturing services which meet its requirements with the service composition module shown in Figure 9. The selected cloud manufacturing services can be imported to the service verification module shown in Figure 10. The service composition formal model is established. The service properties are verified.

Figure 9.

The interface of service composition of open CNC machining system integration.

Figure 10.

The interface of formal verification of open CNC machining system integration service.

Interaction interfaces of sub-services

The integrated manufacturing system development service consists of eight sub-services: client, reception, order, warehousing, monitoring, scheduling, programming, and control. For example, FM4CMSIS for client sub-service is established as follows:

service Sub_Client // Client sub-service

{

Act 1: requestPartsCuttingService {output message: demandPCS} //Request for machining service of parts

Act 2: responseInformationVPartsCutting {input message: demandInformationVPC; output message: supplyInformationVPC }// Reply machining information of parts

Act 3: endNo4PartsCuttingService {input message: no4PCS} // Machine processing requirements can’t be met, customer ends services

Act 4: confirmOk4PartsCuttingService {input message: ok4PCS }//Machine processing requirements can be met, customer accept services

Act 5: queryMaterialArrived {output message: queryMA} //Send machining material

Act 6: payServiceFee {input message: demandPSF; output message: supplySFA } //Pay for services

Act 7: endOk4PartsCuttingService {input message: partsAIA}//Machining parts are completed, ending services normally

}

The interface of client sub-service is shown in Figure 11.

Figure 11.

Client sub-service interfaces.

Business logic

According to the principle of cloud manufacturing service interaction scenario segmentation, the interactive activities of the eight sub-services of OIMSBMCS can be segmented into five service interaction scenarios. Its overall business logic structure is shown in Figure 12. The service interaction scenario OIISN1 will be executed first. After the completion of the OIISN1, according to the system real-time state, the service interaction scenario OIISN2 or OIISN3 is chosen to perform. Once one of them is executed, the other one will not be executed. If OIISN2 is chosen and executed, the service will end after the completion of OIISN2. If OIISN3 is chosen and executed, OIISN4 and OIISN5 will follow successively.

Figure 12.

Business logic diagram of the service interaction scenarios.

Formal description of the interaction scenarios

Service interaction scenario consists of activities, interfaces, messages, operations, and other elements, which are defined by FM4CMSIS. The operation of FM4CMSIS is represented as “operation name + message.” For example, operation “input” added to the message indicates the input operation of the message; operation “output” added to the message indicates the output operation of the message. For the message demandPCS, outputDemandPCS is the output operation of demandPCS, which represents outputting request message of workpiece machining service. InputDemandPCS is the input operation of demandPCS, which indicates receiving request message of workpiece machining service.

For example, FM4CMSIS description of OIISN1 is given as follows:

f_OIISN1(Client)={outputDemandPCS, inputDemandInformationVPC, outputSupplyInformationVPC}

f_OIISN1(Reception)={inputDemandPCS, outputDemandInformationVPC, inputSupplyInformationVPC, outputDemandCreatePCO}

f_OIISN1(Order)={inputDemandCreatePCO,

outputDemandInformationVCNCM, outputDemandInformationVWS}

f_OIISN1(Monitoring)= {inputDemandInformationVCNCM}

f_OIISN1(Warehousing)= {inputDemandInformationVWS}

Timing chart of service interaction scenario OIISN1 is shown in Figure 13.

Figure 13.

Timing chart of service interaction scenario OIISN1. (1) outputDemandPCS, (2) inputDemandPCS, (3) outputDemandInformationVPC, (4) inputDemand InformationVPC, (5) outputSupplyInformationVPC, (6) inputSupplyInformationVPC, (7) outputDemandCreatePCO, (8) inputDemandCreatePCO, (9) outputDemandInformation VCNCM, (10) inputDemandInformationVCNCM, (11) output DemandInformationVWS, (12) inputDemandInformationVWS.

Formal verification of the scenario in FM4CMSIS

The basic principle of cloud manufacturing service composition formal verification is as follows. First, the cloud manufacturing service composition is transformed into FM4CMSIS model and FM4CMSCP model. Then, the models are converted to a process calculus language file. Finally, related attributes of the process calculus language file are verified by formal verification tools and attribute verification mechanism of cloud manufacturing service platform, and the verification results could be shown on the platform.

Correctness verification

For example, the FM4CMSIS model for OIISN4 in process calculus is as follows:

Client_OIISN4∷={!QueryMA}

Reception_OIISN4∷={?QueryMA, !DemandExecutePCO}

Order_OIISN4∷={?DemandExecutePCO, !ExecutePCO}

Scheduling_OIISN4∷={?ExecutePCO, !DemandTM, !DemandPCNC}

Warehousing_OIISN4∷={?DemandTM}

Programming_OIISN4∷={?DemandPCNC, !ProgramCNC}

Control_OIISN4∷= {?ProgramCNC}

OIISN4∷=

{!QueryMA.?QueryMA.!Demand ExecutePCO.?DemandExecutePCO.! ExecutePCO.?ExecutePCO.

!DemandTM.?DemandTM.! DemandPCNC.?DemandPCNC.! ProgramCNC.?ProgramCNC}

Correctnes s_{OIISN 4} = ({a, b}_{i} \in \otimes) \land a \in P \land b \in P \land (P - \sum_{i = 1}^{n} {a, b}_{i} = \emptyset)

where Correctness_OIISN4 is used to verify the correctness of OIISN4. If the verification result does not meet the correctness, the service composition may appear the execution out of order and other problems. Correctness of OIISN4 is verified by the formal verification tools of cloud manufacturing service platform, as shown in Figure 14, which shows that OIISN4 is correct.

Figure 14.

Correctness verification of OIISN4.

If OIISN4 is changed as follows:

OIISN4′∷=

{!QueryMA.?QueryMA.!Execute PCO.?ExecutePCO.!DemandTM.? DemandTM.!DemandPCNC.

?DemandPCNC.!DemandExecutePCO.? DemandExecutePCO.! ProgramCNC.?ProgramCNC}

Then, as shown in Figure 15, OIISN4′ can no longer move forward after running to the interactive operation 2 because the partial moment of operation 3 does not arrive and operation 5 cannot get the trigger conditions, resulting in that subsequent interactive operations 3 to 12 always cannot be implemented, and the service interaction is blocked. In this case, the system is no longer correct. Correctness_OIISN4′ is verified, as shown in Figure 16, which shows that OIISN4′ failed to verify the correctness. Such a conclusion is consistent with that shown in Figure 15.

Figure 15.

Timing chart of OIISN4′. (1) outputQueryMA, (2) inputQueryMA, (3) outputDemandExecutePCO, (4) inputDemandExecutePCO, (5) outputExecutePCO, (6) inputExecutePCO, (7) outputDemandTM, (8) inputDemandTM, (9) outputDemandPCNC, (10) inputDemandPCNC, (11) outputProgramCNC, (12) inputProgramCNC.

Figure 16.

Correctness verification of OIISN4′.

Conformance verification

For example, conformance verification for OIISN4 is as follows

\begin{matrix} {Conformance}_{OIISN 4} = Tim e_{s} \in P \land Cos t_{s} \in P \land Reliabilit y_{s} \\ \in P \land Availabilit y_{s} \in P \land Logistics Tim e_{s} \in P \\ \land Logistics Cos t_{s} \in P \land SCEV 4 QOS \in P \end{matrix}

where Conformance_OIISN4 is used to verify the conformance of the system. If the verification result meets the conformance, the response time, execution cost, reliability, availability, logistics time, and cost of the composite service can meet the requirements of the customer, and comprehensive evaluation value of cloud manufacturing service composition is also consistent with the customer requirements. Conformance_OIISN4 is verified by formal verification tools of cloud manufacturing service platform, as shown in Figure 17, which shows that OIISN4 has passed the conformance verification.

Figure 17.

Conformance verification.

Further application

A robot company in Foshan city takes an order to provide eight automated guided vehicles (AGVs) for a car factory within 15 days. As the company cannot finish the order on time based on its own manufacturing capability, it decides to search for machining services to complete the processing of AGV body. Heat treatment, painting, assembly, and others can be completed by itself. The machining process of AGV body is in turn: milling, drilling, and grinding. The raw material is sent out by the robot company, and the finished product is sent back. The company searches for a set of cloud manufacturing services on the cloud manufacturing service platform in an automatic mode of service composition, as shown in Figures 18 and 19. Six cloud manufacturing services meet the company’s requirements, as shown in Figure 18. The selected cloud manufacturing services can be imported to the service verification module, as shown in Figure 19. The service composition formal model and processing parameter matrix are established. The service properties are verified and then the related graphs are generated.

Figure 18.

The interface of service composition of AGV body processing.

Figure 19.

The interface of formal verification of AGV body processing service composition.

The cloud manufacturing services selected are as follows: M1 milling service, M2 drilling service and M3 grinding service in P1 plant, and M4 milling service, M5 drilling service, and M6 grinding service in P2 plant. The eight AGV body processing tasks are represented as Job_01, Job_02, Job_03, Job_04, Job_05, Job_06, Job_07, and Job_08. The six machines are represented as M_01, M_02, M_03, M_04, M_05, and M_06. The activity diagram of the above machining services is established in Figure 20.

Figure 20.

Activity diagram of AGV body processing service composition.

The model is composed of eight services in parallel, namely, Sv_01, Sv_02, Sv_03, Sv_04, Sv_05, Sv_06, Sv_07, and Sv_08. They follow the parallel composition rule. Each of the eight services is sequentially composed of three sub-services which follow the sequence composition rule. As shown in Figure 20, Sv_08 is composed of Sv_0801, Sv_0802, and Sv_0803 by sequence composition. Sv_0801, Sv_0802, and Sv_0803 are invoked according to the processing order of the parts. The latter service can be executed after the former service is completed. For example, Sv_0802 can be executed if Sv_0801Answer = yes. Each of sub-services can be further decomposed, as shown in Figure 21, where Sv_0801 is composed of Sv_080101 and Sv_080104 by choice composition.

Figure 21.

Activity diagram of Sv_0801 sub-service of AGV body processing services composition.

QoS evaluation of composite service is shown in Table 2. Service scheduling Gantt chart is shown in Figure 22.

Table 2.

QoS evaluation of composite service.

Composite service	Response time	Execution cost	Reliability	Availability	Logistics time	Logistics cost	SCEV4QoS	Result
CS	48	14,600	0.90	0.88	98	2800	0.77	TRUE

Figure 22.

Service scheduling Gantt chart of AGV body processing service composition.

The above results show that the proposed service composition and formal verification method based on extended process calculus are feasible. It can verify the related attributes of composite service, help users carry out a reasonable service composition, and promote the implementation of the cloud manufacturing. Table 3 lists the main function of a variety of service composition methods. Compared with other approaches for service composition, the proposed ISC method meets the most required items for service composition.

Table 3.

Comparison of service composition methods.

	BPEL³⁹	OWL-S⁴⁰	UML⁴¹	Pi Calculus¹⁴	Artificial Intelligence Algorithm²⁷	ISC
Semantic support function	—	√	—	—	—	√
Automatic service composition function	√	—	—	—	√	√
Correctness function	—	—	—	√	—	√
Service quality support function	—	√	—	—	√	√
Control modeling function	√	—	√	√	√	√
Collaborative modeling support function	√	√	√	√	√	√
Service composition connectivity function	√	√	√	√	—	√
Service composition extensibility function	—	—	√	√	√	√
Exception handling support function	√	—	—	√	—	√
Compensation processing support function	√	—	—	√	—	√
Model verification function	—	—	—	√	—	√
Software support function	√	√	√	√	√	√

Conclusion

To deal with the problems existing in manufacturing industry, especially in China’s machining industry, this article puts forward a cloud manufacturing service composition modeling and formal verification approach based on process calculus, which is composed of CMSDM, FM4CMSIS, and FM4CMSCP. The semantics of process calculus to describe the QoS information of service composition is extended. An ISC method based on extended process calculus, business intelligence, and cloud entropy genetic algorithm is proposed. The layered architecture and implementation technologies of cloud manufacturing service composition platform are studied. The cloud manufacturing service composition prototype platform is developed which focuses on the user management, cloud manufacturing resource servitization, service management, service composition, and formal verification. AGV processing service composition and the open integrated manufacturing system service composition are taken as examples to illustrate the application of the proposed service composition approach. The main attributes of the formal models for the application cases are verified. The research results are compared and analyzed. The proposed ISC method outperforms the related methods. The next step of the study is to improve the platform with more powerful functionality and more friendly interface.

Footnotes

Acknowledgements

The authors would like to thank the editors and anonymous reviewers for their constructive and helpful comments which helped to improve the presentation of the paper.

Handling Editor: ZhiWu Li

Declaration of conflicting interests

The author(s) declared no potential conflicts of interest with respect to the research, authorship, and/or publication of this article.

Funding

The author(s) disclosed receipt of the following financial support for the research, authorship, and/or publication of this article: The project was supported by the National Natural Science Foundation of China (51675186 and 51175187) and the Science & Technology Foundation of Guangdong Province (2017A030223002 and 2016A020228005).

ORCID iD

Xifan Yao

References

China Daily. Made in China 2025, http://www.chinadaily.com.cn/opinion/2015-03/10/content_19764324.htm (accessed 3 October 2015).

Wang

et al . Continuous distributed top-k monitoring over high-speed rail data stream in cloud computing environment. Adv Mech Eng 2013; 2013: 590234–590241.

Kholod

Kupriyanov

Shorov

. Decomposition of data mining algorithms into unified functional blocks. Math Probl Eng 2016; 2016: 8197349.

Guo

Hung

Scheunders

et al . Advanced techniques for computational and information sciences. Math Probl Eng 2016; 2016: 5623913.

Xia

. Enlightenments of German industry 4.0 and 2025 of Chinese woodworking machinery manufacturing. Forest Mach Wood Equip 2015; 43: 4–9.

Zhang

Wang

et al . Cloud manufacturing: a new service-oriented networked manufacturing model. Comput Integr Manuf 2010; 16: 1–7+16.

Zhang

Huang

et al . A unified algorithm for virtual desktops placement in distributed cloud computing. Math Probl Eng 2016; 2016: 9084370.

Zhong

Jiang

. Integrated scheduling of production and distribution with release dates and capacitated deliveries. Math Probl Eng 2016; 2016: 9315197.

Yao

Lian

et al . Service-oriented architecture and integrated development environment for cloud manufacturing. Comput Integr Manuf 2012; 18: 2312–2321.

10.

Tan

Liu

. Modular implement of high speed cutting without liquid in metal processing. Tool Eng 2013; 47: 53–56.

11.

Tao

Zhang

Guo

et al . Typical characteristics of cloud manufacturing and several key issues of cloud service composition. Comput Integr Manuf 2011; 17: 477–486.

12.

Nielson

. A monotone framework for CCS. Comput Lang Syst Struct 2009; 35: 365–394.

13.

Lapadula

Pugliese

Tiezzi

. Service discovery and negotiation with COWS. Electron Notes Theor Comput Sci 2008; 200: 133–154.

14.

Viry

. Parallel and distributed programming extensions for mainstream languages based on pi-calculus. Proc Ann ACM Symp Principles Distr Comput 2011; 2011: 343–344.

15.

Zhang

Liu

. Formal verification for CCML based web service composition. Inform Tech J 2011; 10: 1692–1700.

16.

Manzonetto

Salibra

. Applying universal algebra to lambda calculus. J Logic Comput 2010; 20: 877–915.

17.

Zhou

. Manufacturing practices in China. Int J Prod Econ 2013; 146: 1–3.

18.

Xiao

Zhou

. A new classification analysis of customer requirement information based on quantitative standardization for product configuration. Math Probl Eng 2016; 2016: 7274538.

19.

Zhang

Luo

Huang

. A bi-objective model for supply chain design of dispersed manufacturing in China. Int J Prod Econ 2013; 146: 48–58.

20.

Zhou

. Study on failure learning route in manufacturing enterprise service innovation process. Sci Technolo Prog Pol 2015; 32: 46–50.

21.

Yao

et al . Cloud manufacturing service composition modeling and QoS evaluation based on extended process calculus. Comput Integr Manuf 2014; 20: 689–700.

22.

Lin

Xia

Wang

et al . Cloud manufacturing in China: a literature survey. Int J Manuf Res 2014; 9: 369–388.

23.

Chen

Jiang

Zhang

et al . A robust service selection method based on uncertain QoS. Math Probl Eng 2016; 2016: 9480769.

24.

Yang

Liu

Wang

et al . An uncertain QFD approach for the strategic management of logistics services. Math Probl Eng 2016; 2016: 1486189.

25.

Erjiang

Peng

Tian

et al . Online cooperative promotion and cost sharing policy under supply chain competition. Math Probl Eng 2016; 2016: 3619597.

26.

Dou

Chen

Yang

. Genetic scheduling and reinforcement learning in multirobot systems for intelligent warehouses. Math Probl Eng 2016; 2016: 597956.

27.

Liu

Wang

et al . S-ABC: a paradigm of service domain-oriented artificial bee colony algorithms for service selection and composition. Future Gener Comp Sy 2016; 68: 304–319.

28.

Wang

Yang

et al . Integrating modified cuckoo algorithm and creditability evaluation for QoS-aware service composition. Knowl-Based Syst 2018; 140: 64–81.

29.

Guan

Liu

et al . An autonomy-oriented method for service composition and optimal selection in cloud manufacturing. Int J Adv Manuf Tech 2018; 96: 2583–2604.

30.

. A semantic web-based framework for service composition in a cloud manufacturing environment. J Manuf Syst 2017; 42: 69–81.

31.

Navimipour

Vakili

. Comprehensive and systematic review of the service composition mechanisms in the cloud environments. J Netw Comput Appl 2017; 81: 24–36.

32.

Entezari-Maleki

Etesami

Ghorbani

et al . Modeling and evaluation of service composition in commercial multiclouds using timed colored Petri nets. IEEE T Syst Man Cy: Sys 2017; 99: 1–15.

33.

Gabrel

Manouvrier

Moreau

et al . QoS-aware automatic syntactic service composition problem: complexity and resolution. Future Gener Comp Sy 2017; 80: 311–321.

34.

Cardinale

Haddad

Manouvrier

et al . Fuzzy ACID properties for self-adaptive composite cloud services execution. Concurr Comp: Pract E. Epub ahead of print 22 November 2017. DOI: 10.1002/cpe.4360.

35.

Rodriguez-Mier

Mucientes

Lama

. Hybrid optimization algorithm for large-scale QoS-aware service composition. IEEE T Serv Comput 2017; 10: 547–559.

36.

Faruk

Prasad

GLV

Dviya

. A genetic PSO algorithm with QoS-aware cluster cloud service composition. Adv Intell Syst 2015; 425: 395–405.

37.

Lapadula

Pugliese

Tiezzi

. A calculus for orchestration of web services. In: Proceedings of the 16th European symposium on programming, Braga, Portugal, 24 March–1 April 2007, vol. 4421, pp. 33–47. Berlin, Heidelberg: Springer.

38.

Yao

Zhou

. Multi-objective optimization of cloud manufacturing service composition with cloud-entropy enhanced genetic algorithm. J Mech Eng 2016; 62: 577–590.

39.

Sun

Zhang

Shang

et al . Integrating transactions into BPEL service compositions: an aspect-based approach. ACM T Web 2015; 9: 1–31.

40.

Cai

. OWL-S based service composition of three-dimensional geometry modeling. J Multimed 2012; 7: 98–105.

41.

Sabraoui

Ettalbi

Koutbi

et al . Towards an UML profile for web service composition based on behavioral descriptions. J Software Eng Appl 2012; 5: 711–721.