A Choreography Analysis Approach for Microservice Composition in Cyber-Physical-Social Systems

Choreography-driven microservice composition has provided a better way to integrate components in the Cyber-physical-Social System (CPSS). Choreography is a global contract that specifies interactions among microservices participating in a composite service. After modeling a choreography, a problem arises here is whether the choreography specification at design time can be implemented correctly by generated microservices that interact with each other via exchanging messages. In this paper, we propose a novel approach for choreography analysis. Specifically, a choreography is specified using a Labeled Transition Systems (LTSs); then, the microservices participating in a composite service can be generated from the given choreography via projection and -remove; finally, the analysis of the choreography can be checked for both synchronous and asynchronous compositions using refinement checking. Our approach is completely automated under the support of our developed tool and the Process Analysis Toolkit (PAT) tool.