Abstract: A Web service process is well-structured, means its branch flows are splited and converged correctly in the logical structure. Well-structure is an import property to guarantee a service process to work normally. To detect the well-structured property of Web service process described by WS-BPEL, a logical Petri net method is proposed. The service process based on WS-BPEL is modeled as a service net form logical petri nets and the well-structured property is mapped into the features of logic expressions in the logical transitions of the service net. The formal definition and decision method of well-structure is proposed and the examples are also provided to show how to detect whether a service net is well-structured or not. From the proposed method in this study, the well-structured property of WS-BPEL can be easily analyzed.
INTRODUCTION
Web service is a mature technology to achieve the network-based software oriented service computing. A lot of Web services with small grain and simple functions were developed and deployed in the Internet. The software developer can invoke them to build new application system or compose them into Web service processes to cater complicated service requests.
To realize service composition effectively, many composition languages and interface specifications are proposed, such as WS-BPEL, WS-CDL and WSCI. WS-BPEL is the mainstream language of service composition in the industry. However, WS-BPEL is not a strict formal composition language and it adopts the XML format codes to describe the service process. The structural defects of the Web service process, such as interactive deadlock, structure redundancy, or non-well structure cannot be discovered from the code of WS-BPEL directly. These structural defects are the fatal errors for the Web service processes and should be detected and eliminated.
A Web service process is well-structured means that its branch processes are splited and converged correctly in the logical structure. The concept of well-structure is frequently used in the research of workflow (Eder et al., 2013; Ha and Suh, 2008; Van der Aalst et al., 2011). Since the Web service process is similar with workflow, many researchers introduced well-structure into the study of Web service to express whether the logical structure is correct and soundness in the service process. However, most of the proposed methods (Chae et al., 2008; Li et al., 2011; Xiong et al., 2010) are with a high complexity in detect the well-structured property.
How to easily analyze the well-structured property of WS-BPEL is focused in this study. A method to analyze whether a service process based on WS-BPEL is well-structured or is proposed which based on logic petri net.
SERVICE NET BASED ON LOGIC PETRI NET
A logic petri net is generated by appending the logic expressions on some of the transitions in petri nets. It had been successfully used to the model and analyze the real-time cooperative systems (Du et al., 2007), E-commerce workflows (Du et al., 2009) and the Web service processes (Hu et al., 2014). Now the definitions of logical petri net and service net are provided.
Definition 1
Logic petri net: LPN = (P, T, F, I, O, M) is a logic petri net if the following hold:
| • | P is a finite set of places | |
| • | T includes three subsets of transitions, i.e., T = TD∪TI∪TO, where, TD denotes a set of traditional transitions, TI denotes a set of logic input transitions and TO denotes a set of logic output transitions | |
| • | F is a flow relation, i.e., a set of directed arcs F⊆(PxT)∪(TxP) | |
| • | I is a mapping function from a logic input transition to a logic input expression, i.e., ∀t∈TI, I(t) = fi | |
| • | O is a mapping function from a logic output transition to a logic output expression, i.e., ∀t∈TO, O(t) = fo | |
| • | M: P→{0, 1} is a marking function, ∀p∈P, M(p) denotes the token count in p | |
| • | The firing rules of the transitions in LPN are defined as follows: | |
• |
∀t∈TD, if ∀p∈•t: M(p) = 1, t is enabled. If t is enabled, it can fire and a new marking M' is generated from current marking M, denoted by M[t>M', where: | |
| • | ∀t∈TI, I(t) = fI, if fI|M = •T•, i.e., all input places of t satisfy the input expression fI at M, t is enabled. If t is enabled, it can fire and generate a new marking M', where: |
| • | ∀t∈TO, O(t) = fO, if ∀p∈•t: M(p) = 1, t is enabled. If t is enabled, it can fire and a new marking M' is generated and ∃S⊆t•, S must satisfy fO|M' = •T•: |
Definition 2
Service net: A service net is a labeled logic petri net and defined as SN = (LPN, I, O, Γ, φ) where:
| • | LPN is the net model of the service net with the following rules: | |
| • | P = Pc∪Pd is a set of places, where Pd is a set of data places interacting with the exterior Web services and Pc is a set of control places which represent the states of the Web service | |
| • | T = Ts∪TI∪TO is a set of transitions, where, Ts represents the operations in a service process; TI and TO denote the set of logic transitions used to control the business flow in the service process | |
| • | F represents the transformational relation between service operations and service states |
| • | i and o are two special control places, where i is the initial place and o is the terminal place of a service process, with •i = •o = Ø and the initial marking M0(I) = 1, M0(p) = 0 for any other place p and |
| • | φ: T↔Γ is a bidiretional mapping, where Γ is a alphabet |
MAPPING RULES BETWEEN SERVICE NET AND WS-BPEL
Many literatures had provided the methods to convert the service process described by WS-BPEL into petri net. There are some open-source engines, which can analyze and run WS-BPEL, such as RiftSaw and ActiveBPEL2.0. With the help of engine tools, the model transformation can be easily achieved. Since focusing on the well-structured property of WS-BPEL, the mapping rules between the main control structures of WS-BPEL and service net are proposed in this section.
The control structure of WS-BPEL includes the labels of <receive>, <reply>, <invoke>, <sequence>, <if>, <pick>, <flow>, <while> and <repeatUntil> (Tan et al., 2009). To simplify the structure of converted model from WS-BPEL to service net, control structures with similar functions are classified into the same category. The mapping rules of control structure between WS-BPEL and service net are presented in Fig. 1. The label <variables> in the WS-BPEL is mapped into a place with a variable name.
| Fig. 1: | Mapping rules between WS-BPEL and service nets |
DEFINITION OF WELL-STRUCTURE
The definition of well-structured in WS-BPEL is based on the concept of well-structured workflow nets. A well-structured service process is that which parallel branches initiated by an AND split should be synchronized by an AND joint. And the alternative branches initiated by OR split should be synchronized by an OR joint.
Let F = {f1, f2,…, fn} be a set of service processes, tO and ti be two logic transitions linking F with parallel or alternative structure.
Definition 1
Logic expression on parallel or alternative structure: O(tO) and i(ti) represent the logic expressions on tO and ti, respectively. To distinctly differentiate the type of logic transitions, the logic expressions O(tO) and I(ti) should be formulated as the following standard forms.
| • | O(tO) = f1.i∧5f2.i¬v…∧5fn.i∨5f1.i∧ f2.i¬v…∧5fn.i ∨…∨5f1.i∧5f2.i¬v…∧fn.i, denoted as O∨ |
| • | CO(to) = f1.i∧ f2.i∧…∧fn.i, denoted as O∧ |
| • | CI(ti) = f1.o∨ f2.o∨…∨fn.o, denoted as I∨ and |
| • | I(ti) = f1.o∧ f2.o∧…∧fn.o, denoted as I∧ |
A symbol ∂ is introduced to represent the type of logical expression of logical transition.
Definition 2
Matching logical transitions: Let F = {f1, f2,…, fn} be a service net, t1 and t2 are the logical transition to link F, ∀fj: π1(fj.i) = {tO}, ∀fj: π2(fj.o) = {ti}, (1≤j≤n). If t1 and t2 are logical input transition and logical output transition or in converse, t1 and t2 are called matching logical transitions.
Definition 3
Synergic expression: Let F = {f1, f2,…, fn} be a service net, tO and ti are the logical transition to link F, ∀fj: π1(fj.i) = {tO}, ∀fj: π2(fj.o) = {ti}, (1≤j≤n). If ∂(to) = O∨vM(ti) = I∨ or ∂(tO) = O∧vM(ti) = I∧, O(tO) and I(tI) are called the synergic expression, they are denoted as O(tO)◊I(ti).
Defintion 4
Well-structured service net: SN is a service net, if ∀to∈SN, ∃ti: O(to)◊I(ti)∀ti∈SN, ∃to: I(ti)◊o(to) then SN is a well-structured service net.
DETECT WELL-STRUCUTE IN WS-BPEL
Decision method: From definition 4, two steps need to be checked in analyze whether a Web service process is well-structured. One is whether its logical transitions are occurred dually, i.e., a logical input transition with a corresponding logical output transition, the other is whether the dual logical transitions are with a matching expression.
| Algorithm 1: | Detect well-structure in the service process based on WS-BPEL |
A concise algorithm to detect whether a WS-BPEL based service process is well-structured is proposed in algorithm 1.
Examples: Due to the algorithm 1, there are two types of service net which are not well-structured. One is with non-matching logical transition, the other is with non-synergic expression.
Figure 2 shows two service nets while Fig. 2a is well-structured and Fig. 2b is not well-structured. The logical transition to2 is with a non-matching logical transition, i.e., there is no logical transition matching to2.
| Fig. 2(a-b): | Service net with non-matching logical transition |
| Fig. 3(a-b): | Service net with non-synergic expression |
| Table 1: | Comparison of the logic petri net method and other methods based on petri nets |
The branch flow f2 and f3 should be converged first by a logical input transition and then synchronized by the logical transition ti1, i.e., the well-structured service process is shown as the service net in Fig. 2a.
Similarly, Fig. 3 shows two service nets while Fig. 3a is well-structured and Fig. 3b is not well-structured. The logical transition to1 and ti1 are with non-synergic expression. The logical expression of logical transition to1 is p1∧p2∧5p3∨5p1∧5p2∧p3, it means that the branch flow f1 and f2 should be executed simultaneously or only the branch flow f3 is executed. The branch flow f1, f2 and f3 are not permitted to be executed simultaneously. However, the logical expression of logical transition ti1 is labeled a logical expression p4∧p5∧p6, all the branch flow f1, f2 and f3 should be executed simultaneously while the logical transition ti1 is triggered. Thus, the expression labeled on the logical transition to1 and ti1 is not a synergic expression and the service net is not well-structured.
The service net shown in the Fig. 3a is well-structured, the logical expression of logical transition to1 is updated as p1∧p2∧p3 and it is the synergic expression of p4∧p5∧p6.
Comparison: The method based on Communicating Reachability Graph (CRG) (Li et al., 2011) and the siphon based method (Xiong et al., 2010) to analyze the well-structured property were provided based on the petri net. The communicating reachability graph is a variant of the coverability tree, thus it cannot avoid the space explosion when the service process with a complicated business flow. The siphon based method was also faced the same problem since the coverability tree need building when the siphon of the petri net was computed. Since the two petri net based methods were with the problem of space explosion they could only be used to detect the well-structured property of simple service processes. An efficient result cannot be achieved when the above method used to analyze the well-structured property of complicated service processes. The comparison of our proposed method and the above methods (Li et al., 2011; Xiong et al., 2010) is shown in Table 1. The logic petri net method is not with the problem of space explosion and it is also with a high efficiency since the coverability tree is not built when analyzing the well-structured property.
CONCLUSION
Well-structure is a vital property of service processes. Since WS-BPEL is not with a formal format, it is difficult to detect the well-structured property in the service process described by WS-BPEL. A logical petri net method to analyze the well-structured property of WS-BPEL is proposed in this study. By mapping the WS-BPEL into a service net modeling by logic petri net, the well-structured property is converted by the restriction of logical expression in the service net. The well-structured property is easily analyzed by detecting whether the logical transitions are with the synergic expressions. The examples are also given to shown the efficiency of the proposed method in this study.
ACKNOWLEDGMENTS
This study is supported by the National Basic Research Program of China under Grant No. 2010CB328101; the National Natural Science Foundation of China under Grant No. 61170078 and 61273180; the Doctoral Program of Higher Education of the Specialized Research Fund of China under Grant No. 20113718110004, the Basic Research Program of Qingdao City of China under Grant No. 13-1-4-116-jch.