Automatic Analysis of Complex Interactions in Microservice Systems

Interactions in microservice systems are complex due to three dimensions: numerous asynchronous interactions, the diversity of asynchronous communication, and unbounded buffers. Analyzing such complex interactions is challenging. In this paper, we propose an approach for interaction analysis using model checking techniques, which is supported by the Process Analysis Toolkit (PAT) tool. First, we use Labeled Transition Systems (LTSs) to model interaction behaviors in microservice systems as sequences of send actions under synchronous and asynchronous communications. Second, we introduce a notion of correctness called “interaction soundness” which is considered as a minimal requirement for microservice systems. Third, we propose an encoding of LTSs into the CSP# process algebra for automatic verification of the property interaction soundness. The experimental results show that our approach can automatically and effectively identify interaction faults in microservice systems.