# A Correctness Checking Approach for Collaborative Business Processes in the Cloud

Authors: Qi Mo; Yuqi Wang; Jixiang Xiang; Tong Li
Journal: Complexity
 (2020)

---

## Abstract

With the increasing popularity of cloud computing, especially the emergence of Business Process as a Service (BPaaS), more and more enterprises construct their process collaborations based on BPaaS services. Indeed, the collaborative business process built by BPaaS services can be seen as a complex system, as it covers multiple business processes (i.e., BPaaS services) and they act independently. Since business processes corresponding to BPaaS services are usually provided by different cloud service providers, and their interactions are unforeseen in advance, in actual execution, some behavioral anomalies (e.g., deadlocks) may occur. To this end, based on BPaaS services, we propose an approach to build process collaborations in the cloud. In this approach, we first model collaborative business processes using open nets. Then, we check their correctness based on stubborn sets. Finally, in case they are partially correct, we generate reliable paths for the coordination execution between business processes. Our approach is implemented in the PIPE (an open tool for Petri nets) and evaluated on actual cases that show its effectiveness and efficiency.


---

## Body

## 1. Introduction

Currently, the new paradigm cloud computing has received great attention, as it can deliver shared services (e.g., computing capacity, storage, and software applications) to clients over the Internet in a ubiquitous, convenient, and on-demand way with a minimal management effort [1–3].With the widespread application of cloud computing, especially the emergence of BPaaS (a cloud service that can be delivered to clients in the form of processes) [4], more and more enterprises deploy their business processes to the cloud to achieve value-added services. Based on the cloud platform, such as keyword search [5], enterprises residing on the cloud can find and compose some business processes with complementary competencies and knowledge (i.e., BPaaS services) into their business processes to build collaborative business processes to achieve business success [6–8]. For example, for a retailer residing on the cloud, its transportation process can be outsourced to a BPaaS service that coordinates the actual transportation to improve the effectiveness and efficiency. In practice, this model brings at least two benefits to enterprises. First, enterprises can more easily build their collaborative business processes than ever before, as BPaaS services can be directly invoked in the cloud without having to develop them independently [9]. Second, collaborative business processes built by BPaaS services are more scalable and reliable because they are deployed in the cloud.In fact, the collaborative business process built by composing business processes (i.e., BPaaS services) gathered in the cloud can be seen as a complex system, as it covers multiple business processes and these business processes act independently [10]. In the cloud, these business processes are usually developed by different organizations and their interactions are unforeseen by interactive parties. Consequently, behavioral anomalies (e.g., deadlocks) may be caused and eventually have an adverse impact on the execution of their composition.In order to eliminate these behavioral anomalies, the correctness checking approach is dominant in existing approaches [6, 10–13]. Given a collaborative business process, the approach automatically detects its correctness (e.g., soundness [6]) using formal techniques (e.g., model checking). In case it is incorrect, developers can repair it via diagnosis information described by a trace leading to errors.However, in the actual checking process, existing approaches for correctness checking [6, 10, 11] usually need to construct the full state space (i.e., a direct graph that covers all reachable states and edges between states) of collaborative business processes, and hence, they may suffer from the low efficiency. Some approaches [12, 13] do exist that focus on improving the checking efficiency. Concretely, these approaches first abstract business processes in the collaboration as public views. Then, they compose these public views to build an abstract collaborative process. Finally, they detect the correctness based on the abstract collaborative process. In general, these approaches can improve checking efficiency while considering privacy. Yet, they require business processes in the collaboration to be structured. Note that the term “structured” means that the business process only contains the sequence, concurrency, selection, and loop structures, and it is formed through the composition of these four structures. Since the assumption may not hold in practice [14], the efficiency of their correctness checking may not increase significantly. Additionally, they do not consider the fact that business processes in the collaboration are typically partially correct (there is at least one path in the collaboration process, and from which the collaboration process can be successfully terminated) [15, 16], and hence, they cannot generate reliable paths for each business process. In particular, a reliable execution path can be seen as a collaborative work plan between a set of business processes [17], and from which their collaboration can be successfully terminated.To address these problems, based on stubborn sets in [18], this paper proposes an approach to build collaboration processes in the cloud (see Figure 1). Concretely, in our approach, we first model collaborative business processes based on BPaaS services using open nets [19]. Afterwards, we check their correctness based on stubborn sets. At last, in case they are partially correct, we generate reliable paths for the coordination execution between business processes.Figure 1
Overview of our approach.The main contributions of this paper are summarized as follows:(1)
We present a method for rapid correctness checking based on stubborn sets(2)
We propose a method for generating reliable paths for the coordination execution between business processes(3)
The proposed approach is implemented in the PIPE, and its effectiveness and efficiency are validated with actual casesThe paper has the following organizations.Section 2 gives a motivating example to illustrate our approach throughout the paper. Section 3 introduces open nets and uses them to model collaborative business processes. Section 4 presents the method for checking correctness based on the stubborn set. Section 5 proposes a method for generating reliable paths for each business process. Section 6 introduces our prototype tool called cctool and evaluates our approach based on real-world cases. Section 7 compares the related work. Section 8 concludes this paper.


## 2. Motivating Example

To achieve additional value-added services, a supplierSupp deploys its ordering process to the cloud as a BPaaS service for other enterprises to invoke. Based on the cloud platform, a retailer Reta residing on the cloud finds the service and composes it into its process to build a collaborative business process OP to achieve business success.With BPMN, the processes ofSupp and Reta are depicted in Figure 2, where Supp can receive ordering requests from Reta. In general, the product A in Supp is sufficient, and hence, Supp receives the request for ordering product A in any case. However, product B in Supp is insufficient in some cases. Thus, Supp first checks its stock and then receives the request for ordering product B. In case order A or B is received, Supp sends the ordered product to Reta. After that, Reta is able to sell it to customers for an intermediate profit.Figure 2
OP.Generally, the business processes ofReta and Supp in the cloud are independently developed by different cloud service providers; thereby, all potential interactions between them are unforeseen in advance. Consequently, some behavioral anomalies, such as deadlocks, may occur during OP’s actual execution. For instance, in OP, if Supp waits to receive the order of product B while Reta sends an order of product A; then, a deadlock occurs, and it is depicted as red lines in Figure 2.In order to avoid these behavioral anomalies, we propose a method to check OP’s correctness based on the stubborn set in this paper. In case of partially correct, we then present a method to generate all reliable execution paths for the coordination execution betweenReta and Supp. In actual execution, based on these reliable paths, the interaction between Reta and Supp can be successfully terminated.


## 3. Modeling Methods

In this section, we first briefly introduce the concept of open nets [19] and then illustrate the method to model collaborative business processes based on BPaaS services.


### 3.1. Open Nets

In this paper, open nets will be used to describe business processes and their composition, which can be used to model collaborative business processes in the cloud. Compared with the traditional Petri nets, open nets are enriched with message places to model asynchronous message channels between business processes (e.g., BPaaS services) in the cloud [19]. Open net can be formally defined as follows.Definition 1.
(Open Net). An open net can be defined as a tupleN=(P, T; F, M0, Me), where(1)
P is a set of places, PI⊆P are internal places, and PM⊆P are message places, such that PI∩PM=∅(2)
T and F are the transitions and flow relation of N(3)
M0 is the initial marking, such that M0(i) = 1, and M(p) = 0 for place p≠i, where i is the source place(4)
Me is the final marking, such that M0(o) = 1, and M(p) = 0 for place p≠o, where o is the sink place
Using the place fusion technique [4, 20], we can compose multiple open nets into an open net. Given two open nets, their composition can be formally defined as follows.Definition 2.
(Composition). The composition of two open netsN1 = (P1, T1; F1, M01, Me1) and N2 = (P2, T2; F2, M02, Me2) can be described as an open net N1||N2 = (P, T; F, M0, Me), where(1)
P=P1∪P2(2)
T=T1∪T2(3)
F=F1∪F2(4)
M0 is an initial marking, such that M0(i1) = 1∧M0(i2) = 1, and M(p) = 0 for place p≠i1 and p≠i2(5)
Me is a final marking, such that Me (o1) = 1∧Me(o2) = 1, and M(p) = 0 for place p≠ o1 and p≠ o2
Clearly, according to Definition2, we can conclude that the composition is both associative and commutative. Consequently, given a set of open nets, their composition can be noted as N1⋯Nn.


### 3.2. Modeling Collaborative Business Processes

In [21], based on open nets, we proposed a method to construct collaborative business processes. Its basic idea is that we first convert all business processes in the collaboration into open nets based on their informal descriptions and then compose these open nets to generate a collaborative business process. The method can also be used in our context. That is, we first map the business process corresponding to each BPaaS service for collaboration to an open net, and then, a collaboration process can be built by composing these open nets.Note that in this paper, we restrict ourselves to business processes that cover no loops, as the loop in the process model can typically be converted into a sequential structure [22].Example 1.
To formally construct collaborative business process OP, based on its description, we first convert the business processes corresponding to the BPaaS services ofReta and Supp into two open nets, i.e., N1 and N2 in Figure 3. In particular, in Figure 3, the red places indicate message places, and the label of each transition is described in Table 1.
Then, we can formally construct OP by composing the two open nets, as shown in Figure4.Figure 3
Open nets. (a) Open netN1 corresponding to Reta. (b) Open net N2 corresponding to Supp.Table 1
Labels ofN1 and N2.
Transition
Label
t
1
Send orderA
t
2
Send orderB
t
3
Receive product
t
4
Check stock
t
5
ReceiveB-order
t
6
ReceiveA-order
t
8
Send productFigure 4
Collaborative business process OP.


## 3.1. Open Nets

In this paper, open nets will be used to describe business processes and their composition, which can be used to model collaborative business processes in the cloud. Compared with the traditional Petri nets, open nets are enriched with message places to model asynchronous message channels between business processes (e.g., BPaaS services) in the cloud [19]. Open net can be formally defined as follows.Definition 1.
(Open Net). An open net can be defined as a tupleN=(P, T; F, M0, Me), where(1)
P is a set of places, PI⊆P are internal places, and PM⊆P are message places, such that PI∩PM=∅(2)
T and F are the transitions and flow relation of N(3)
M0 is the initial marking, such that M0(i) = 1, and M(p) = 0 for place p≠i, where i is the source place(4)
Me is the final marking, such that M0(o) = 1, and M(p) = 0 for place p≠o, where o is the sink place
Using the place fusion technique [4, 20], we can compose multiple open nets into an open net. Given two open nets, their composition can be formally defined as follows.Definition 2.
(Composition). The composition of two open netsN1 = (P1, T1; F1, M01, Me1) and N2 = (P2, T2; F2, M02, Me2) can be described as an open net N1||N2 = (P, T; F, M0, Me), where(1)
P=P1∪P2(2)
T=T1∪T2(3)
F=F1∪F2(4)
M0 is an initial marking, such that M0(i1) = 1∧M0(i2) = 1, and M(p) = 0 for place p≠i1 and p≠i2(5)
Me is a final marking, such that Me (o1) = 1∧Me(o2) = 1, and M(p) = 0 for place p≠ o1 and p≠ o2
Clearly, according to Definition2, we can conclude that the composition is both associative and commutative. Consequently, given a set of open nets, their composition can be noted as N1⋯Nn.


## 3.2. Modeling Collaborative Business Processes

In [21], based on open nets, we proposed a method to construct collaborative business processes. Its basic idea is that we first convert all business processes in the collaboration into open nets based on their informal descriptions and then compose these open nets to generate a collaborative business process. The method can also be used in our context. That is, we first map the business process corresponding to each BPaaS service for collaboration to an open net, and then, a collaboration process can be built by composing these open nets.Note that in this paper, we restrict ourselves to business processes that cover no loops, as the loop in the process model can typically be converted into a sequential structure [22].Example 1.
To formally construct collaborative business process OP, based on its description, we first convert the business processes corresponding to the BPaaS services ofReta and Supp into two open nets, i.e., N1 and N2 in Figure 3. In particular, in Figure 3, the red places indicate message places, and the label of each transition is described in Table 1.
Then, we can formally construct OP by composing the two open nets, as shown in Figure4.Figure 3
Open nets. (a) Open netN1 corresponding to Reta. (b) Open net N2 corresponding to Supp.Table 1
Labels ofN1 and N2.
Transition
Label
t
1
Send orderA
t
2
Send orderB
t
3
Receive product
t
4
Check stock
t
5
ReceiveB-order
t
6
ReceiveA-order
t
8
Send productFigure 4
Collaborative business process OP.


## 4. Checking Correctness

In this section, we first define the correctness of collaborative business processes based onweak termination [19]. Then, we define the stubborn set for collaborative business processes and present a method for generating the reduced state space. At last, we propose an algorithm to check the correctness of the collaborative business processes based on its reduced state space.


### 4.1. Correctness

In this paper, we employ a special variant ofsoundness [4], i.e., weak termination, to define the correctness of collaborative business processes, because activities in BPaaS services can be used in different collaborations and the exclusion of some activities in a concrete collaboration may not be a design flow in practice [23].Definition 3.
(Correctness). LetN=(P, T; F, M0, Me) be a collaborative business process built by composing BPaaS services in the cloud. Then, for each reachable marking M in N, if M can reach the final marking, then N is called correct.
In essence, Definition 3 implies the fact that each BPaaS service in the collaboration can be successfully terminated, i.e., the final marking can be reached, and the messages generated during the execution ofN can be received.


### 4.2. Stubborn Sets

To check the correctness of collaboration processes, existing approaches (e.g., [6, 10, 11]) typically need to build their full state space at first; thereby, they are inefficient and intractable, even for collaboration processes that are bounded, as the state-space explosion may occur. In order to alleviate the issue, in this paper, we first generate the reduced state space of collaborative business processes using stubborn sets [24] and then check the correctness on it. In this way, our approach can greatly improve checking efficiency for actual collaboration processes.Currently, multiple stubborn sets for verifying different properties have been proposed, such as the stubborn set for simple linear time logic [25]. In general, the construction of the stubborn set is depended on the properties to be verified [26]. We first present the definition of the stubborn set for collaborative business processes based on the concepts related to the stubborn set of Petri nets in [18]. Informally, given a marking M, its stubborn set St(M) refers to a set of enabled transitions at M and St(M) remains stubborn when the transitions outside St(M) fire.Definition 4.
(Stubborn Set). LetN=(P, T; F, M0, Me) be a collaborative business process and M be its marking. Then, the stubborn set St(M) of M can be described as(1)
If∃t∈en(M), then ∃t∈St(M) where t∈en(M)(2)
Ift∈en(M), then∃t••∈St(M)(3)
Ift∉en(M), then∃p∈t•: M(p) = 0 and p•∈St(M)
In Definition4, (1) states that the stubborn set is not empty if there are some enabled transitions at marking M; (2) implies that the conflict set of each transition is included in St(M); and (3) implies that the casual set of each transition is covered in St(M).
With Definition4, below we give an algorithm to calculate the stubborn set corresponding to a special marking.
Algorithm1 first picks any transition from the currently enabled transitions (L1). Then, the algorithm iteratively uses (2) or (3) of Definition 4 until reaching a fixed point (L3∼L11). Assume that N has n transitions, then the time complexity of the algorithm is O(n).Algorithm 1:Compute stubborn sets.
Input:
N = (P, T; F, M0, Me) and marking M
Output: The stubborn set St(M)
(1)
pick anyt ∈ en(M);
(2)
St(M) = {t}; ℝ = {t};
(3)
while ℝ ≠ ∅ do
(4)
pickt ∈ ℝ;
(5)
ift ∉ en(M) then
(6)
Θ = {p•|∃p ∈ t• s.t. M(p) = 0};
(7)
else
(8)
Θ =t••;
(9)
end if
(10)
St(M) = St(M) ∪ Θ;
(11)
ℝ = ℝ ∪ (Θ\St(M));
(12)
end while
(13)
returnSt(M);Example 2.
Using Algorithm1, we can generate a possible stubborn set St(M0) for the initial marking M0 in OP, i.e., St(M0) = {t1, t2}. Concretely, if the algorithm chooses the enabled transition t1 to generate the stubborn set, then transition t2 is added to St(M0) as it is in conflict with transition t1. After that, the algorithm computes the conflict set of transition t2 as it is enabled. Yet, since the conflict set at this point is empty, the algorithm terminates.
With the concept of the stubborn set, the reduced state space of collaborative business processes can be generated using the following algorithm.
Technically, the basic idea of Algorithm2 is similar to the process of generating the reachability graph of Petri nets [20]. The only difference between them is that only the stubborn set is used to generate the successors of the marking at each iteration (L7∼L15). Assume that SGG has n nodes, then the time complexity of the algorithm is O(n).Algorithm 2:Compute the reduced state space.
Input:
N = (P, T; F, M0, Me)
Output: The reduced state space SSG;
(1)
define SSG = (N, E, M0, Me);
(2)
tagM0;
(3)
addM0 to Υ and N;
(4)
whileΥ ≠ ∅ do
(5)
pick anyM ∈ Υ;
(6)
generate the stubborn setSt(M) of M;
(7)
for eacht∈St(M) do
(8)
computeM[t > M’;
(9)
add (M, t, M′) to E;
(10)
ifM′ is untagged then
(11)
tagM’;
(12)
addM′ to Υ and N;
(13)
end if
(14)
end for
(15)
return SSG;


### 4.3. Checking Correctness

In [21], given a collaboration process, we proposed an effective algorithm for checking its correctness with the concept of transitive closures. Here, we briefly describe its basic idea. That is, the algorithm first generates its state space, i.e., the reachability graph. Then, it calculates the transitive closures corresponding to all nodes in the state space with an algorithm called Floyd–Warshall [27]. Finally, the algorithm determines the correctness based on these generated transitive closures. Concretely, if the transitive closures corresponding to all nodes in the state space cover a final marking, then we derive that the collaboration process is correct, and otherwise, it is incorrect. In the case of incorrectness, two cases exist, i.e., if some nodes (not all) in the state space can reach a final marking, then we define that the collaboration process is partially correct, and otherwise it is fully incorrect. In our context, the algorithm is directly employed to check the correctness of a cloud-based collaboration process. Note that the Floyd–Warshall algorithm is a classic algorithm for computing transitive closures. Its basic idea is that given a directed graph, the algorithm first constructs its adjacency matrix and then calculates transitive closures of nodes based on transitive relations [27]. To save space, the details on the algorithm are not presented in this paper.Example 3.
According to the algorithm described in [21], the fact that OP is partially correct can be derived. Concretely, we first calculate OP’s reduced state space SSG, as depicted in Figure 5.
Then, we calculate the transitive closure corresponding to each node in SSG. Clearly, in Figure5, we can see that closure(M5) does not contain Me (i.e., marking M5 cannot reach the final marking), and hence OP is partially correct.Figure 5
Reduced state space of OP.


## 4.1. Correctness

In this paper, we employ a special variant ofsoundness [4], i.e., weak termination, to define the correctness of collaborative business processes, because activities in BPaaS services can be used in different collaborations and the exclusion of some activities in a concrete collaboration may not be a design flow in practice [23].Definition 3.
(Correctness). LetN=(P, T; F, M0, Me) be a collaborative business process built by composing BPaaS services in the cloud. Then, for each reachable marking M in N, if M can reach the final marking, then N is called correct.
In essence, Definition 3 implies the fact that each BPaaS service in the collaboration can be successfully terminated, i.e., the final marking can be reached, and the messages generated during the execution ofN can be received.


## 4.2. Stubborn Sets

To check the correctness of collaboration processes, existing approaches (e.g., [6, 10, 11]) typically need to build their full state space at first; thereby, they are inefficient and intractable, even for collaboration processes that are bounded, as the state-space explosion may occur. In order to alleviate the issue, in this paper, we first generate the reduced state space of collaborative business processes using stubborn sets [24] and then check the correctness on it. In this way, our approach can greatly improve checking efficiency for actual collaboration processes.Currently, multiple stubborn sets for verifying different properties have been proposed, such as the stubborn set for simple linear time logic [25]. In general, the construction of the stubborn set is depended on the properties to be verified [26]. We first present the definition of the stubborn set for collaborative business processes based on the concepts related to the stubborn set of Petri nets in [18]. Informally, given a marking M, its stubborn set St(M) refers to a set of enabled transitions at M and St(M) remains stubborn when the transitions outside St(M) fire.Definition 4.
(Stubborn Set). LetN=(P, T; F, M0, Me) be a collaborative business process and M be its marking. Then, the stubborn set St(M) of M can be described as(1)
If∃t∈en(M), then ∃t∈St(M) where t∈en(M)(2)
Ift∈en(M), then∃t••∈St(M)(3)
Ift∉en(M), then∃p∈t•: M(p) = 0 and p•∈St(M)
In Definition4, (1) states that the stubborn set is not empty if there are some enabled transitions at marking M; (2) implies that the conflict set of each transition is included in St(M); and (3) implies that the casual set of each transition is covered in St(M).
With Definition4, below we give an algorithm to calculate the stubborn set corresponding to a special marking.
Algorithm1 first picks any transition from the currently enabled transitions (L1). Then, the algorithm iteratively uses (2) or (3) of Definition 4 until reaching a fixed point (L3∼L11). Assume that N has n transitions, then the time complexity of the algorithm is O(n).Algorithm 1:Compute stubborn sets.
Input:
N = (P, T; F, M0, Me) and marking M
Output: The stubborn set St(M)
(1)
pick anyt ∈ en(M);
(2)
St(M) = {t}; ℝ = {t};
(3)
while ℝ ≠ ∅ do
(4)
pickt ∈ ℝ;
(5)
ift ∉ en(M) then
(6)
Θ = {p•|∃p ∈ t• s.t. M(p) = 0};
(7)
else
(8)
Θ =t••;
(9)
end if
(10)
St(M) = St(M) ∪ Θ;
(11)
ℝ = ℝ ∪ (Θ\St(M));
(12)
end while
(13)
returnSt(M);Example 2.
Using Algorithm1, we can generate a possible stubborn set St(M0) for the initial marking M0 in OP, i.e., St(M0) = {t1, t2}. Concretely, if the algorithm chooses the enabled transition t1 to generate the stubborn set, then transition t2 is added to St(M0) as it is in conflict with transition t1. After that, the algorithm computes the conflict set of transition t2 as it is enabled. Yet, since the conflict set at this point is empty, the algorithm terminates.
With the concept of the stubborn set, the reduced state space of collaborative business processes can be generated using the following algorithm.
Technically, the basic idea of Algorithm2 is similar to the process of generating the reachability graph of Petri nets [20]. The only difference between them is that only the stubborn set is used to generate the successors of the marking at each iteration (L7∼L15). Assume that SGG has n nodes, then the time complexity of the algorithm is O(n).Algorithm 2:Compute the reduced state space.
Input:
N = (P, T; F, M0, Me)
Output: The reduced state space SSG;
(1)
define SSG = (N, E, M0, Me);
(2)
tagM0;
(3)
addM0 to Υ and N;
(4)
whileΥ ≠ ∅ do
(5)
pick anyM ∈ Υ;
(6)
generate the stubborn setSt(M) of M;
(7)
for eacht∈St(M) do
(8)
computeM[t > M’;
(9)
add (M, t, M′) to E;
(10)
ifM′ is untagged then
(11)
tagM’;
(12)
addM′ to Υ and N;
(13)
end if
(14)
end for
(15)
return SSG;


## 4.3. Checking Correctness

In [21], given a collaboration process, we proposed an effective algorithm for checking its correctness with the concept of transitive closures. Here, we briefly describe its basic idea. That is, the algorithm first generates its state space, i.e., the reachability graph. Then, it calculates the transitive closures corresponding to all nodes in the state space with an algorithm called Floyd–Warshall [27]. Finally, the algorithm determines the correctness based on these generated transitive closures. Concretely, if the transitive closures corresponding to all nodes in the state space cover a final marking, then we derive that the collaboration process is correct, and otherwise, it is incorrect. In the case of incorrectness, two cases exist, i.e., if some nodes (not all) in the state space can reach a final marking, then we define that the collaboration process is partially correct, and otherwise it is fully incorrect. In our context, the algorithm is directly employed to check the correctness of a cloud-based collaboration process. Note that the Floyd–Warshall algorithm is a classic algorithm for computing transitive closures. Its basic idea is that given a directed graph, the algorithm first constructs its adjacency matrix and then calculates transitive closures of nodes based on transitive relations [27]. To save space, the details on the algorithm are not presented in this paper.Example 3.
According to the algorithm described in [21], the fact that OP is partially correct can be derived. Concretely, we first calculate OP’s reduced state space SSG, as depicted in Figure 5.
Then, we calculate the transitive closure corresponding to each node in SSG. Clearly, in Figure5, we can see that closure(M5) does not contain Me (i.e., marking M5 cannot reach the final marking), and hence OP is partially correct.Figure 5
Reduced state space of OP.


## 5. Generating Reliable Paths

We first present the concept of execution paths. Intuitively, an execution path of an open net refers to a trace from its initial marking to its final marking. Given a business process, its execution path can be formally defined as follows.Definition 5.
(Execution Path). LetN= (P, T; F, M0, Me) be a business process; then, its execution path is a sequence of transitions from M0 to Me.
Given a collaborative business process, its execution paths, called collaborative execution paths, are formed by the composition of execution paths in multiple business processes.Definition 6.
(Collaborative Execution Path). LetN = (P, T; F, M0, Me) be a collaborative business process built by composing BPaaS services in the cloud. Then, one of its execution paths can be defined as cep = {ep1, …, epn} where epi (1≤i≤n) is an execution path of Ni.
In collaborative execution paths, not every path can be executed successfully. Based on message places, we can define reliable execution paths from collaborative execution paths.Definition 7.
(Reliable Execution Path). LetN=(P, T; F, M0, Me) be a collaborative business process built by composing BPaaS services in the cloud. Then, given one of its execution paths cep = {ep1, …, epn}, cep is reliable iff for each input message place pi connected to a transition of epi, there exists an output message place po connected to a transition of epo, such that i≠o.
In essence, a reliable execution path can be seen as a collaborative work plan. In practice, it can guide each business process to act properly, ensuring their collaboration can be successfully terminated.
Then, we give an algorithm for generating reliable execution paths for a set of business processes.
Algorithm3 first generates the state space of each business process (L1). Then, the algorithm obtains the execution paths of each state space and their Cartesian product (L2∼L3) is computed. Finally, for each execution path in the cross product, if it satisfies Definition 6, then the algorithm adds it to ∑(L4∼L9).
By analyzing Algorithm3, we can derive that its time complexity is O(|SG1| + … + |SGn| + |∏(EP1,…, EPn)|), where |SGi| indicates the number of the nodes in SGi and |∏(EP1, …, EPn)| indicates the number of the execution paths in ∏(EP1, …, EPn).Algorithm 3:Generate reliable execution paths.
Input: business processes N1, …, Nn
Output: reliable execution paths ∑
(1)
generate the state spaces SG1, …, SGn;
(2)
obtain the sets of execution paths EP1, …, EPn;
(3)
compute∏(EP1, …, EPn);
(4)
for each execution path ep in ∏(EP1, …, EPn) do
(5)
if ep satisfies Definition 6 then
(6)
add ep to∑;
(7)
end if
(8)
end for
(9)
return ∑;Example 4.
Based on Algorithm3, we can obtain all reliable execution paths in OP. We first compute the execution paths EP1 = {t1∧t3, t2∧t3} of N1 depicted in Figure 3(a) and the execution paths EP2 = {t4∧t5∧t8, t6∧t8} of N2 depicted in Figure 3(b). Then, we compute the Cartesian product between EP1 and EP2, i.e., ∏(EP1, EP2) = {(t1∧t3, t4∧t5∧t8), (t1∧t3, t6∧t8), (t2∧t3, t4∧t5∧t8), (t2∧t3, t6∧t8)}. Finally, according to Definition 6, we derive that the reliable execution paths in OP are∑ = {(t1∧t3, t6∧t8), (t2∧t3, t4∧t5∧t8)}. In practice, these reliable execution paths can guide Reta and Supp to operate in a coordinated manner, ensuring the correct execution of OP. For example, if Reta orders product A (i.e., executing t1), then Supp knows that it should choose to receive order A (i.e., executing t6) instead of checking stock, as the collaborative execution path (t1∧t3, t6∧t8) is a reliable execution path, thus avoiding the deadlock described in our motivating example.


## 6. Implementation and Experiments

In this section, we first introduce our prototype tool called cctool. Then, we validate the proposed approach with actual cases.


### 6.1. Implementation

The proposed approach is implemented as a module cctool in the PIPE. Currently, the module cctool is submitted to the GitHub (https://github.com/MoqiYNU/cctool). The running interface of cctool is shown in Figure 6, where the motivating example OP is validated.Figure 6
Screenshot of the tool cctool.As presented in Figure6, at the right side of the interface is the workspace of the PIPE, where each business process can be modeled separately. By double-clicking the module label of cctool, a collaboration process can be constructed through message place fusion and then its reduced state space is generated. Finally, its correctness will be checked based on the reduced state space. In case it is partially correct, all reliable execution paths in it will be written to the hard disk as a text file. With the help of these reliable execution paths, the collaboration process executes according to the specified paths and can be successfully terminated eventually.


### 6.2. Experiments

To confirm the effectiveness and efficiency of the proposed approach, we validate it with actual cases. In our experiments, we utilized a PC with Inter(R) CORE i7 CPU 1.80 GHz and 16 GB memory, running Windows 10.


#### 6.2.1. Cases

Since public collaboration processes cannot be available at present [28], in [21], we build a case set that contains 30 diverse and practical collaboration processes from available resources such as research papers (e.g., [6–8, 10, 11, 29]) and other online materials (e.g., the official website of BPMN). Additionally, based on the 7PMG guideline [30], we also confirm that these cases are reasonable for our experiments, as each collaboration process in the case set contains approximately 50 activities and this is roughly consistent with the tasks involved in the actual process. Currently, these cases have been submitted to the GitHub (https://github.com/MoqiYNU/Cases). In this paper, we directly employ these cases to conduct our experiments. To save space, the details (e.g., places and transitions) of each case are presented in [21].


#### 6.2.2. Effectiveness

In this paper, the effectiveness means that the proposed approach can successfully achieve correctness checking. In our experiments, we also compare our approach with two types of typical correctness checking approaches, i.e., the checking approach based on the full state space (called CaF) [6, 10, 11] and the checking approach based on the view (CaV) [12, 13]. For the sake of simplicity, our approach in experiments is denoted as CaS, i.e., a checking approach based on the stubborn set.Table2 presents the experimental results of correctness checking for all cases, where “+” means correct, “+/−” means partially correct, and “−” means fully incorrect. Following the experimental results, we can see that our approach (i.e., Cas), and both the CaF and CaV approaches can complete the correctness checking for all cases. Meanwhile, we also observe that the checking results of our approach are consistent with the CaF and CaV approaches, thereby confirming the fact that our approach is effective.Table 2
Results of correctness checking.
Case
Checking results
Cas
CaF|CaV
Ca-05∼Ca-09, Ca-14∼Ca-18, Ca-26∼Ca-27
+
+ | +
Ca-01∼Ca-04, Ca-11∼Ca-13, Ca-19∼Ca25, Ca-28∼Ca-30
+/−
+/− | +/−
Ca-10
−
− | −


#### 6.2.3. Efficiency

In this paper, the efficiency means that the proposed approach can more efficiently achieve correctness checking compared with existing typical approaches. In our experiments, we also compare our approach with CaF and CaV.By recording the time that it takes for each approach to detect the case, we obtain the average running overheads of the three approaches, as shown in Figure7.Figure 7
Checking time of three approaches.In Figure7, we observe that for large cases (i.e., the case that contains more states), CaF needs to take more time to complete the correctness checking. For example, for Ca-25, it takes 16488 ms to complete correctness checking. By analyzing CaF, we find that this is mainly caused by the full state space that needs to be exploited during its correctness checking. As far as CaV is concerned, there are some differences. That is, for structured large cases with more internal transitions (i.e., transitions without associated message places), the approach can quickly achieve correctness checking. For example, for Ca-30 which is structured and contains 22 internal transitions (55 transitions in total), it only takes 25 ms for complete checking while 730 ms is taken for CaF. However, for unstructured large cases with less internal transitions, the approach still takes more time to complete correctness checking. For example, for Ca-25, it still takes 14460 ms to complete correctness checking. In practical applications, since most process models are not structured [14], the checking efficiency of the approach may not increase significantly. This is also confirmed in Figure 7, from which we can see that the checking efficiency of CaV, on all cases, is not significantly improved compared to CaF. As far as our approach is concerned, compared with CaF and CaV, its checking efficiency has been greatly improved, as only the reduced state space needs to exploit during correctness checking. For example, for Ca-25, it only takes 5 ms to achieve correctness checking as only 135 nodes and 182 edges are generated in its reduced state space instead of 1939 nodes and 8040 edges in its full state space.Based on the experimental results above, both the effectiveness and efficiency of our approach are confirmed. In practice, the construction of collaborative business processes in the cloud can benefit from the proposed approach.


## 6.1. Implementation

The proposed approach is implemented as a module cctool in the PIPE. Currently, the module cctool is submitted to the GitHub (https://github.com/MoqiYNU/cctool). The running interface of cctool is shown in Figure 6, where the motivating example OP is validated.Figure 6
Screenshot of the tool cctool.As presented in Figure6, at the right side of the interface is the workspace of the PIPE, where each business process can be modeled separately. By double-clicking the module label of cctool, a collaboration process can be constructed through message place fusion and then its reduced state space is generated. Finally, its correctness will be checked based on the reduced state space. In case it is partially correct, all reliable execution paths in it will be written to the hard disk as a text file. With the help of these reliable execution paths, the collaboration process executes according to the specified paths and can be successfully terminated eventually.


## 6.2. Experiments

To confirm the effectiveness and efficiency of the proposed approach, we validate it with actual cases. In our experiments, we utilized a PC with Inter(R) CORE i7 CPU 1.80 GHz and 16 GB memory, running Windows 10.


### 6.2.1. Cases

Since public collaboration processes cannot be available at present [28], in [21], we build a case set that contains 30 diverse and practical collaboration processes from available resources such as research papers (e.g., [6–8, 10, 11, 29]) and other online materials (e.g., the official website of BPMN). Additionally, based on the 7PMG guideline [30], we also confirm that these cases are reasonable for our experiments, as each collaboration process in the case set contains approximately 50 activities and this is roughly consistent with the tasks involved in the actual process. Currently, these cases have been submitted to the GitHub (https://github.com/MoqiYNU/Cases). In this paper, we directly employ these cases to conduct our experiments. To save space, the details (e.g., places and transitions) of each case are presented in [21].


### 6.2.2. Effectiveness

In this paper, the effectiveness means that the proposed approach can successfully achieve correctness checking. In our experiments, we also compare our approach with two types of typical correctness checking approaches, i.e., the checking approach based on the full state space (called CaF) [6, 10, 11] and the checking approach based on the view (CaV) [12, 13]. For the sake of simplicity, our approach in experiments is denoted as CaS, i.e., a checking approach based on the stubborn set.Table2 presents the experimental results of correctness checking for all cases, where “+” means correct, “+/−” means partially correct, and “−” means fully incorrect. Following the experimental results, we can see that our approach (i.e., Cas), and both the CaF and CaV approaches can complete the correctness checking for all cases. Meanwhile, we also observe that the checking results of our approach are consistent with the CaF and CaV approaches, thereby confirming the fact that our approach is effective.Table 2
Results of correctness checking.
Case
Checking results
Cas
CaF|CaV
Ca-05∼Ca-09, Ca-14∼Ca-18, Ca-26∼Ca-27
+
+ | +
Ca-01∼Ca-04, Ca-11∼Ca-13, Ca-19∼Ca25, Ca-28∼Ca-30
+/−
+/− | +/−
Ca-10
−
− | −


### 6.2.3. Efficiency

In this paper, the efficiency means that the proposed approach can more efficiently achieve correctness checking compared with existing typical approaches. In our experiments, we also compare our approach with CaF and CaV.By recording the time that it takes for each approach to detect the case, we obtain the average running overheads of the three approaches, as shown in Figure7.Figure 7
Checking time of three approaches.In Figure7, we observe that for large cases (i.e., the case that contains more states), CaF needs to take more time to complete the correctness checking. For example, for Ca-25, it takes 16488 ms to complete correctness checking. By analyzing CaF, we find that this is mainly caused by the full state space that needs to be exploited during its correctness checking. As far as CaV is concerned, there are some differences. That is, for structured large cases with more internal transitions (i.e., transitions without associated message places), the approach can quickly achieve correctness checking. For example, for Ca-30 which is structured and contains 22 internal transitions (55 transitions in total), it only takes 25 ms for complete checking while 730 ms is taken for CaF. However, for unstructured large cases with less internal transitions, the approach still takes more time to complete correctness checking. For example, for Ca-25, it still takes 14460 ms to complete correctness checking. In practical applications, since most process models are not structured [14], the checking efficiency of the approach may not increase significantly. This is also confirmed in Figure 7, from which we can see that the checking efficiency of CaV, on all cases, is not significantly improved compared to CaF. As far as our approach is concerned, compared with CaF and CaV, its checking efficiency has been greatly improved, as only the reduced state space needs to exploit during correctness checking. For example, for Ca-25, it only takes 5 ms to achieve correctness checking as only 135 nodes and 182 edges are generated in its reduced state space instead of 1939 nodes and 8040 edges in its full state space.Based on the experimental results above, both the effectiveness and efficiency of our approach are confirmed. In practice, the construction of collaborative business processes in the cloud can benefit from the proposed approach.


## 6.2.1. Cases

Since public collaboration processes cannot be available at present [28], in [21], we build a case set that contains 30 diverse and practical collaboration processes from available resources such as research papers (e.g., [6–8, 10, 11, 29]) and other online materials (e.g., the official website of BPMN). Additionally, based on the 7PMG guideline [30], we also confirm that these cases are reasonable for our experiments, as each collaboration process in the case set contains approximately 50 activities and this is roughly consistent with the tasks involved in the actual process. Currently, these cases have been submitted to the GitHub (https://github.com/MoqiYNU/Cases). In this paper, we directly employ these cases to conduct our experiments. To save space, the details (e.g., places and transitions) of each case are presented in [21].


## 6.2.2. Effectiveness

In this paper, the effectiveness means that the proposed approach can successfully achieve correctness checking. In our experiments, we also compare our approach with two types of typical correctness checking approaches, i.e., the checking approach based on the full state space (called CaF) [6, 10, 11] and the checking approach based on the view (CaV) [12, 13]. For the sake of simplicity, our approach in experiments is denoted as CaS, i.e., a checking approach based on the stubborn set.Table2 presents the experimental results of correctness checking for all cases, where “+” means correct, “+/−” means partially correct, and “−” means fully incorrect. Following the experimental results, we can see that our approach (i.e., Cas), and both the CaF and CaV approaches can complete the correctness checking for all cases. Meanwhile, we also observe that the checking results of our approach are consistent with the CaF and CaV approaches, thereby confirming the fact that our approach is effective.Table 2
Results of correctness checking.
Case
Checking results
Cas
CaF|CaV
Ca-05∼Ca-09, Ca-14∼Ca-18, Ca-26∼Ca-27
+
+ | +
Ca-01∼Ca-04, Ca-11∼Ca-13, Ca-19∼Ca25, Ca-28∼Ca-30
+/−
+/− | +/−
Ca-10
−
− | −


## 6.2.3. Efficiency

In this paper, the efficiency means that the proposed approach can more efficiently achieve correctness checking compared with existing typical approaches. In our experiments, we also compare our approach with CaF and CaV.By recording the time that it takes for each approach to detect the case, we obtain the average running overheads of the three approaches, as shown in Figure7.Figure 7
Checking time of three approaches.In Figure7, we observe that for large cases (i.e., the case that contains more states), CaF needs to take more time to complete the correctness checking. For example, for Ca-25, it takes 16488 ms to complete correctness checking. By analyzing CaF, we find that this is mainly caused by the full state space that needs to be exploited during its correctness checking. As far as CaV is concerned, there are some differences. That is, for structured large cases with more internal transitions (i.e., transitions without associated message places), the approach can quickly achieve correctness checking. For example, for Ca-30 which is structured and contains 22 internal transitions (55 transitions in total), it only takes 25 ms for complete checking while 730 ms is taken for CaF. However, for unstructured large cases with less internal transitions, the approach still takes more time to complete correctness checking. For example, for Ca-25, it still takes 14460 ms to complete correctness checking. In practical applications, since most process models are not structured [14], the checking efficiency of the approach may not increase significantly. This is also confirmed in Figure 7, from which we can see that the checking efficiency of CaV, on all cases, is not significantly improved compared to CaF. As far as our approach is concerned, compared with CaF and CaV, its checking efficiency has been greatly improved, as only the reduced state space needs to exploit during correctness checking. For example, for Ca-25, it only takes 5 ms to achieve correctness checking as only 135 nodes and 182 edges are generated in its reduced state space instead of 1939 nodes and 8040 edges in its full state space.Based on the experimental results above, both the effectiveness and efficiency of our approach are confirmed. In practice, the construction of collaborative business processes in the cloud can benefit from the proposed approach.


## 7. Related Work

Both the state space-based and view-based checking approaches are related to our approach.


### 7.1. State Space-Based Checking Approaches

To sum up, state space-based checking approaches can be divided into the following three subtypes: the automata-based checking approach, the Petri net-based checking approach, and the process algebra-based checking approach.


#### 7.1.1. Automata-Based Checking Approaches

In [31], Xu et al. first convert BPEL processes into the guarded automata models based on transformation rules. Then, they translate the generated automata models into Promela processes. Finally, some conversational properties are verified on SPIN. In [32], Zhou et al. proposed a formal technique to verify the interaction among web service-based processes considering requestors’ requirements. In [33], Flavio et al. first provide a direct formalization for BPMN based on Labeled Transition Systems. Then, they verify some LTL-based properties (e.g., the reachability property) using the model checking technique.


#### 7.1.2. Petri Net-Based Checking Approaches

In [6], Aalst first define the correctness criterion in terms of soundness. Then, they build the cross-organizational workflow based on synchronous and asynchronous communications. Lastly, they verify its correctness based on the reachability graph. Zhang et al. [29] proposed a Petri net and Pi calculus-based approach to model and analyze business collaborations. In the approach, they first fuse the two formal methods based on a mapping method, in which Petri nets are used to specify the local flow of the business process while the interaction between them is specified by Pi calculus, and the mapping integrates both to obtain a unified model. Then, they generate the state graph of the unified model, and the soundness can be verified on it. Ge et al. [34] proposed an effective method to verify the correctness of cross-organizational workflows based on the invariant analysis. In this approach, they first model cross-organizational workflows using Interaction-Oriented Petri Nets (IOPN). Then, they decompose the model into a set of sequence diagrams. Lastly, the correctness can be verified on these sequence diagrams. Zeng et al. [10] proposed an approach to model and verify cross-department business processes. In this approach, they first employ the RM_WF_Net (a WF-net [6] extended with message and resource factors) to model cross-department business collaborations. Then, they verify their correctness based on their reachability graph. Kheldoun et al. [35] proposed a verification technique for complex business processes based on high-level Petri nets. In this approach, they first employ Business Process Modeling Notation (BPMN) to describe a collaborative process. Then, they map the generated model to Petri nets based on some proposed rules. Lastly, they use model checking to check its correctness. Du et al. [17] proposed a three-stage approach to analyze the time compatibility via model checking. In this approach, they first model each web service as a fragment described Petri nets. Then, they transform each fragment into a time automata net (TAN). Lastly, by composing these generated TANs, a web service composition is built and its correctness can be analyzed by UPPAAL. To model and verify the emergency response process, Duan et al. [11] proposed a refinement-based approach. They first refine a top-level model into a bottom-level model using some collaboration patterns from different abstraction levels and then verify the refined model at its reachability graph.


#### 7.1.3. Process Algebra-Based Checking Approaches

Wong and Gibbons [36] employ the process algebra CSP (Communicating Sequential Process) to formalize BPMN and then verify some correctness properties using the tool FDR (Failure Divergence Refinement). Mendoza [37] proposed a formal compositional verification approach to specify and verify business processes. In this approach, they employ CSP + T (Communicating Sequential Processes + Time) to model the BPMN model with time and then use model checking to verify its correctness. Based on the idea of model transformation, Zhu et al. [38] first utilize the idea of model transformation to establish a verification framework. Then, they map the composition to CSP processes based on a set of transformation rules. Lastly, the correctness can be validated by the tool FDR.


### 7.2. View-Based Correctness Checking Approaches

To support B2B collaboration, Norta and Eshuis [12] proposed an approach to describe structurally collaborative processes. Their approach first defines private and public layers based on WF-nets. Then, the approach uses some combination projections such as grey box projection to generate external processes from conceptual processes. Lastly, the correctness of business process collaborations can be verified on the composition of external processes. To more effectively verify the correctness of cross-organizational processes, Mo et al. [13] first use private processes to describe the complete process of organizations. Then, they abstract them into public views based on four rules. Lastly, the collaborative business process is built by composing public processes. Based on the approach, the verification efficiency can be improved. To effectively model cross-organizational emergency response processes, Duan et al. [24] first introduce the TRM_WF_net, i.e., a WF-net with messages and resources. Then, based on TRM_WF_nets, they present a three-layer framework to describe the emergency response process. Lastly, a set of rules are given to reduce the TRM_WF_net model. In practice, these rules can improve the evaluation efficiency of temporal performance while considering privacy.


### 7.3. Summary of Existing Work

Following the literature review above, we observe that most of the existing approaches (e.g., [6, 10, 17, 29, 31–38]) verify the correctness using the full state space. Hence, these approaches may suffer from a low efficiency, as the state-space explosion exists. Several approaches (e.g., [12, 13, 24]) check correctness based on the public view. To a certain extent, these approaches can improve the checking efficiency while considering privacy. Yet, they require business processes in the collaboration to be structured, and the assumption may not hold in practice [14]. Thus, the efficiency of their correctness checking may not increase significantly. In comparison, since our approach checks correctness based on stubborn sets and puts no restrictions on the business process, the verification efficiency of our approach can be greatly improved.


## 7.1. State Space-Based Checking Approaches

To sum up, state space-based checking approaches can be divided into the following three subtypes: the automata-based checking approach, the Petri net-based checking approach, and the process algebra-based checking approach.


### 7.1.1. Automata-Based Checking Approaches

In [31], Xu et al. first convert BPEL processes into the guarded automata models based on transformation rules. Then, they translate the generated automata models into Promela processes. Finally, some conversational properties are verified on SPIN. In [32], Zhou et al. proposed a formal technique to verify the interaction among web service-based processes considering requestors’ requirements. In [33], Flavio et al. first provide a direct formalization for BPMN based on Labeled Transition Systems. Then, they verify some LTL-based properties (e.g., the reachability property) using the model checking technique.


### 7.1.2. Petri Net-Based Checking Approaches

In [6], Aalst first define the correctness criterion in terms of soundness. Then, they build the cross-organizational workflow based on synchronous and asynchronous communications. Lastly, they verify its correctness based on the reachability graph. Zhang et al. [29] proposed a Petri net and Pi calculus-based approach to model and analyze business collaborations. In the approach, they first fuse the two formal methods based on a mapping method, in which Petri nets are used to specify the local flow of the business process while the interaction between them is specified by Pi calculus, and the mapping integrates both to obtain a unified model. Then, they generate the state graph of the unified model, and the soundness can be verified on it. Ge et al. [34] proposed an effective method to verify the correctness of cross-organizational workflows based on the invariant analysis. In this approach, they first model cross-organizational workflows using Interaction-Oriented Petri Nets (IOPN). Then, they decompose the model into a set of sequence diagrams. Lastly, the correctness can be verified on these sequence diagrams. Zeng et al. [10] proposed an approach to model and verify cross-department business processes. In this approach, they first employ the RM_WF_Net (a WF-net [6] extended with message and resource factors) to model cross-department business collaborations. Then, they verify their correctness based on their reachability graph. Kheldoun et al. [35] proposed a verification technique for complex business processes based on high-level Petri nets. In this approach, they first employ Business Process Modeling Notation (BPMN) to describe a collaborative process. Then, they map the generated model to Petri nets based on some proposed rules. Lastly, they use model checking to check its correctness. Du et al. [17] proposed a three-stage approach to analyze the time compatibility via model checking. In this approach, they first model each web service as a fragment described Petri nets. Then, they transform each fragment into a time automata net (TAN). Lastly, by composing these generated TANs, a web service composition is built and its correctness can be analyzed by UPPAAL. To model and verify the emergency response process, Duan et al. [11] proposed a refinement-based approach. They first refine a top-level model into a bottom-level model using some collaboration patterns from different abstraction levels and then verify the refined model at its reachability graph.


### 7.1.3. Process Algebra-Based Checking Approaches

Wong and Gibbons [36] employ the process algebra CSP (Communicating Sequential Process) to formalize BPMN and then verify some correctness properties using the tool FDR (Failure Divergence Refinement). Mendoza [37] proposed a formal compositional verification approach to specify and verify business processes. In this approach, they employ CSP + T (Communicating Sequential Processes + Time) to model the BPMN model with time and then use model checking to verify its correctness. Based on the idea of model transformation, Zhu et al. [38] first utilize the idea of model transformation to establish a verification framework. Then, they map the composition to CSP processes based on a set of transformation rules. Lastly, the correctness can be validated by the tool FDR.


## 7.1.1. Automata-Based Checking Approaches

In [31], Xu et al. first convert BPEL processes into the guarded automata models based on transformation rules. Then, they translate the generated automata models into Promela processes. Finally, some conversational properties are verified on SPIN. In [32], Zhou et al. proposed a formal technique to verify the interaction among web service-based processes considering requestors’ requirements. In [33], Flavio et al. first provide a direct formalization for BPMN based on Labeled Transition Systems. Then, they verify some LTL-based properties (e.g., the reachability property) using the model checking technique.


## 7.1.2. Petri Net-Based Checking Approaches

In [6], Aalst first define the correctness criterion in terms of soundness. Then, they build the cross-organizational workflow based on synchronous and asynchronous communications. Lastly, they verify its correctness based on the reachability graph. Zhang et al. [29] proposed a Petri net and Pi calculus-based approach to model and analyze business collaborations. In the approach, they first fuse the two formal methods based on a mapping method, in which Petri nets are used to specify the local flow of the business process while the interaction between them is specified by Pi calculus, and the mapping integrates both to obtain a unified model. Then, they generate the state graph of the unified model, and the soundness can be verified on it. Ge et al. [34] proposed an effective method to verify the correctness of cross-organizational workflows based on the invariant analysis. In this approach, they first model cross-organizational workflows using Interaction-Oriented Petri Nets (IOPN). Then, they decompose the model into a set of sequence diagrams. Lastly, the correctness can be verified on these sequence diagrams. Zeng et al. [10] proposed an approach to model and verify cross-department business processes. In this approach, they first employ the RM_WF_Net (a WF-net [6] extended with message and resource factors) to model cross-department business collaborations. Then, they verify their correctness based on their reachability graph. Kheldoun et al. [35] proposed a verification technique for complex business processes based on high-level Petri nets. In this approach, they first employ Business Process Modeling Notation (BPMN) to describe a collaborative process. Then, they map the generated model to Petri nets based on some proposed rules. Lastly, they use model checking to check its correctness. Du et al. [17] proposed a three-stage approach to analyze the time compatibility via model checking. In this approach, they first model each web service as a fragment described Petri nets. Then, they transform each fragment into a time automata net (TAN). Lastly, by composing these generated TANs, a web service composition is built and its correctness can be analyzed by UPPAAL. To model and verify the emergency response process, Duan et al. [11] proposed a refinement-based approach. They first refine a top-level model into a bottom-level model using some collaboration patterns from different abstraction levels and then verify the refined model at its reachability graph.


## 7.1.3. Process Algebra-Based Checking Approaches

Wong and Gibbons [36] employ the process algebra CSP (Communicating Sequential Process) to formalize BPMN and then verify some correctness properties using the tool FDR (Failure Divergence Refinement). Mendoza [37] proposed a formal compositional verification approach to specify and verify business processes. In this approach, they employ CSP + T (Communicating Sequential Processes + Time) to model the BPMN model with time and then use model checking to verify its correctness. Based on the idea of model transformation, Zhu et al. [38] first utilize the idea of model transformation to establish a verification framework. Then, they map the composition to CSP processes based on a set of transformation rules. Lastly, the correctness can be validated by the tool FDR.


## 7.2. View-Based Correctness Checking Approaches

To support B2B collaboration, Norta and Eshuis [12] proposed an approach to describe structurally collaborative processes. Their approach first defines private and public layers based on WF-nets. Then, the approach uses some combination projections such as grey box projection to generate external processes from conceptual processes. Lastly, the correctness of business process collaborations can be verified on the composition of external processes. To more effectively verify the correctness of cross-organizational processes, Mo et al. [13] first use private processes to describe the complete process of organizations. Then, they abstract them into public views based on four rules. Lastly, the collaborative business process is built by composing public processes. Based on the approach, the verification efficiency can be improved. To effectively model cross-organizational emergency response processes, Duan et al. [24] first introduce the TRM_WF_net, i.e., a WF-net with messages and resources. Then, based on TRM_WF_nets, they present a three-layer framework to describe the emergency response process. Lastly, a set of rules are given to reduce the TRM_WF_net model. In practice, these rules can improve the evaluation efficiency of temporal performance while considering privacy.


## 7.3. Summary of Existing Work

Following the literature review above, we observe that most of the existing approaches (e.g., [6, 10, 17, 29, 31–38]) verify the correctness using the full state space. Hence, these approaches may suffer from a low efficiency, as the state-space explosion exists. Several approaches (e.g., [12, 13, 24]) check correctness based on the public view. To a certain extent, these approaches can improve the checking efficiency while considering privacy. Yet, they require business processes in the collaboration to be structured, and the assumption may not hold in practice [14]. Thus, the efficiency of their correctness checking may not increase significantly. In comparison, since our approach checks correctness based on stubborn sets and puts no restrictions on the business process, the verification efficiency of our approach can be greatly improved.


## 8. Conclusion

Based on BPaaS services, developers gathered in the cloud can compose them to construct collaborative business processes to achieve value-added services. However, the correctness is considered to be a key problem at their design phase. In this paper, based on the stubborn set, we propose an approach to check their correctness. In practice, our approach can greatly improve the development efficiency compared with the existing approaches.In general, the time and resource properties are considered to be two important aspects for collaborative business processes in the cloud [9]. Our further work will develop effective techniques to evaluate the temporal performance and to resolve the resource conflict problem. Additionally, edge computing and the Internet of Things (IOT) are two areas closely related to cloud computing [5, 39–44]. Based on the cloud service, our further work will extend the proposed approach to the two areas.



---

*Source: 2751084-2020-02-11.xml*