Cloud Manufacturing Services Composition Formal Modeling And Verification Based On Process Calculus

Cloud manufacturing as a new manufacturing model,has brought the dawn for solving "information island" problems in manufacturing by using the idea of cloud computing,distributed technologies and resources reuse.Formal modeling and verification of cloud manufacturing service composition is a key technology to ensure successful implementation of cloud service composition.By taking cloud manufacturing service composition as the research object,based on process calculus,service composition methods,service interaction scenario modeling,service composition process modeling,formal verification,and service composition platform for cloud manufacturing are researched from three dimensions of theory,modeling and application,which,thus,promotes correctness and security of service composition under cloud manufacturing environment,helps users on-demand access and pay for cloud manufacturing services,and share manufacturing resources and optimize their allocation in a broader scope,so as to improve manufacturing flexibility,agility and competitiveness of enterprises.The key technologies of cloud manufacturing service composition,modeling and formal verification are studied systematically in this paper.The main contents are as follows:The architecture of cloud manufacturing service composition platform is studied,where the main functions and implementation techniques of its each layer,including manufacturing resources layer,virtual resources layer,service information layer,core function layer,terminal application layer and service operation layer,are described in detail.Cloud manufacturing resources are analyzed and divided into physical,knowledge,and capacity resources according to the service-oriented concept.The characteristics of the three kinds of manufacturing resources are studied,and their description and encapsulation methods are given.The implementation process of cloud manufacturing resource servitization is addressed,which consists of resource-awareness,virtual encapsulation,service metamorphosis,and service presentation.Cloud manufacturing resource servitization models are set up,and the servitization cases of machine tools are studied.An intelligent service composition method for the cloud manufacturing service platform is addressed based on process calculus,cloud-entropy enhanced genetic algorithm and business intelligence.The basic principle of the intelligent service composition method and its three different service composition modes(namely manual,semi-automatic and automatic mode)are introduced.Cloud manufacturing service composition strategy is proposed and analyzed.The corresponding calculation methods of service matching degree,composition harmony degree and cloud-entropy are given.The multi-objective optimization mathematical model of cloud manufacturing service composition is built.A new service composition optimization approach,called cloud-entropy enhanced genetic algorithm(CEGA),is put forward to solve cloud manufacturing service composition problems with multi-objectives.The task of AGV(automated guided vehicle)manufacturing is taken as an example to verify the correctness of the established multi-objective optimization model and the feasibility of the proposed CEGA algorithm.Formal modeling methods for cloud manufacturing service composition are presented with focus on formal modeling for service interaction scenario and service composition process.The formal model for cloud manufacturing service interaction scenario is used to describe the interaction behaviors among cloud manufacturing services,which can clearly express the business logic relationship of the cloud manufacturing service composition and can simulate the whole interaction behaviors.The formal model for cloud manufacturing service composition process is used to describe the composition activities,which can express the work flow and the relations among manufacturing processes corresponding to the cloud manufacturing service composition.MillingMachine and MoldFactory services are taken as examples to establish the interaction scenario formal model and the composition process formal model respectively.The formal verification mechanism of the main attributes of cloud manufacturing service composition is studied.By using process calculus as a tool,the service interaction scenario model verification and service composition process model verification are linked together to verify the related properties of the composite service.In the formal verification process of the service interaction scenario model,the interaction activities of the service composition are divided into several service interaction scenarios according to the scenario segmentation principle with focus on verifying the functional attributes of each service interaction scenario.While the formal verification of the service composition process model focuses on verifying the non-functional attributes of the service composition activities.The technical architecture and implementation tools of a machining cloud service platform are studied,and the application of cloud manufacturing service composition modeling and verification technologies in cloud service platform are expounded.The medical oxygen inhalator manufacturing task is taken as an example to illustrate the application of the intelligent service composition method in the machining cloud service platform,while the AGV processing service composition and the open integrated manufacturing system service composition are taken as examples to respectively illustrate the application of the service composition process model and the service interaction scenario model.The main attributes of the formal models for the two application cases are verified with the proposed methods.Case study results show that the proposed formal modeling and verification methods based on the extended process calculus are feasible,and can verify the related attributes of service composition.Compared with other approaches for service composition,the proposed intelligent service composition method meets the most required items for service composition.