Automatic analysis of complex interactions in microservice systems

DOI10.1155/2020/2128793MaRDI QIDQ2175983zbMATH OpenOpenAlexFDO

Authors Fei Dai, Hao Chen, Zhenping Qiang, Zhihong Liang, Bi Huang, Leiguang Wang

Publication date 30 April 2020

Published in Complexity (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1155/2020/2128793

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Review text

Summary: 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.

Recommendations

• Automated analysis of asynchronously communicating systems
• A formal framework for specifying and verifying microservices based process flows
• A flow analysis approach for service-oriented architectures

Cites work

• Conversation protocols: a formalism for specification and verification of reactive electronic services
• Counterexample guided synthesis of monitors for realizability enforcement
• Deciding choreography realizability
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• On deciding synchronizability for asynchronously communicating systems
• Synchronizability for Verification of Asynchronously Communicating Systems

Cited in

(2)

• scientific article; zbMATH DE number 2080835 (Why is no real title available?)
• Service demand distribution estimation for microservices using Markovian arrival processes

This page was built for publication: Automatic analysis of complex interactions in microservice systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2175983)