Deadlock Analysis of Microservice Systems with Bounded Buffers
Li Yang, Bi Huang, XinZhuo Chai, Guoxi Liu, Xiaojing Wu, Fei Dai · 2024
In modern software architectures, microservice are widely used due to their flexibility and scalability. However, the concurrent nature and complex interactions of microservice may lead to problems such as deadlocks, which affect the reliability of the system. In this thesis, we study the deadlock analysis of microservice with bounded buffers. First, we model microservices composed of microservices that communicating asynchronously via bounded FIFO buffers as Labeled Transition Systems. Next, the defined microservices are coded in the PAT (Process Analysis Toolkit) tool using the CSP# language. Finally, the model checking function of PAT was used to detect and analyze the deadlock of the system. The experimental results show that the method effectively identifies potential deadlock problems in the system and provides strong support for the design and optimization of the microservice system.