# Automatic Analysis of Complex Interactions in Microservice Systems

Authors: Fei Dai; Hao Chen; Zhenping Qiang; Zhihong Liang; Bi Huang; Leiguang Wang
Journal: Complexity
 (2020)

---

## Abstract

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.


---

## Body

## 1. Introduction

The cloud computing paradigm [1–3] and edge computing paradigm [4–6] enable us to utilize IT resources flexibly. This trend not only drives many software systems to migrate from monolithic architecture to microservice architecture [7] but also attracts more and more research focuses on how to build “cloud-native” [8] applications.Microservice architecture [9] can be used to develop a single application composed of a set of microservices. Compared with traditional web services, these microservices are much more fine-grained and are independently developed and deployed [3]. These characteristics of microservice architecture are particularly suitable for losing coupling and updating systems running on cloud infrastructures [10].The interactions in microservice systems are complex due to three dimensions: numerous asynchronous interactions, the diversity of asynchronous communication, and unbounded buffers. First, the execution of a microservice system may involve numerous interactions among microservices. Most of these interactions are asynchronous because synchronous interactions may cause the multiplicative effect of downtime [11, 12]. For example, Netflix’s online service system involves 5 billion service invocations per day [13]. These asynchronous interactions may cause unexpected sequences of messages during execution. Second, under point-to-point semantics, there are at least two asynchronous communications with FIFO buffers [14], namely, peer-to-peer communication and mailbox communication. Microservice systems can be realized by the two different asynchronous communication models. Compared with the mailbox semantics, the peer-to-peer semantics causes the interaction topology to be a much complex graph. Third, because the sizes of the buffers of microservice systems are not known a priori, their sizes are often considered to be unbounded. Microservice systems with unbounded buffers may exhibit infinite state space such that the reachability problem of such systems is known to be undecidable [15].The complexity of interactions in microservice systems poses great challenges to analyzing because missing or improper coordination among microservices may cause interaction faults. The results of the industrial survey in [10] show that interaction faults are common in microservice systems.Although there are a few papers on microservice systems [16], most of them focus on debugging [10, 11, 17–19], deployment [20, 21], composition [22], architecture [23], and adaptation [24]. However, there is little research on the interaction analysis of microservice systems. A basic and effective technique for analyzing interactions in microservice systems is synchronizability analysis [25–27]. A system is synchronizable if it sends actions which remain the same for both the asynchronous communication and synchronous communication. However, recent research shows synchronizability is undecidable [14].In this paper, we propose an approach for interaction analysis using model checking techniques, which is supported by the Process Analysis Toolkit (PAT) [28] tool. Such an analysis approach enables us to effectively and automatically identify interaction faults of microservice systems. Our contribution can be summarized as follows:(i)
We model complex interactions in microservice systems under synchronous and peer-to-peer asynchronous communications(ii)
We introduce a notion of correctness called “interaction soundness” which is considered as a minimal requirement for microservice systems(iii)
We automatically verify the property interaction soundness using model checking techniques under the support of the Process Analysis Toolkit (PAT) tool.Moreover, we propose an encoding of LTSs into the CSP# process algebra. We choose CSP# because it is equipped with the PAT tool which offers the PAT simulator for state space generation and the PAT verifier for property verification. In particular, when the PAT verifier returnsnot valid using model checking, it gives us the counterexample which is very useful to fix faults.The rest of this paper is organized as follows. Section2 discusses related work. Section 3 presents some formal definitions used throughout this paper. Section 4 formally defines the interaction behaviors of microservice systems under synchronous and peer-to-peer asynchronous communications. Section 5 introduces a notion of interaction soundness and verifies the property using model checking techniques based on CSP# encoding. Section 6 discusses the implementation of our approach and experimental results. Section 7 concludes this paper.


## 2. Related Work

There has been some research on debugging microservice systems. In [10], the authors conducted an industrial survey to show three main faults in microservice systems, namely, internal faults, interaction faults, and environment faults. In [11, 17], the authors proposed a novel approach for debugging microservice systems. In [18], the authors discussed complex live testing strategies for microservice systems. In [19], the authors proposed a new approach to test performance of each microservice participating in a microservice system. All these studies can be used to test microservice systems. However, our work focuses on analyzing interactions in microservice systems.There are some other studies on microservice systems. In [20], the authors proposed an approach to modeling and managing deployment costs for microservice systems. In [21], the authors discussed how to improve the performance of a microservice architecture. In [22], the authors proposed an approach to integrate microservices based on Linked Data. In [23], the authors presented a tool for generating and managing models of microservice architecture. In [24], the authors discussed how to balance the granularity of a microservice architecture. However, all these methods cannot be used to analyze interactions in microservice systems.To the best of our knowledge, we are the first to analyze complex interactions in microservice systems.


## 3. Preliminaries

In this section, we present some definitions used throughout this paper.Definition 1.
(labeled transition system). A labeled transition system is a tupleLTS = (S, s0, F, A, Δ), where(i)
S is a set of states(ii)
s0 ∈ S is the initial state(iii)
F ⊆ S is a set of final states(iv)
A is a set of labels(v)
Δ⊆S×A×S is a transition relation
For the sake of simplicity, we user⟶as to denote (r, a, s) ∈ Δ.
CSP# is an extension of CSP (communicating sequential processes) [29]. In this paper, we use CSP# for microservice system verification. In essence, CPS# is a formal method which integrates state-based specification and event-based specification. The following is a BNF description of the #CSP process expression. More details of CSP# can be found in [30].P::=Stop in-action|Skip terminal|e ⟶ P prefix|ch!exp ⟶ P channel input|ch?exp ⟶ P channel output|P\X hiding|P; Q sequential composition|P[]X external choice|PΠX internal choice|if b {P} else {Q} conditional choice|[b]P guarded process|P||Q parallel composition|P|||Q interleaving|PΔQ interrupting|ref(Q) process referencingwhere P and Q are processes, e is an event, X is a set of event names (e.g., {e1, e2}), b is a Boolean expression, ch is a channel, exp is an expression, and x is a variable [28].
The syntax of LTL formulas are defined as follows. More details of LTL can be found in [29].F = e | prop | [] F | <> F | X F | F1 U F2 | F1 R F2where e is an event, prop is a predefined proposition, F, F1, and F2 are three LTL formulas, [] denotes “always,” <> denotes “eventually,” X denotes “next,” U denotes “until”, and R denotes “release.”


## 4. Interaction Behavior Model

In this section, we introduce a formal model (see Figure1) for modeling complex interactions in microservice systems. In our model, microservices with unbounded buffers communicate asynchronously with each other and interactions in a microservice system can be viewed as sequences of send actions because receive actions which consume messages from buffers are considered as local invisible actions.Figure 1
The formal model of complex interactions in microservice systems under the peer-to-peer communication.Figure1 illustrates the three communicating microservices MS1, MS2, and MS3 with messages a, b, c, and d that are from the example in [8]. The initial states of each microservice are subscripted with 0 and marked with incoming half-arrows. The final states of each microservice are marked with double circles. Each transition of each microservice is labeled with send action (exclamation marks) or receive message action (question marks). The buffers are in red lines and marked with i and j, where i denotes the sender and j denotes the receiver. For example, the buffer12 denotes the buffer of MS2 which is used to store incoming messages sent from MS1. Note that each buffer is an FIFO message queue.When we further consider asynchronous messaging in Figure1, there are two different semantics for the point-to-point asynchronous communication, namely, peer-to-peer communication and mailbox communication. The mailbox communication shown in Figure 2 requires all messages sent to MS1 from the other microservices are stored in a buffer (i.e., a message queue) that is specific to MS1. The peer-to-peer communication requires each message sent from a microservice MS1 to another microservice MS2 is stored in a buffer in an FIFO fashion which is specific to the pair (MS1, MS2). In other words, each participating microservice of a microservice system is equipped with many buffers for different incoming messages from other microservices. In this paper, we focus on peer-to-peer communication.Figure 2
The mailbox communication.Based on the analysis above, we first use finite LTSs to model the behaviors of individual microservices. Then, we move to model the asynchronous interaction behaviors of microservice systems both with unbounded buffers and with bounded buffers (sayk). Finally, we model the synchronous interaction behaviors of microservice systems based on the asynchronous interaction behaviors.Definition 2.
(message set). A message setM is a tuple (Σ, p, src, dst).(i)
Σ is a finite set of letters(ii)
p≥1 is a nonnegative integer number which denotes the number of participating microservices(iii)
src and dst are functions that associate message m ∈ Σ to nonnegative integer numbers src(m) ≠dst(m) ∈ {1, 2, …, p}
We often usemi⟶j for a message m such that src(m) = i and dst(m) = j.Definition 3.
(microservice). A microserviceMS is a labeled transition system (S, s0, F, M, δ), where(i)
S is the finite set of states(ii)
s0 is the initial state(iii)
F ⊆ S is the finite set of final states(iv)
M is a message set(v)
δ ⊆ S × (M ∪ {ε}) × S is the transition relation
A transitionτ ∈ δ can be one of the following three types:(1)
A send-transition (s1, !m1⟶2, s2) which denotes that the microservice MS1 sends out a message m1⟶2 to another microservice MS2 where m1⟶2 ∈ M(2)
A receive-transition (s1, ?m1⟶2, s2) which denotes that the microservice MS1 consumes a message m1⟶2 where m1⟶2 ∈ M(3)
Anε-transition (s1, ε, s2) which denotes the invisible action of MS1
We often usesi⟶!mi⟶jsj to denote that (si, !mi⟶j, sj).


### 4.1. Asynchronous Interaction Behaviors of Microservice Systems

Definition 4.
(asynchronous interaction behavior of a microservice system with unbounded buffers). An asynchronous interaction behavior of a microservice system with unbounded buffers over a set of microservices (MS1, MS2, …, MSn), where MSi = (Si, s0i, Fi, Mi, δi) and Mi = (Σi, pi, srci, dsti), is denoted by a labeled transition system Ba = (C, c0, F, M, Δ) (possible infinite state) where(i)
C ⊆ Q1 × S1 × Q2 × S2…Qn × Sn is the set of states such that ∀i ∈ {1, 2, …, n}:Qi = (bufferji), where ∀j ∈ {1, 2, …, n}∧i ≠ j∧bufferji ⊆ (Mj)∗.(ii)
c0 ∈ C is the initial state such that c0 = (,,…,︸n−1, c01, ,,…,︸n−1, c02,…, ,,…,︸n−1, c0n), where c0i = MSi·s0i.(iii)
F ⊆ C is the set of final states such that ∀f ∈ F = (,,…,︸n−1, f1, ,,…,︸n−1, f2,…, ,,…,︸n−1, fn), where fi ∈ MSi·Fi.(iv)
M = ∪iMi is the set of messages.(v)
Δ ⊆ C × (M∪{ε}) × C for c = (Q1, s1, Q2, s2, …, Qn, sn) and c′ = (Q′1, s′1, Q′2, s′2, …, Q′n, s′n).(a)
c⟶!mi⟶jc′ ∈ Δ if ∃i, j ∈ {1, 2, …, n}:m ∈ M:(i)
src(m) = i ∧ dst(m) = j,(ii)
si⟶!mi⟶jsi′ ∈ δi,(iii)
∀k ∈ {1, 2, …, n}:k ≠ i ⟹ s’k = sk,(iv)
∀k ∈ {1, 2, …, n} ∧ k = i ⟹ bufferkj = bufferkjm,(v)
∀k, l ∈ {1, 2, …, n} ∧k ≠ i∧l ≠ j∧k ≠ l ⟹ bufferkl′ = bufferkl.[send action](b)
c⟶!mi⟶jc′ ∈ Δ if ∃i, j ∈ {1, 2, …, n}∧m ∈ M:(i)
src(m) = i∧dst(m) = j,(ii)
sj⟶!mi⟶jsj′ ∈ δj,(iii)
∀k ∈ {1, 2, …, n}:k ≠ j ⟹ sk′ = sk,(iv)
∀k ∈ {1, 2, …, n}∧k = i ⟹ bufferkj′ = mbufferkj,(v)
∀k, l ∈ {1, 2, …, n}k ≠ i∧l ≠ j∧k ≠ l ⟹ bufferkl′ = bufferkl.[receive action](c)
c⟶εc′ ∈ Δ if ∃i, j ∈ {1, 2, …, n}:(i)
si⟶εsi′ ∈ δi,(ii)
∀k ∈ {1, 2, …, n}: k ≠ i ⟹ sk′ = sk,(iii)
∀k ∈ {1, 2, …, n}: Qk′ = Qk.[internal action]
According to Definition4, microservices with unbounded buffers participating in a microservice system can interact with each other under the peer-to-peer semantics. The states (C) of a composite service consisting of n microservices are described by each microservice’ local state and its respective buffers. Each microservice has n − 1 unbounded buffers. When MS1 sends a message m to MS2, the message will be inserted to the tail of the buffer12 which is specific to the pair (MS1, MS2) and then MS2 can consume this message from the head of its buffer12. The send action (item 4a) is nonblocking and involves a sender, a receiver, and receiver’s buffer. After the sender MSi sends a message m to the receiver MSj, the state of the sender is changed (4a-ii), the message will be inserted to the tail of the bufferij which is specific to the pair (MSi, MSj) (4a-iv), and the other buffers do not change (4a-v). The receive message action (item 4b) is blocking and local, which involves only a receiver. After the receive message action is executed, the state of the message receiver is changed (4b-ii), the message at the head of the buffer of the receiver is consumed (4b-ii), and the other buffers do not change (4b-v). The epsilon-labeled transition (item 4c) is internal actions and can simply change the local state of a microservice.
Moreover, if we setQi = (bufferi) and keep others unchanged in Definition 4, the semantics of asynchronous communication is changed to the mailbox communication. Therefore, the mailbox communication is a special case of the peer-to-peer communication.
The interaction behavior of a microservice system depends on not only the order in which send actions are executed but also the size of each microservice’s buffers [31]. When buffers are unbounded, interaction behavior may be infinite.
We define the asynchronous interaction behavior of microservice systems with bounded buffers in the following, where each participating microservice has buffers of sizek.Definition 5 (asynchronous interaction behavior of a microservice system with buffers of size k).
The asynchronous interaction behavior of a microservice system with buffers of sizek is denoted by a labeled transition system Bak=C,c0,F,M,Δ and described by augmenting condition (a) in Definition 4 to include the condition Qj = (q1, qj−1, qj+1,…, qn): |qj| < k, where |qi| denotes the length of the buffers for microservice MSi.
In a microservice system with buffers of sizek, the send actions are blocked if the receiver’s buffer contains k messages. Therefore, the interaction behavior of a microservice system with buffers of size k is finite.
Figure3(a) illustrates the asynchronous interaction behavior of the microservice system with buffers of size 2 shown in Figure 1 under the peer-to-peer communication. The initial state is denoted by c0 = (([], []), s01, ([], []), s02, ([], []), s03) (i.e., each microservice is in its initial state and all the buffers are empty). After MS1 sends the message a to the buffer12 of MS2, the system evolves from c0 to c1 and the buffer12 contains a. Then, MS2 consumes the “matching” message a at the head of its buffer12, the system evolves from c1 to c3, and the message a is removed from the buffer12.
Figure3(b) illustrates the asynchronous interaction behavior of the microservice system with buffers of size 2 shown in Figure 1 under the mailbox communication. The initial state is c0 = (([], []), s01, ([], []), s02, ([], []), s03), and the final state is c10.Figure 3
The asynchronous interaction behavior of the microservice system with buffers of size 2 shown in Figure1. (a) The peer-to-peer communication. (b) The mailbox communication.
(a)
(b)


### 4.2. Synchronous Interaction Behaviors of Microservice Systems

In synchronous communication, every send action is executed followed by a receive action, i.e., the microservices interact synchronously. It seems that each microservice of a microservice system has buffers of size 0.Definition 6.
(synchronous behavior of a microservices system). A synchronous behavior of a microservices system over a set of microservices (MS1, MS2, …, MSn), where MSi = MSi = (Si, s0i, Fi, Mi, δi) and Mi = (Σi, pi, srci, dsti), is denoted by a labeled transition system Bs = (C, c0, F, M, Δ), where(i)
C⊆S1×S2⋯×Sn is the set of states.(ii)
c0 ∈ C is the initial state.(iii)
F ⊆ C is the set of final states such that ∀f ∈ F = (f1, f2, …, fn) where fi ∈ MSi·Fi.(iv)
M = ∪iMi is the set of messages.(v)
Δ ⊆C × (M ∪ {ε}) × C for c = (s1, s2, …, sn) and c′=s1′,s2′,…,sn′.(a)
c⟶!mi⟶jc′ ∈ Δ if ∃i, j ∈ {1, 2, …, n}∧m ∈ M:(i)
src(m) = i∧dst(m) = j,(ii)
si⟶!mi⟶jsi′ ∈ δi,(iii)
sj⟶!mi⟶jsj′ ∈ δj,(iv)
∀k ∈ {1, 2, …, n} : k ≠ i∧k ≠ j ⟹ sk′ = sk.[synchronous send-receive action](b)
c⟶εc′ ∈ Δ if ∃i, j ∈ {1, 2, …, n}:(i)
si⟶εsi′ ∈ δi,(ii)
∀k ∈ {1, 2, …, n} : k ≠ i ⟹ sk′ = sk,[internal action]
Figure4 illustrates the synchronous behavior of a microservice system shown in Figure 1. The behavior of the system have transitions a1⟶2, followed by a1⟶2, followed by b1⟶2, and followed by c3⟶2.Figure 4
The synchronous interaction behavior of the microservice system shown in Figure1.


## 4.1. Asynchronous Interaction Behaviors of Microservice Systems

Definition 4.
(asynchronous interaction behavior of a microservice system with unbounded buffers). An asynchronous interaction behavior of a microservice system with unbounded buffers over a set of microservices (MS1, MS2, …, MSn), where MSi = (Si, s0i, Fi, Mi, δi) and Mi = (Σi, pi, srci, dsti), is denoted by a labeled transition system Ba = (C, c0, F, M, Δ) (possible infinite state) where(i)
C ⊆ Q1 × S1 × Q2 × S2…Qn × Sn is the set of states such that ∀i ∈ {1, 2, …, n}:Qi = (bufferji), where ∀j ∈ {1, 2, …, n}∧i ≠ j∧bufferji ⊆ (Mj)∗.(ii)
c0 ∈ C is the initial state such that c0 = (,,…,︸n−1, c01, ,,…,︸n−1, c02,…, ,,…,︸n−1, c0n), where c0i = MSi·s0i.(iii)
F ⊆ C is the set of final states such that ∀f ∈ F = (,,…,︸n−1, f1, ,,…,︸n−1, f2,…, ,,…,︸n−1, fn), where fi ∈ MSi·Fi.(iv)
M = ∪iMi is the set of messages.(v)
Δ ⊆ C × (M∪{ε}) × C for c = (Q1, s1, Q2, s2, …, Qn, sn) and c′ = (Q′1, s′1, Q′2, s′2, …, Q′n, s′n).(a)
c⟶!mi⟶jc′ ∈ Δ if ∃i, j ∈ {1, 2, …, n}:m ∈ M:(i)
src(m) = i ∧ dst(m) = j,(ii)
si⟶!mi⟶jsi′ ∈ δi,(iii)
∀k ∈ {1, 2, …, n}:k ≠ i ⟹ s’k = sk,(iv)
∀k ∈ {1, 2, …, n} ∧ k = i ⟹ bufferkj = bufferkjm,(v)
∀k, l ∈ {1, 2, …, n} ∧k ≠ i∧l ≠ j∧k ≠ l ⟹ bufferkl′ = bufferkl.[send action](b)
c⟶!mi⟶jc′ ∈ Δ if ∃i, j ∈ {1, 2, …, n}∧m ∈ M:(i)
src(m) = i∧dst(m) = j,(ii)
sj⟶!mi⟶jsj′ ∈ δj,(iii)
∀k ∈ {1, 2, …, n}:k ≠ j ⟹ sk′ = sk,(iv)
∀k ∈ {1, 2, …, n}∧k = i ⟹ bufferkj′ = mbufferkj,(v)
∀k, l ∈ {1, 2, …, n}k ≠ i∧l ≠ j∧k ≠ l ⟹ bufferkl′ = bufferkl.[receive action](c)
c⟶εc′ ∈ Δ if ∃i, j ∈ {1, 2, …, n}:(i)
si⟶εsi′ ∈ δi,(ii)
∀k ∈ {1, 2, …, n}: k ≠ i ⟹ sk′ = sk,(iii)
∀k ∈ {1, 2, …, n}: Qk′ = Qk.[internal action]
According to Definition4, microservices with unbounded buffers participating in a microservice system can interact with each other under the peer-to-peer semantics. The states (C) of a composite service consisting of n microservices are described by each microservice’ local state and its respective buffers. Each microservice has n − 1 unbounded buffers. When MS1 sends a message m to MS2, the message will be inserted to the tail of the buffer12 which is specific to the pair (MS1, MS2) and then MS2 can consume this message from the head of its buffer12. The send action (item 4a) is nonblocking and involves a sender, a receiver, and receiver’s buffer. After the sender MSi sends a message m to the receiver MSj, the state of the sender is changed (4a-ii), the message will be inserted to the tail of the bufferij which is specific to the pair (MSi, MSj) (4a-iv), and the other buffers do not change (4a-v). The receive message action (item 4b) is blocking and local, which involves only a receiver. After the receive message action is executed, the state of the message receiver is changed (4b-ii), the message at the head of the buffer of the receiver is consumed (4b-ii), and the other buffers do not change (4b-v). The epsilon-labeled transition (item 4c) is internal actions and can simply change the local state of a microservice.
Moreover, if we setQi = (bufferi) and keep others unchanged in Definition 4, the semantics of asynchronous communication is changed to the mailbox communication. Therefore, the mailbox communication is a special case of the peer-to-peer communication.
The interaction behavior of a microservice system depends on not only the order in which send actions are executed but also the size of each microservice’s buffers [31]. When buffers are unbounded, interaction behavior may be infinite.
We define the asynchronous interaction behavior of microservice systems with bounded buffers in the following, where each participating microservice has buffers of sizek.Definition 5 (asynchronous interaction behavior of a microservice system with buffers of size k).
The asynchronous interaction behavior of a microservice system with buffers of sizek is denoted by a labeled transition system Bak=C,c0,F,M,Δ and described by augmenting condition (a) in Definition 4 to include the condition Qj = (q1, qj−1, qj+1,…, qn): |qj| < k, where |qi| denotes the length of the buffers for microservice MSi.
In a microservice system with buffers of sizek, the send actions are blocked if the receiver’s buffer contains k messages. Therefore, the interaction behavior of a microservice system with buffers of size k is finite.
Figure3(a) illustrates the asynchronous interaction behavior of the microservice system with buffers of size 2 shown in Figure 1 under the peer-to-peer communication. The initial state is denoted by c0 = (([], []), s01, ([], []), s02, ([], []), s03) (i.e., each microservice is in its initial state and all the buffers are empty). After MS1 sends the message a to the buffer12 of MS2, the system evolves from c0 to c1 and the buffer12 contains a. Then, MS2 consumes the “matching” message a at the head of its buffer12, the system evolves from c1 to c3, and the message a is removed from the buffer12.
Figure3(b) illustrates the asynchronous interaction behavior of the microservice system with buffers of size 2 shown in Figure 1 under the mailbox communication. The initial state is c0 = (([], []), s01, ([], []), s02, ([], []), s03), and the final state is c10.Figure 3
The asynchronous interaction behavior of the microservice system with buffers of size 2 shown in Figure1. (a) The peer-to-peer communication. (b) The mailbox communication.
(a)
(b)


## 4.2. Synchronous Interaction Behaviors of Microservice Systems

In synchronous communication, every send action is executed followed by a receive action, i.e., the microservices interact synchronously. It seems that each microservice of a microservice system has buffers of size 0.Definition 6.
(synchronous behavior of a microservices system). A synchronous behavior of a microservices system over a set of microservices (MS1, MS2, …, MSn), where MSi = MSi = (Si, s0i, Fi, Mi, δi) and Mi = (Σi, pi, srci, dsti), is denoted by a labeled transition system Bs = (C, c0, F, M, Δ), where(i)
C⊆S1×S2⋯×Sn is the set of states.(ii)
c0 ∈ C is the initial state.(iii)
F ⊆ C is the set of final states such that ∀f ∈ F = (f1, f2, …, fn) where fi ∈ MSi·Fi.(iv)
M = ∪iMi is the set of messages.(v)
Δ ⊆C × (M ∪ {ε}) × C for c = (s1, s2, …, sn) and c′=s1′,s2′,…,sn′.(a)
c⟶!mi⟶jc′ ∈ Δ if ∃i, j ∈ {1, 2, …, n}∧m ∈ M:(i)
src(m) = i∧dst(m) = j,(ii)
si⟶!mi⟶jsi′ ∈ δi,(iii)
sj⟶!mi⟶jsj′ ∈ δj,(iv)
∀k ∈ {1, 2, …, n} : k ≠ i∧k ≠ j ⟹ sk′ = sk.[synchronous send-receive action](b)
c⟶εc′ ∈ Δ if ∃i, j ∈ {1, 2, …, n}:(i)
si⟶εsi′ ∈ δi,(ii)
∀k ∈ {1, 2, …, n} : k ≠ i ⟹ sk′ = sk,[internal action]
Figure4 illustrates the synchronous behavior of a microservice system shown in Figure 1. The behavior of the system have transitions a1⟶2, followed by a1⟶2, followed by b1⟶2, and followed by c3⟶2.Figure 4
The synchronous interaction behavior of the microservice system shown in Figure1.


## 5. Interaction Soundness-Based Verification

Given a microservice system, one crucial problem is to check whether the interaction behavior is correct. In this paper, we check whether the interaction behavior of a microservice system satisfies a minimal requirement for correctness using model-checking techniques. The whole process includes the following three steps:(1)
We introduce a notion of correctness called ‘interaction soundness’ which is considered as a minimal requirement for microservice systems(2)
We present an encoding of the interaction behavior into the CSP# process(3)
We translate the property interaction soundness into LTL formulas such that we can verify this property using model-checking techniques under the support by the PAT verifier.


### 5.1. Interaction Soundness

Let us further analyze the asynchronous interaction behavior of a microservice system with buffers of size 2 shown in Figure3(a). When the execution of the microservice system is along the sequence of send and receive actions circled by a red dashed line, the terminating state is c17 which denotes that each participating microservice reaches its corresponding final state, but the message queue buffer12 of MS1 and the message queue buffer21 of MS2 are not empty. In other words, there is an interaction fault which causes messages a1⟶2 and d1⟶2 not to be consumed correctly.In Figure5, we take a snapshot of the system in c17. There are two messages a1⟶2 in buffer12 of MS1 and one message d1⟶2 in buffer21 of MS2.Figure 5
A snapshot of a microservice system inc17.Based on the above analysis, we use the interaction correctness criterion as a minimal requirement any microservice system should satisfy. In particular, the requirement is described as follows.For any case, the microservice system will terminate eventually and the moment the system terminates the terminating state is the final state.Definition 7.
(interaction soundness under synchronous communication). A microservice systemBs = (M, C, F, c0, Δ) is interaction soundness under synchronous communication if and only if the following condition is satisfied.
For every statec reachable from the initial state c0, there exists a transition sequence leading from state c to a final state cx. Formally,(1)∀c∈C∧c0⟶!mi⟶jc1⟶!mi⟶j⋯⟶!mi⟶jc⟹c⟶!mi⟶jcn+1⟶!mi⟶j⋯⟶!mi⟶jcx∧cx∈F.Definition 8.
(interaction soundness under unbounded asynchronous communication or k-bounded asynchronous communication). A microservice systemBa = (M, C, F, c0, Δ) or Bak=C,c0,F,M,Δ is interaction soundness under unbounded asynchronous communication or k-bounded asynchronous communication if and only if the following condition is satisfied.
For every statec reachable from the initial state c0, there exists a transition sequence leading from state c to a final state cx. Formally,(2)∀c∈C∧c0⟶!mi⟶jc1⟶!mi⟶j⋯⟶!mi⟶jc⟹c⟶!mi⟶jcn+1⟶!mi⟶j⋯⟶!mi⟶jcx∧cx∈F.
The difference between Definitions7 and 8 is that the states of the former are described in terms of local states of the participating microservices, while the states of the latter are described in terms of local states of the participating microservices and their respective buffers.


### 5.2. CPS# Encoding for the Behaviors of Microservice Systems

We first discuss how to encode an asynchronous interaction behavior of a microservice system as a CSP# process. Then, we discuss how to encode a synchronous interaction behavior.The CSP# process encoding an asynchronous interaction behavior of a microservice system mainly includes the following three steps:(1)
Encodes all the transitions in each microservice as events in CSP#. For example, the send-transition (s1, !m1⟶2, s2) is encoded as an event !m and the receive-transition (s1, ?m1⟶2, s2) is encoded as an event ?m.(2)
Encodes the order in which the adjacent transitions are executed as prefix or external choice in CSP#. For example, the order in which the microserviceMS1 executes transitions in Figure 1 is a1⟶2, followed by a1⟶2 and b1⟶2 which can be encoded as !a->!a->!b- > Skip without considering buffers.(3)
Encodes peer-to-peer asynchronous communication. In CSP#, the channel can be used to encode a buffer. Because each buffer is specific to the pair (sender, receiver) in the peer-to-peer asynchronous communication, we use the processbufferij!m ⟶ P to denote that the sender MSi sends the message m to the bufferij of the receiver MSj. Conversely, we use the process bufferij[x = = m]?m ⟶ P to denote that the receiver MSj consumes the message m from its bufferij, where the expression [x = = m] is used to check whether the top element in the bufferij is the matching message m.Given a microservice systemBa = (M, C, F, c0, Δ) over a set of microservices {MS1, MS2, …, MSn}, we generate the CSP# process by using Algorithm 1.Algorithm 1: Encoding an asynchronous interaction behavior.
Input: a microservice system Ba = (C, c0, F, M, Δ)
Output: a CSP# process
(1)
{buffer12,…, buffern−1n} = gen_buffers(Ba·C)
(2)
set{buffer12,…, buffern−1n}’s size
(3)
gen_message_variable(Ba·M})
(4)
forMS
i ∈ (MS1, MS2, …, MSn) do
(5)
{σ1,…, σn} = trace(MSi)
(6)
forσj ∈ (σ1,…, σn) do
(7)
z = 1
(8)
while (m = getHead(σj))! = null
(9)
iftype(m) = = “!”
(10)
Pz() = buffersrc(m)_dst(m)!action(m) ⟶ Pz+1()
(11)
else
(12)
Pz() = buffersrc(m)_dst(m)[xz = = action(m)]?action(m) ⟶ Pz+1()
(13)
z = z + 1
(14)
end if
(15)
end while
(16)
PMSi() = P1()
(17)
end for
(18)
end for
(19)
System
() = PMS1()|||PMS1()|||…|||PMSn()Functiongen_buffers generates all the buffers in a microservice system:(3)gen_buffersBa⋅C=bufferi,j∀i,j∈1,2,…,n.Functiongen_message_variable generates message variables in a microservice system:(4)gen_message_variableBa⋅M=1,2,…,Mtotal.Functiontrace() obtains a set of sequences of send and receive messages on any path from the initial state s0:(5)traceM1=sortσi∀m∈M1⋅M:m∈σi,where the function sort(σi) sorts the messages on the path by their execution order.For a message!m1⟶2∈M, function action(!m1⟶2) = m denotes the message and function type(!m1⟶2) = ! denotes the message type.Letm, n, and p be separately the number of microservices, the max number of the traces, and the max number of messages on a branch. The worst time complexity of Algorithm 1 is (m∗n∗p).Example 1.
For the microservice system with buffers of size 2 shown in Figure3, the CSP# process is shown below:////////////////The buffers//////////////////channelbuffer12 2;channelbuffer13 2;channelbuffer21 2;channelbuffer23 2;channelbuffer31 2;channelbuffer32 2;////////////////The messages//////////////////vara = 1;varb = 2;varc = 3;vard = 4;//////////The process of each participating microservice///////PMS1() = buffer12!a ⟶ buffer12!a ⟶ buffer13!b ⟶ Skip;PMS2() = buffer12? 1 ⟶ buffer12? 1 ⟶ buffer32? 3 ⟶ Skip[]buffer32? 3 ⟶ buffer21!d ⟶ Skip;PMS3() = buffer13?2 ⟶ buffer32!c ⟶ Skip;//////The process of an asynchronous interaction behavior of a microservice system //////System() = PMS1()|||PMS2()|||PMS3().
Because synchronous communication is a special case of asynchronous communication (i.e., the size of buffer is set to 0), the CSP# process of a synchronous behavior can be generated by using Algorithm1 except setting the size of bufferij to be 0.


### 5.3. LTL Formulas of Interaction Soundness

After generating the CSP# process of a microservice system using Algorithm1, we can generate the state space of the CSP# process using the PAT simulator and verify temporal logic properties using the PAT verifier. Thus, we need to translate Definitions 7 and 8 into LTL formulas.The property interaction soundness under synchronous communication can be defined as follows:(6)system=“init”‐><>“terminate”&&F,where init denotes the initial state of the system, terminate denotes the final state of the system, and F denotes strong fairness conditions.The property interaction soundness under asynchronous communication can be defined as follows:(7)#definebufijcallcempty,bufferij==true;system=“init”‐><>“terminate”&&bufij&&F,where cempty is channel operation which is a Boolean function to test whether the asynchronous channel is empty or not and bufferij is channel specific to the pair (MSi, MSj) which denotes the buffer of a microservice MSj.Example 2.
For the microservice system with buffers of size 3 shown in Figure3, the LTL formula of the property interaction soundness is defined as follows:#define buf12 call(cempty,buffer12) = = true;#define buf13 call(cempty,buffer13) = = true;#define buf21 call(cempty,buffer21) = = true;#define buf23 call(cempty,buffer23) = = true;#define buf31 call(cempty,buffer31) = = true;#define buf32 call(cempty,buffer32) = = true;#assert System()| = [](“init”-> <> (“terminate” && buf12 && buf13 && buf21 && buf23 && buf31 && buf32));


## 5.1. Interaction Soundness

Let us further analyze the asynchronous interaction behavior of a microservice system with buffers of size 2 shown in Figure3(a). When the execution of the microservice system is along the sequence of send and receive actions circled by a red dashed line, the terminating state is c17 which denotes that each participating microservice reaches its corresponding final state, but the message queue buffer12 of MS1 and the message queue buffer21 of MS2 are not empty. In other words, there is an interaction fault which causes messages a1⟶2 and d1⟶2 not to be consumed correctly.In Figure5, we take a snapshot of the system in c17. There are two messages a1⟶2 in buffer12 of MS1 and one message d1⟶2 in buffer21 of MS2.Figure 5
A snapshot of a microservice system inc17.Based on the above analysis, we use the interaction correctness criterion as a minimal requirement any microservice system should satisfy. In particular, the requirement is described as follows.For any case, the microservice system will terminate eventually and the moment the system terminates the terminating state is the final state.Definition 7.
(interaction soundness under synchronous communication). A microservice systemBs = (M, C, F, c0, Δ) is interaction soundness under synchronous communication if and only if the following condition is satisfied.
For every statec reachable from the initial state c0, there exists a transition sequence leading from state c to a final state cx. Formally,(1)∀c∈C∧c0⟶!mi⟶jc1⟶!mi⟶j⋯⟶!mi⟶jc⟹c⟶!mi⟶jcn+1⟶!mi⟶j⋯⟶!mi⟶jcx∧cx∈F.Definition 8.
(interaction soundness under unbounded asynchronous communication or k-bounded asynchronous communication). A microservice systemBa = (M, C, F, c0, Δ) or Bak=C,c0,F,M,Δ is interaction soundness under unbounded asynchronous communication or k-bounded asynchronous communication if and only if the following condition is satisfied.
For every statec reachable from the initial state c0, there exists a transition sequence leading from state c to a final state cx. Formally,(2)∀c∈C∧c0⟶!mi⟶jc1⟶!mi⟶j⋯⟶!mi⟶jc⟹c⟶!mi⟶jcn+1⟶!mi⟶j⋯⟶!mi⟶jcx∧cx∈F.
The difference between Definitions7 and 8 is that the states of the former are described in terms of local states of the participating microservices, while the states of the latter are described in terms of local states of the participating microservices and their respective buffers.


## 5.2. CPS# Encoding for the Behaviors of Microservice Systems

We first discuss how to encode an asynchronous interaction behavior of a microservice system as a CSP# process. Then, we discuss how to encode a synchronous interaction behavior.The CSP# process encoding an asynchronous interaction behavior of a microservice system mainly includes the following three steps:(1)
Encodes all the transitions in each microservice as events in CSP#. For example, the send-transition (s1, !m1⟶2, s2) is encoded as an event !m and the receive-transition (s1, ?m1⟶2, s2) is encoded as an event ?m.(2)
Encodes the order in which the adjacent transitions are executed as prefix or external choice in CSP#. For example, the order in which the microserviceMS1 executes transitions in Figure 1 is a1⟶2, followed by a1⟶2 and b1⟶2 which can be encoded as !a->!a->!b- > Skip without considering buffers.(3)
Encodes peer-to-peer asynchronous communication. In CSP#, the channel can be used to encode a buffer. Because each buffer is specific to the pair (sender, receiver) in the peer-to-peer asynchronous communication, we use the processbufferij!m ⟶ P to denote that the sender MSi sends the message m to the bufferij of the receiver MSj. Conversely, we use the process bufferij[x = = m]?m ⟶ P to denote that the receiver MSj consumes the message m from its bufferij, where the expression [x = = m] is used to check whether the top element in the bufferij is the matching message m.Given a microservice systemBa = (M, C, F, c0, Δ) over a set of microservices {MS1, MS2, …, MSn}, we generate the CSP# process by using Algorithm 1.Algorithm 1: Encoding an asynchronous interaction behavior.
Input: a microservice system Ba = (C, c0, F, M, Δ)
Output: a CSP# process
(1)
{buffer12,…, buffern−1n} = gen_buffers(Ba·C)
(2)
set{buffer12,…, buffern−1n}’s size
(3)
gen_message_variable(Ba·M})
(4)
forMS
i ∈ (MS1, MS2, …, MSn) do
(5)
{σ1,…, σn} = trace(MSi)
(6)
forσj ∈ (σ1,…, σn) do
(7)
z = 1
(8)
while (m = getHead(σj))! = null
(9)
iftype(m) = = “!”
(10)
Pz() = buffersrc(m)_dst(m)!action(m) ⟶ Pz+1()
(11)
else
(12)
Pz() = buffersrc(m)_dst(m)[xz = = action(m)]?action(m) ⟶ Pz+1()
(13)
z = z + 1
(14)
end if
(15)
end while
(16)
PMSi() = P1()
(17)
end for
(18)
end for
(19)
System
() = PMS1()|||PMS1()|||…|||PMSn()Functiongen_buffers generates all the buffers in a microservice system:(3)gen_buffersBa⋅C=bufferi,j∀i,j∈1,2,…,n.Functiongen_message_variable generates message variables in a microservice system:(4)gen_message_variableBa⋅M=1,2,…,Mtotal.Functiontrace() obtains a set of sequences of send and receive messages on any path from the initial state s0:(5)traceM1=sortσi∀m∈M1⋅M:m∈σi,where the function sort(σi) sorts the messages on the path by their execution order.For a message!m1⟶2∈M, function action(!m1⟶2) = m denotes the message and function type(!m1⟶2) = ! denotes the message type.Letm, n, and p be separately the number of microservices, the max number of the traces, and the max number of messages on a branch. The worst time complexity of Algorithm 1 is (m∗n∗p).Example 1.
For the microservice system with buffers of size 2 shown in Figure3, the CSP# process is shown below:////////////////The buffers//////////////////channelbuffer12 2;channelbuffer13 2;channelbuffer21 2;channelbuffer23 2;channelbuffer31 2;channelbuffer32 2;////////////////The messages//////////////////vara = 1;varb = 2;varc = 3;vard = 4;//////////The process of each participating microservice///////PMS1() = buffer12!a ⟶ buffer12!a ⟶ buffer13!b ⟶ Skip;PMS2() = buffer12? 1 ⟶ buffer12? 1 ⟶ buffer32? 3 ⟶ Skip[]buffer32? 3 ⟶ buffer21!d ⟶ Skip;PMS3() = buffer13?2 ⟶ buffer32!c ⟶ Skip;//////The process of an asynchronous interaction behavior of a microservice system //////System() = PMS1()|||PMS2()|||PMS3().
Because synchronous communication is a special case of asynchronous communication (i.e., the size of buffer is set to 0), the CSP# process of a synchronous behavior can be generated by using Algorithm1 except setting the size of bufferij to be 0.


## 5.3. LTL Formulas of Interaction Soundness

After generating the CSP# process of a microservice system using Algorithm1, we can generate the state space of the CSP# process using the PAT simulator and verify temporal logic properties using the PAT verifier. Thus, we need to translate Definitions 7 and 8 into LTL formulas.The property interaction soundness under synchronous communication can be defined as follows:(6)system=“init”‐><>“terminate”&&F,where init denotes the initial state of the system, terminate denotes the final state of the system, and F denotes strong fairness conditions.The property interaction soundness under asynchronous communication can be defined as follows:(7)#definebufijcallcempty,bufferij==true;system=“init”‐><>“terminate”&&bufij&&F,where cempty is channel operation which is a Boolean function to test whether the asynchronous channel is empty or not and bufferij is channel specific to the pair (MSi, MSj) which denotes the buffer of a microservice MSj.Example 2.
For the microservice system with buffers of size 3 shown in Figure3, the LTL formula of the property interaction soundness is defined as follows:#define buf12 call(cempty,buffer12) = = true;#define buf13 call(cempty,buffer13) = = true;#define buf21 call(cempty,buffer21) = = true;#define buf23 call(cempty,buffer23) = = true;#define buf31 call(cempty,buffer31) = = true;#define buf32 call(cempty,buffer32) = = true;#assert System()| = [](“init”-> <> (“terminate” && buf12 && buf13 && buf21 && buf23 && buf31 && buf32));


## 6. Implementation and Experiments

### 6.1. Implementation

Our approach is completely automated. First, we have implemented an encoder which takes a microservice system as input and outputs the corresponding CSP# process. Second, once the CSP# process is obtained, we can generate the state space of the asynchronous interaction behavior of the microservice system using the PAT simulator which is defined in an LTS. Third, we verify whether the generated state space satisfies the property interaction soundness using the PAT verifier.The generated asynchronous interaction behavior of the microservice system with buffers of size 3 shown in Figure1 is shown in Figure 6 using the PAT simulator. The verification result shown in Figure 7 returns not valid, which means that the microservice system with buffers of size 3 has an interaction fault.Figure 6
A snapshot of the asynchronous interaction behavior using the PAT simulator.Figure 7
A snapshot of the verification result using the PAT verifier.


### 6.2. Experiments

To validate our approach, we use 10 cases obtained from the literature. We choose these cases because the literature is representative. All cases were carried out on a PC with 2.50 GHz Processor and 8 GB of RAM, running Windows 10.Table1 shows the experimental results for all the cases we conducted. The table gives for each case the number of participating microservices (MSs) involved in a microservice system, the number of messages (Ms), the size of the LTS of the synchronous interaction behaviors of a microservice system (Bs), the verification result under synchronous communication (IRa) (“−” denotes that the system is not interaction sound and “+” denotes that the system is interaction sound), the size of the LTS of the asynchronous interaction behaviors of a microservice system with buffers of size k (Bak), and the verification result under k-bounded asynchronous communication (IRs).Table 1
Verification results for all cases.
Id
Description
Number
B
s
B
a
1
B
a
2
B
a
3
|MSs|
|Ms|
LTS(|T|/|S|)
IR
a
LTS(|T|/|S|)
IR
s
LTS(|T|/|S|)
IR
s
LTS(|T|/|S|)
IR
s
Ca-01 [33]
Booking system
4
7
(10,11)
−
(23\29)
−
(24\31)
−
(24\31)
−
Ca-02 [34]
Train station
4
8
(11,13)
+
(44,76)
−
(64,122)
−
(84,168)
−
Ca-03 [32]
Protocol
3
3
(7,14)
+
(26,62)
−
(35,91)
−
(44,120)
−
Ca-04 [35]
Online shopping
3
6
(7,7)
+
(13,13)
+
(13,13)
+
(13,13)
+
Ca-05 [36]
Cloud application
4
5
(6,10)
−
(96,240)
−
Too large
−
Too large
−
Ca-06 [37]
Figure 2
3
3
(3,3)
+
(10,14)
−
(15,24)
−
(20,34)
−
Ca-07 [38]
Figure 1
4
5
(11,14)
+
(28,43)
+
(28,43)
+
(28,43)
+
Ca-08 [15]
Composition 2
2
5
(5,6)
+
(10,11)
+
(10,11)
+
(10,11)
+
Ca-09 [39]
Figure 8
3
3
(7,6)
−
(16,20)
−
(16,20)
−
(16,20)
−
Ca-10 [14]
Figure 1
3
4
(6,5)
+
(13,15)
+
(20,26)
−
(20,26)
−Out of the 10 cases presented in Table1, 7 cases can be interaction sound under synchronous communication, e.g., see cases Ca-02, Ca-03, Ca-04, Ca-06, Ca-07, Ca-08, and Ca-10. In 7 cases, microservice systems with buffers of size 3 are not interaction sound, e.g., see cases Ca-01, Ca-02, Ca-03, Ca-05, Ca-06, Ca-09, and Ca-10.From Table1, we can further see that, (1) in each case, the LTS of the asynchronous interaction behavior of a microservice system is bigger than that of the synchronous interaction behavior, i.e., the asynchronous interaction behavior is more complex than the synchronous interaction behavior; (2) the asynchronous interaction behavior of some microservice systems is stable, i.e., once the size of the LTS of the asynchronous interaction behavior remains unchanged for a buffer bound, e.g., see cases Ca-04, Ca-07, Ca-08, Ca-09, and Ca-10. This property on the system is called stable which is proposed in [40]; (3) when some microservice systems with buffers of size 1 are interaction sound, it does not mean that the systems with buffers of size k (k > 1) are also interaction sound, e.g., see the case Ca-10; (4) during the experiments, Case-5 faces the state space explosion problem. “Too large” means that the PAT simulator is forced to stop due to the huge state space size (>300 states).


## 6.1. Implementation

Our approach is completely automated. First, we have implemented an encoder which takes a microservice system as input and outputs the corresponding CSP# process. Second, once the CSP# process is obtained, we can generate the state space of the asynchronous interaction behavior of the microservice system using the PAT simulator which is defined in an LTS. Third, we verify whether the generated state space satisfies the property interaction soundness using the PAT verifier.The generated asynchronous interaction behavior of the microservice system with buffers of size 3 shown in Figure1 is shown in Figure 6 using the PAT simulator. The verification result shown in Figure 7 returns not valid, which means that the microservice system with buffers of size 3 has an interaction fault.Figure 6
A snapshot of the asynchronous interaction behavior using the PAT simulator.Figure 7
A snapshot of the verification result using the PAT verifier.


## 6.2. Experiments

To validate our approach, we use 10 cases obtained from the literature. We choose these cases because the literature is representative. All cases were carried out on a PC with 2.50 GHz Processor and 8 GB of RAM, running Windows 10.Table1 shows the experimental results for all the cases we conducted. The table gives for each case the number of participating microservices (MSs) involved in a microservice system, the number of messages (Ms), the size of the LTS of the synchronous interaction behaviors of a microservice system (Bs), the verification result under synchronous communication (IRa) (“−” denotes that the system is not interaction sound and “+” denotes that the system is interaction sound), the size of the LTS of the asynchronous interaction behaviors of a microservice system with buffers of size k (Bak), and the verification result under k-bounded asynchronous communication (IRs).Table 1
Verification results for all cases.
Id
Description
Number
B
s
B
a
1
B
a
2
B
a
3
|MSs|
|Ms|
LTS(|T|/|S|)
IR
a
LTS(|T|/|S|)
IR
s
LTS(|T|/|S|)
IR
s
LTS(|T|/|S|)
IR
s
Ca-01 [33]
Booking system
4
7
(10,11)
−
(23\29)
−
(24\31)
−
(24\31)
−
Ca-02 [34]
Train station
4
8
(11,13)
+
(44,76)
−
(64,122)
−
(84,168)
−
Ca-03 [32]
Protocol
3
3
(7,14)
+
(26,62)
−
(35,91)
−
(44,120)
−
Ca-04 [35]
Online shopping
3
6
(7,7)
+
(13,13)
+
(13,13)
+
(13,13)
+
Ca-05 [36]
Cloud application
4
5
(6,10)
−
(96,240)
−
Too large
−
Too large
−
Ca-06 [37]
Figure 2
3
3
(3,3)
+
(10,14)
−
(15,24)
−
(20,34)
−
Ca-07 [38]
Figure 1
4
5
(11,14)
+
(28,43)
+
(28,43)
+
(28,43)
+
Ca-08 [15]
Composition 2
2
5
(5,6)
+
(10,11)
+
(10,11)
+
(10,11)
+
Ca-09 [39]
Figure 8
3
3
(7,6)
−
(16,20)
−
(16,20)
−
(16,20)
−
Ca-10 [14]
Figure 1
3
4
(6,5)
+
(13,15)
+
(20,26)
−
(20,26)
−Out of the 10 cases presented in Table1, 7 cases can be interaction sound under synchronous communication, e.g., see cases Ca-02, Ca-03, Ca-04, Ca-06, Ca-07, Ca-08, and Ca-10. In 7 cases, microservice systems with buffers of size 3 are not interaction sound, e.g., see cases Ca-01, Ca-02, Ca-03, Ca-05, Ca-06, Ca-09, and Ca-10.From Table1, we can further see that, (1) in each case, the LTS of the asynchronous interaction behavior of a microservice system is bigger than that of the synchronous interaction behavior, i.e., the asynchronous interaction behavior is more complex than the synchronous interaction behavior; (2) the asynchronous interaction behavior of some microservice systems is stable, i.e., once the size of the LTS of the asynchronous interaction behavior remains unchanged for a buffer bound, e.g., see cases Ca-04, Ca-07, Ca-08, Ca-09, and Ca-10. This property on the system is called stable which is proposed in [40]; (3) when some microservice systems with buffers of size 1 are interaction sound, it does not mean that the systems with buffers of size k (k > 1) are also interaction sound, e.g., see the case Ca-10; (4) during the experiments, Case-5 faces the state space explosion problem. “Too large” means that the PAT simulator is forced to stop due to the huge state space size (>300 states).


## 7. Conclusion and Future Work

In this paper, we introduce a formal model for modeling complex interactions of microservice systems and verify whether these systems satisfy a minimal requirement for correctness using model-checking techniques. We have used LTLs to model complex interactions of microservice systems under synchronous and asynchronous communications and introduced a notion of correctness called “interaction soundness” which is considered as a minimal requirement for microservice systems. We automatically verified the property interaction soundness under the support of the PAT tool. Experiments showed that many cases have interaction faults.Our future work is to investigate whether our results stand for mailbox communication, e.g., each microservice is equipped with one buffer which is used to store incoming messages from the other microservices.



---

*Source: 2128793-2020-03-31.xml*