High Level Petri Net Modelling and Analysis of Flexible Web Services Composition

Abstract

In this paper we propose a model to deal with flexibility in complex Web services composition (WSC). In this context, we use a model based on high level Petri nets called RECATNets, where control and data flows are easily supported. Indeed, RECATNets combine the strengths of recursive Petri nets with the expressive power of abstract data types. Since RECATNets semantics is expressed in terms of the conditional rewriting logic, one can use the Maude LTL Model-Checker to investigate several behavioral properties of Web services composition.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

With the increasing complexity of business requirements, the distributed and flexible characteristics of Web services, the possibility of errors in Web service composition (WSC for short) is greatly increased. As a result, many researchers tried to propose formal methods, Finite State Machine [1], Pi calculus [2] or Petri nets [3, 4] to build the formal description and verification models of WSC. However, one of the weaknesses of these methods is their lack of support for managing flexible WSC which require dynamic adaptation of their structure. We refer to flexible WSC as the ability to create, modify, extend or suppress (sub)processes in a structured way, at the occurrence of exceptions. In addition, such a composite Web services can potentially be very large, complex and cumbersome. In regard to the previous points, if we want to describe, faithfully, real-life WSC, we need an expressive modeling formalism that allows, in one hand, to specify their flexible and distributed features, and in other hand, to check the interaction (control-flow) correctness of these business processes while taking into account their data flow aspect. In this paper, a new model based on a kind of high level algebraic Petri nets combining the expressive power of abstract data types and Recursive Petri nets [5] called Recursive ECATNets (RECATNets for short) [6] is proposed in order to cope with the flexibility problem in complex WSC. The RECATNets model offers practical mechanisms for a direct and intuitive support of dynamic creation and suppression of processes. They are well-suited for handling the most advanced WSC patterns (involving cancellation and multiple instances). The proposed model is expressive enough to capture the semantics of complex service compositions and their respective specificities. Since RECATNets semantics is expressed in terms of the conditional rewriting logic [7], one can use the Maude LTL model-checker [8] to investigate several behavioral properties of Web services composition. The remainder of this paper is organized as follows. Section 2 gives a brief overview of related work. Section 3 presents the basic concepts of RECTANets. Web service modeling and specification using RECATNet are presented in Sect. 4. Section 5 is devoted to the algebra for composing Web services and its RECATNets-based formal semantics. A case study is presented in Sect. 6. Section 7 presents the analysis method and the verification process. Finally, Sect. 8 concludes and gives some further research directions.

2 Related Works

The composition of web services requires the modelling of different combinations of web services involved in this composition [9]. The modelling of web services composition is addressed in several papers. In this section, we briefly overview some approaches that are closely related to our work. In [10], the authors propose in their project e-flow to use workflow management system in order to compose web services. However, this approach lacks a formal model for specifying web services composition. In [11], the authors developed a Petri net based approach that uses several structural properties for identifying inconsistent dependency specification in a workflow. However, the proposed approach is restricted to acyclic workflows. In [3], the authors propose a Petri net-based algebra for composing web services. They provide a direct mapping from each composition operator to Petri nets. Their model is expressive enough; but data types cannot distinguish because they used elementary Petri nets. Contrary to our model, data types can be distinguished because the model used the expressive power of abstract data types. In [4], the authors used colored Petri nets [12] for modelling web services and their composition where data types can be distinguished. However, the author focalise in modeling, only, simple patterns. The author propose in [13] a model for composing web services based high level Petri nets, called G-nets. In this model, the authors propose to compose web services via special places called instantiated switch places. For the analysis, the author need to tranform their G-net models into Predicate/Transition nets (PrT-nets). However, some useful patterns like multiple instance and cancellation of service are not addressed. In [14], the author present a review of forty-three patterns for modeling business process using Colored Petri-Net (CPN). However, we note that the pattern of multiple instantiation of a sub-process is difficult to implement when a particular instance of a sub-process initiates other sub-process instances or involves recursive calls to the one of these ancestors process. This is even more complex when the number of such instances is not known prior to the execution of the process or where such instances require synchronization on many levels. One of the weakness of the previous approach is their lack a support for modeling useful advanced patterns like multiple instance and cancellation of service. In order to address this issue, we present a modular and hierarchical formalism called RECATNet that allows composition via abstract transitions. The usefulness of our proposed model is: (1) offering a practical mechanisms for handling the most advanced flow patterns (dynamic) multiple instance and cancellation of Web service, (2) providing a hierarchical composition of web services, (3) its modular specification and its flexibility by adding/removing service’s instances in a dynamic manner, (4) allowing distributed execution of web services composition and (5) its semantic may be defined in terms of conditional rewriting logic [7] therefore, the model-checker MAUDE [8] can be used to check its correctness.

Fig. 1

Transition types in RECATNets. a Elementary transition. b Abstract transition

3 Recursive ECATNet Review

Recursive ECATNets (abbreviated RECATNets) [6] are a kind of high level algebraic Petri nets combining the expressive power of abstract data types and Recursive Petri nets [5]. Each place in such a net is associated to a sort (i.e. a data type of the underlying algebraic specification associated to this net). The marking of a place is a multiset of algebraic terms (without variables) of the same sort of this place. Moreover, transitions in RECATNet are partitioned into two types (Fig. 1): elementary and abstract transitions. Each abstract transition is associated to a starting marking, denoted like a multi-set of places put inside bracket. A capacity associated to a place p specifies the number of algebraic terms which can be contained in this place for each element of the sort associated to p. As shown in Fig. 1, the places p and $p'$ are respectively associated to the sorts s and $s'$ and to the capacity c and $c'$. An arc from an input place p to a transition t (elementary or abstract) is labelled by two algebraic expressions IC(p, t) (Input Condition) and DT(p, t) (Destroyed Tokens). The expression IC(p, t) specifies the partial condition on the marking of the place p for the enabling of t (see Table 1). The expression DT(p, t) specifies the multiset of terms to be removed from the marking of place p when t is fired. Also, each transition t may be labelled by a Boolean expression TC(t) which specifies an additional enabling condition on the values taken by contextual variables of t (i.e. local variables of the expressions IC and DT labelling all the input arcs of t). When the condition TC(t) is omitted, the default value is the term True. For an elementary transition t, an output arc $(t,p')$ connecting this transition t to a place $p'$ is labelled by the expression $CT(t,p')$ (Created Tokens). However, for an abstract transition t, an output arc $(t,p')$ is labelled by the expression $\langle i \rangle CT(t,p')$ (Indexed Created Tokens). These two algebraic expressions specify the multiset of terms to produce in the output place $p'$ when the transition t is fired. In the graphical representation of RECATNets, we note the capacity of a place regarding an element of its sort only if this number is finite. If $IC(p,t) =_{def} DT(p,t)$ on input arc (p, t) (e.g. $IC(p,t) =a^{+}$ and $DT(p,t) =a)$, the expression DT(p, t) is omitted on this arc. In what follows, we note $Spec=(\Sigma , E)$ an algebraic specification of an abstract data type associated to a RECATNet, where $\Sigma =(S, OP)$ is its multi-sort signature (S is a finite set of sort symbols and OP is a finite set operations, such $OP\cap S = \phi$). E is the set of equations associated to Spec. $X= (X_{s})_{s\in S}$ is a set of disjoint variables associated to Spec where $OP\cap X = \phi$ and $X_{s}$ is the set of variables of sort s. We denote by $T_{\Sigma ,s} (X)$ the set of S-sorted S-terms with variables in the set X.$[T_{\Sigma }(X)]_{\oplus }$ denotes the set of the multisets of the $\Sigma$-terms $T_{\Sigma }(X)$ where the multiset union operator ($_{\oplus }$) is associative, commutative and admits the empty multiset $\phi$ as the identity element.

Table 1 Different forms of Input Condition IC(p, t)

Fig. 2

Example of a RECATNet and two possible firing sequences

Definition 1

A recursive ECATNet is a tuple $RECATNet =\langle Spec; P, T, F; sort, Cap, IC, DT, CT, TC,I,\varUpsilon , ICT, K \rangle$ where:

• $Spec = (\Sigma , E)$ is a many sorted algebra where the sorts domains are finite (with $\Sigma =(S,OP)$), and $X= (X_{s})_{s\in S}$ is a set of S-sorted variables,

• [P, T, F] is a net where (T $\cap$ P = $\phi$) and $T = T_{elt} \cup T_{abs}$ is finite set of transitions partitioned into abstract and elementary ones. $T_{abs}$ and $T_{elt}$ denoted the set of abstract and elementary transitions,

• sort: $P \rightarrow S$, is a mapping called a sort assignment,

• Cap: is a P-vector on capacity places: p$\in$P, Cap(p): $T_{\Sigma } (\phi )\rightarrow \mathbb {N}\cup \{ \infty \}$,

• $IC: P\times T\rightarrow [T_{\Sigma , sort(p)} (X)]_{\oplus }^{*}$ where $* \in \{0, +, - \}$ maps a multiset of terms for every input arc,

• $DT: P\times T \rightarrow [T_{\Sigma , sort(p)} (X)]_{\oplus }$ maps a multiset of terms for every input arc,

• $CT: P\times T \rightarrow [T_{\Sigma , sort(p)} (X)]_{\oplus }$ maps a multiset of terms for every output arc (p, t) where $t \in T_{elt}$ and a starting marking associated to $t \in T_{abs}$ according to place p,

• $TC: T\rightarrow [T_{\Sigma ,bool} (X)]$ maps a boolean expression for each transition,

• $I=I_{cut}\cup I_{pre}$ is a finite set of indices, called termination indices, dedicated to cut steps and preemptions (interruptions) respectively,

• $\varUpsilon$ is a family, indexed by I, of effective representation of semi-linear sets of final markings,

• $ICT: P \times T_{abs} \times I \rightarrow [T_{\Sigma , sort(p)} (X)]_{\oplus }$ maps a multiset of terms for every output arc (p, t, i) where $t \in T_{abs}$ and $i \in I$,

• $K: T_{elt} \rightarrow T_{abs} \times I_{pre}$, maps a set of interrupted abstract trasitions, and their associated termination indexes, for every elementary transition.

Let’s use the net presented in Fig. 2a to highlight RECATNet’s graphical symbols and associated notations. (1) An elementary transition is represented by a filled rectangle; its name is possibly followed by a set of terms $t'\langle i \rangle \in T_{abs} \times I$. Each term specifies an abstract transition $t'$ which is under the control of t, associated with a termination index to be used when aborting $t'$ consequently to a firing of t. For instance $t_{cancel}$ is an elementary transition where its firing preempts threads started by the firing of $t_{1}$ and the associated termination index is 1. (2) An abstract transition t is represented by a double rectangles with the center filled; its name is followed by the starting marking CT(t). For instance, $t_{1}$ is an abstract transition and $CT(t_{1})= \langle p_{5}, Rq \rangle$ means that any thread created by firing of $t_{1}$ starts with one token i.e. one request Rq in place $p_{5}$. (3) Any termination set can be defined concisely based on place marking. For instance, ${\varUpsilon }_0$ specifies the final marking of threads such that the place $p_{6}$ is marked at least by one token. (4) The set I of termination indices is deduced from the indices used to subscript the termination sets and from the indices bound to elementary transitions i.e. interruption. From the example $I= \{0,1\}$. Informally, a RECATNet generates during its execution a dynamical tree of marked threads called an extended marking, which reflects the global state of such net. This latter denotes the fatherhood relation between the generated threads (describing the inter-threads calls). Each of these threads has its own execution context.

Definition 2

(Extended marking) An extended marking of a RECATNet is a labelled rooted tree denoted $Tr=\langle V, M, E, A\rangle$ where:

• V is the set of nodes (i.e. threads),

• M is a Mapping $V\rightarrow [T_{\Sigma }(\phi )]_{\oplus }$ associating an ordinary marking with each node of the tree, such that $\forall v\in V, \forall p\in P, M(v)(p)\le Cap(p)$,

• $E\subseteq V\times V$ is the set of edges,

• A is a mapping $E \rightarrow T_{abs}$ associating an abstract transition with each edge.

Note that contrary to ordinary nets, RECATNet are often disconnected since each connected component may be activated by the firing of abstract transitions.

Running example. Figure 2b highlights a possible firing sequences of the RECATNet represented in Fig. 2a. The graphical representation of any extended marking Tr is a tree where an arc $v_{1}(m_{1}) \rightarrow v_{2}(m_{2})$ labeled by $t_{abs}$ means that $v_{2}$ is a child of $v_{1}$ created by firing abstract transition $t_{abs}$ and $m_{1}$ (resp. $m_{2}$) is the marking of $v_{1}$ (resp. $v_{2}$). Note that the initial extended marking $Tr_{0}$ is reduced to a single node $v_{0}$ whose marking is $\langle p_{1}, Rq_{1}\rangle \otimes \langle p_{0}, ok \rangle$. From the initial extended marking $Tr_{0}$, the abstract transition $t_{1}$ is enabled; its firing leads to the extended marking $Tr_{1}$ which contains a fresh node $v_{1}$ marked by the starting marking $CT(t_{1})$. Then, the firing of the elementary transition $t_{2}$ from node $v_{1}$ of $Tr_{1}$ leads to an extended marking $Tr_{2}$, having the same structure as $Tr_{1}$ but only the marking of node $v_{1}$ is changed. From node $v_{1}$ in $Tr_{2}$, the cut step $\tau _{0}$ is enabled; its firing leads to an extended marking $Tr_{3}$ by removing the node $v_{1}$ and change the marking on its node father i.e. $v_{0}$ by adding $ICT(t_{1},0)= (p_{4}, achieved)$. Also, another way to remove nodes in extended marking using elementary transition with associated preemption. For instance, from node $v_{0}$ in $Tr_{1}$, the elementary transition $t_{cancel}$ with associated preemption $(t_{1}, 1)$ is enabled; its firing leads to an extended marking $Tr_{4}$ by removing the node $v_{1}$ and change the marking on its node father i.e. $v_{0}$ by adding $ICT(t_{1},1)= (p_{3}, cancelled)$. More details about RECATNets such as formal firing and fundamental properties are presented in [6, 15]. This paper shows the usefulness of using the formalism of RECATNets in the field of Web services composition.

4 Modeling Web Services Using RECATNet

We give now a formal definition of a Web service.

Definition 3

(Web Service) A Web service is a tuple [3] $S=\langle NameS, Desc, Loc, URL, CS, RECATNetS \rangle$ where:

• NameS is the name of the service used as its unique identifier,

• Desc is the description of the provided service. It summarizes what functionalities the service offers,

• Loc is the server in which the service is located,

• URL is the invocation of the Web service,

• CS is a set of the component services of the Web service, if $CS=\{NameS\}$ then S is a basic service, otherwiseS is a Composite service,

• $RECATNetS=\langle Spec; P, T, F; sort, Cap, IC, DT, CT, TC,I,\varUpsilon , ICT, K \rangle$ is the RECATNet service modeling the dynamic behavior of the Web service.

We show in the next section how Web services can be incrementally composed.

5 Web Services Composition

The common control structure in Web services composition usually includes simple patterns like: sequential, choice, iteration, parallel and discriminator operators and complex patterns like multiple instance and cancellation service [14]. Suppose $S_{1},S_{2}$ and $S_{3}$ are three different atomic Web services i.e. each service $S_{i}$ perfoms an individual operation that cannot be split into sub-operations. The algebra operator descriptions of these control structure can be seen as: $S= \varepsilon \mid S_{1} \bullet S_{2} \mid S_{1}+ S_{2}\mid \mu (S_{1})\mid S_{1}\parallel S_{2} \mid (S_{1}\mid S_{2})\rhd S_{3}\mid (S_{1})^\star \mid S_{1}!$ where:

• $\varepsilon$ stands for an empty service, i.e., a service performs no operation.

• $S_{1} \bullet S_{2}$ performs the service $S_{1}$ followed by the service $S_{2}$, i.e., $\bullet$ is an operator of sequence.

• $S_{1}+ S_{2}$ can reproduce either the behavior $S_{1}$ or $S_{2}$, i.e., $+$ is an alternative operator.

• $\mu (S_{1})$ represents a composite service where the behavior $S_{1}$ may be executed multiple times, i.e., $\mu$ is an iteration operator.

• $S_{1}\parallel S_{2}$ performs concurrently the two services $S_{1}$ and $S_{2}$ i.e., $\parallel$ is a Parallel operator.

• $(S_{1}\mid S_{2})\rhd S_{3}$ waits for the execution of one service (among the $S_{1}$ and $S_{2}$) before activating the service $S_{3}$ i.e.$\rhd$ is a discriminator operator. Note that $S_{1}$ and $S_{2}$ are executed in parallel and independently,

• $(S_{1})^\star$ repressents a composite service which allows creating multiple instances of a given Web service $S_{1}$. These instances are independent of each other and run concurrently,

• $S_{1}!$ represents a composite service which if the Web service $S_{1}$ has started, it is disabled and, where possible, the currently running instance is halted and removed.

In this section, we give a formal definition, in term of RECATNet, of the composition operators. Let specified, as defined in Definition 1, each atomic Web service by $S_{i}=\langle NameS_{i}, Desc_{i}, Loc_{i}, URL_{i}, CS_{i}, RECATNetS_{i}\rangle$ where $RECATNetS_{i}=\langle Spec_{i}; P_{i}, T_{i}, F_{i}; sort_{i}, Cap_{i}, IC_{i}, DT_{i}, CT_{i}, TC_{i}, I_{i},\varUpsilon _{i}, ICT_{i}, K_{i} \rangle$. Let’s define a function initMarking(WS) that is used to return the start marking i.e. initial state of the invoked Web service WS. The following notations are common to all the composition operators:

• NameS is the name of the new service,

• Desc is the description of the new service,

• Loc is the location of the new service,

• URL is the invocation of the new service.

5.1 Empty Service

The empty service $\varepsilon$ is a service that performs no operation. It is used for technical and theoretical reasons.

Definition 4

The empty service is defined as $\varepsilon = \langle NameS, Desc, Loc, URL, CS, RECATNetS \rangle$ where:

• $NameS = Empty$

• Desc = “EmptyWeb Service”

• $Loc= Null$ stating that there is no server for the service,

• $URL=Null$ stating that there is no URL for the service,

• $CS=\{Empty\}$ and

• $RECATNetS=\langle Spec;\{p\},\phi ,\phi ;\phi ,\phi ,\phi ,\phi ,\phi \rangle$

In Fig. 3a, we show the graphic representation of the empty service $\varepsilon$.

Fig. 3

Empty service (a), sequence service (b) and choice service (c)

5.2 Sequence

The sequence operator allows the construction of a service composed of two services executed one after the other. This is typically the case when a service should wait the execution result of another one before starting its execution.

Definition 5

The sequence operator $S_{1}\bullet S_{2}$ is defined as $S= \langle NameS, Desc, Loc, URL, CS, RECATNetS \rangle$ where:

• $CS=CS_{1}\cup CS_{2}$ and

• $RECATNetS=\langle Spec; P, T, F;...\rangle$ where: $P=\{p_{1}\cup p_{2}\cup p_{3}\}$, $T=\{t_{1}\cup t_{2}\}$, $F= \{(p_{1},t_{1}),(t_{1},p_{2}),(p_{2},t_{2}),(t_{2},p_{3})\}$, $CT=\{(t_{1}, initMarking(S_{1})),(t_{2}, initMarking(S_{2}))\}$.

Graphically, given two services $S_{1}$ and $S_{2}$, the composite service $S_{1}\bullet S_{2}$ is represented by the RECATNet shown in Fig. 3b.

5.3 Choice

Given two services $S_{1}$ and $S_{2}$, the choice (alternative) operator allows modelling the execution of either $S_{1}$ or $S_{1}$, but not both.

Definition 6

The choice operator $S_{1}+S_{2}$ is defined as $S= \langle NameS, Desc, Loc, URL, CS, RECATNetS \rangle$ where:

• $CS==CS_{1}\cup CS_{2}$ and

• $RECATNetS=\langle Spec; P, T, F;...\rangle$ where: $P=\{p_{1}\cup p_{2}\}$, $T=\{t_{1}\cup t_{2}\}$, $F= \{(p_{1},t_{1}),(p_{1},t_{2}),(t_{1},p_{2}),(t_{2},p_{2})\}$, $CT=\{(t_{1}, initMarking(S_{1})),(t_{2}, initMarking(S_{2}))\}$.

Graphically, given two services $S_{1}$ and $S_{2}$, the composite service $S_{1}+S_{2}$ is represented by the RECATNet shown in Fig. 3c.

5.4 Iteration

The iteration operator allows a service S to be performed a certain number of times.

Definition 7

The iteration operator$\mu (S_{1})$ is defined as $S= \langle NameS, Desc, Loc, URL, CS, RECATNetS \rangle$ where:

• $CS=CS_{1}$ and

• $RECATNetS=\langle Spec; P, T, F;... \rangle$ where: $P=\{p_{1}\cup p_{2}\}$, $T=\{t_{1}\cup t_{2}\}$, $F= \{(p_{1},t_{1}),(p_{1},t_{2}),(t_{2},p_{2})\}$, $CT=\{(t_{1}, initMarking(S_{1}))\}$.

Graphically, if we consider the service $S_{1}$, the composite service $\mu (S_{1})$ is represented by the RECATNet shown in Fig. 4a.

5.5 Parallel

Given two services $S_{1}$ and $S_{1}$, the parallel operator builds a composite service performing the two services in parallel and without interaction between them. The accomplishment of the resulting service is achieved when the two services are completed.

Definition 8

The parallel operator $S_{1}\parallel S_{2}$ is defined as $S= \langle NameS, Desc, Loc, URL, CS, RECATNetS \rangle$ where:

• $CS=CS_{1}\cup CS_{2}$ and

• $RECATNetS= \langle Spec; P, T, F;...\rangle$ where: $P=\{p_{1}\cup p_{2}\cup p_{3}\cup p_{4}\}$, $T=\{t_{1}\cup t_{2}\cup t_{3}\}$, $F= \{(p_{1},t_{1}),(t_{1},p_{2}),(t_{1},p_{3}),(p_{2},t_{2}),(p_{3},t_{3}),(t_{3},p_{4}),(t_{3},p_{4})\}$, $CT=\{(t_{2}, initMarking(S_{1})),(t_{3}, initMarking(S_{2}))\}$.

Graphically, if we consider two services $S_{1}$ and $S_{2}$, the composite service $S_{1}\parallel S_{2}$ is represented by the RECATNet shown in Fig. 4b.

Fig. 4

Iteration (a), parallel (b) and discriminator service (c)

5.6 Discriminator

Two or more equivalent services are invoked in parallel to achieve a given task but only one is required to finish before proceeding with the invocation of the next composed services of the composite service. It is presumed that these services are equivalent in terms of functionalities. The results of the first service to finish are used while the results of the remaining invoked services are ignored. At least one service of the invoked set of services must succeed for the composite service to succeed. The main goal of the discriminator operator is to increase reliability and delays of the services through the Web. For the customers, best services are those which respond in optimal time and are constantly available.

Definition 9

The discriminator operator $(S_{1}\mid S_{2})\rhd S_{3}$ is defined as $S= \langle NameS, Desc, Loc, URL, CS, RECATNetS \rangle$ where:

• $CS=CS_{1}\cup CS_{2}\cup CS_{3}$ and

• $RECATNetS=\langle Spec; P, T, F;...\rangle$ where: $P=\{p_{1}\cup p_{2}\cup p_{3}\cup p_{4}\cup p_{5}\cup p_{6}\}$, $T=\{t_{1}\cup t_{2}\cup t_{3}\cup t_{4}\cup t_{5}\}$, $F= \{(p_{1},t_{1}),(t_{1},p_{2}),(t_{1},p_{3}), (t_{1},p_{5}),(t_{2},p_{4}),(t_{3},p_{4}), (p_{4},t_{4}),(p_{4},t_{5},(p_{5},t_{5}),(t_{4},p_{6}),(t_{5},p_{6}))\}$, $CT=\{(t_{2}, initMarking(S_{1})),(t_{3}, initMarking(S_{2})),(t_{5}, initMarking(S_{3}))\}$.

Graphically, if we consider three Web services $S_{1}$, $S_{2}$ and $S_{3}$, the composite service $(S_{1}\mid S_{2})\rhd S_{3}$ is represented by the RECATNet shown in Fig. 4c.

5.7 Multiple Instance Service

Multiple instance operator allows for a given Web service to be instantiated multiple times in a business process. The number of instances is not known during the design or run time. These instances are run concurrently but, whilst they are running, new ones can be created.

Definition 10

Multiple instance service operator $(S_{1})^\star$ is defined as $S= \langle NameS, Desc, Loc, URL, CS, RECATNetS \rangle$ where:

• $CS=CS_{1}$ and

• $RECATNetS=\langle Spec; P, T, F;...\rangle$ where: $P=\{p_{1}\cup p_{2}\cup p_{create}\cup p_{stopcreate}\}$, $T=\{t_{1}\cup t_{addIns}\cup t_{remove}\}$, $F= \{(p_{1},t_{1}), (t_{1},p_{2}),(p_{1},t_{addIns}), (t_{addIns},p_{1}), (p_{create},t_{addIns}),(p_{create},t_{remove}), (t_{remove},p_{stopcreate})\}$, $CT=\{(t_{1}, initMarking(S_{1}))\}$.

Graphically, if we consider a Web service $S_{1}$, the composite service $(S_{1})^\star$ is represented by the RECATNet shown in Fig. 5a.

Fig. 5

Multiple instance service (a) and Cancel service (b)

5.8 Cancel Service

The cancel service operator provides the ability to stop a running instance of a Web service. For instance, the purchaser can cancel his buyonline’s order at any time before it starts or during its running but not after the payment was done.

Definition 11

Cancel service operator $S_{1}!$ is defined as $S= \langle NameS, Desc, Loc, URL, CS, RECATNetS \rangle$ where:

• $CS=CS_{1}$ and

• $RECATNetS=\langle Spec; P, T, F;...\rangle$ where: $P=\{p_{1}\cup p_{2}\cup p_{3}\cup p_{startCancel}\cup p_{endCancel}\}$, $T=\{t_{1}\cup t_{cancel}\}$, $F= \{(p_{1},t_{1}),(t_{1},p_{2},\langle 0 \rangle ),(t_{1},p_{3},\langle 1 \rangle ), (p_{startCancel},t_{cancel}),(t_{cancel},p_{endCancel})\}$, $CT=\{(t_{1}, initMarking(S_{1}))\}$, $K(t_{cancel}) =(t_{1}, 1)$.

Graphically, if we consider a Web service $S_{1}$, the composite service $S_{1}!$ is represented by the RECATNet shown in Fig. 5b.

6 A Case Study

Figure 6 shows an illustrative example of modelling a simplified BuyOnline service adapted from [16]. BuyOnline web service provides online book buying service which is composed of four atomic services: LocateBook, SigIn, CreateAcct and Payement. The composite web service may receive a list of request, sent by users, through the Place StartBO. Each request is represented by a token $(ID, BN,SII,CAI,CCI)$ denotes repsectivelly Identifier, BookName, SignInInfo, CreateAcctInfo, $CreditCardInfo$. At the beginning, BuyOnline service starts by searching a book in web site according to the book name using service LocateBook. This operation is performed by firing the abstract transition LocateBook which, if this book can be found, returns its ISBN number. Then, the user can by this book but a valid register is required. If the user has a legal account, then finish loging using service SignIn; otherwise the user needs to create a new account using the service CreateAcct. In the last one, informations about the created account must be returned i.e. $CAO\ne \phi$. Finally, the service payment can finish the payment for the book according to ISBN number and credit card information CCI provided by user. Two cases are distinguished, if the credit card information are valid, the service payment will perform the payment by success; otherwise the service payment terminates by error i.e. echecP, and an error meaasge $CCI-not-valid$ is sent to user. Note that the user can cancel his/her online book buying service by firing the elementary transition CancelBO. Note that for each request sent by user, an instance of BuyOnline service is created. These instances are independent and may be executed in a distributed manner. In order to support dynamic creation instances of BuyOnline service, we need to update the model according to the pattern of Multiple instance operator shown in Fig. 5a. Here, and in order to perform analysis, we assume that our model is finite i.e. starts by a finite set of requests.

Fig. 6

BuyOnline book service

7 Verification of Web Services Composition

Our approach of verification can be described in Fig. 7. First, atomic services must be described in their associated RECATNets. Then, based on composition rules defined previously, generates the composite web services in terms of RECATNet. This operation may be insured by our java’s tool RECATNet-WSC that is partially implemented. After that, from the obtained RECATNet, we generate in an automated manner its semantics in terms of rewriting logic [7] using the model-to-text (M2T) transformation tool Acceleo.¹ The rewriting logic files are used as an input of the model-checker Maude [8] to investigate several behavioral properties of Web services composition.

Fig. 7

Our approach

Fig. 8

RECATNets meta-model

7.1 RECATNets Meta-Modeling

In order to use M2T transformation using tool Acceleo, we need to define the meta-model of RECATNet. As shown in Fig. 8, we propose a general meta-model of our formalism using the UML class diagram model. Our proposed meta-model is composed mainly of the following classes.

• RECATNet: it builds the final model from a set of Place, Arc, Transition and CutStep.

• Place: it represents the RECATNet places. It has three attributes :name, marking and capacity.

• Transition: it represents the RECATNet transitions. It has three attributes: name, TC and K. One classe inherits from the super-class Transition: AbsTransition for abstract transition. This class contains one attribute startMarking.

• Arc: it represents the RECATNet arcs. It contains one attribute inscription. This class is a super-class of two classes. The first one is InputArc for arcs going from places to transitions. It contains two attributes IC for Input Condition and DT for Destroyed Token. The second is OutputArc for arcs going from transitions to places. It contains only the attribute CT for Created Token. In addition, the last class is a super-class of IndexedOutputArc for arcs going from abstract transition to places. It contains one attribute index to identify the set of indices of termination.

• CutStep: it represents the RECATNet cut steps. It contains two attributes index to identify the index of termination and condition to identify the condition for firing the cut step.

7.2 RECATNet Semantics in Terms of Rewriting Logic

RECATNet’s semantics may be defined, easily, in terms of rewriting logic, therefore someone can use the LTL model-checker of MAUDE to investigate several behavioral properties of Web services compositions. A set of rewriting rules has been introduced in [6, 15] in order to express the semantics of RECATNet in terms of rewriting rules. In order to automate this approach, we have developed a model-to-text (M2T) transformation tool based Acceleo generator code. The transformation’s rules have been inspired from rewriting rules proposed in [6]. For instance, if we consider the RECATNet of the atomic service Payment in Fig. 6, the generated Maude specification using M2T transformation is shown in Fig. 9. In fact, three rewriting rules are generated associated to the three elementary transitions in the RECATNet of the atomic service Payment in Fig. 6. For instance, the rewriting rule in line 4 rl[Payment-running] describes the firing of the elementary transition Payment-running. So, this rewrite rule requires that the left-hand side is a marking where the place Payment-Ready is marked and yields to a marking i.e. the right-hand side, where the place EndP is marked.

Fig. 9

Generated Maude specification

7.3 Implementation Using the Maude Tool

An important property will be checked in Web service composition called soundness which concerns the correctness of internal control-flow of a composite Web service. The soundness of a Web services component is based on two criteria:

• Proper termination: This property called also compatibility of component Web services [17]. Proper termination means that starting from an initial extended marking, every possible execution path properly terminates (eventually) i.e. reaches a final extended marking. This property is expressed in LTL by the following formula: F finalState where the proposition finalState is valid in extended marking Tr if this latter is reduced to its root node with only terms in place ReqAchieved. The temporal operator F is denoted by $\langle \rangle$ in MAUDE notation. This formula has been proven to be true by MAUDE LTL-model checker in Fig. 10.

• No dead service: This property means that every atomic Web service must be invoked, at least, once. This requirement imposes that the Web services component should not contain Web services that can never be executed. In order to check this property, we define the proposition isInvoked(ws) which is valid in an extended marking Tr, if the specified Web service ws is invoked i.e. is running. Thus, to check that there is no dead service, we express the negation of this formula as the following LTL formula $\bigvee \limits _{ws \in WS}G \lnot isInvoked(ws)$ where WS is the set of atomic web services used during composition. Here, $WS=\{LocateBook, SigIn, CreateAcct, Payement\}$. If this formula is not valid, it means that the property No dead service is verified. The temporal operators G (Generally) and $\lnot$ (not) are denoted, respectively, by [] and $\sim$ in MAUDE notation. In our case study, as we have a choice between the service SigIn and CreateAcct, this formula is expressed in LTL as following: $[]\sim isInvoked(LocateBook) \backslash / []\sim (isInvoked(SignIn) \backslash / isInvoked(CreateAcct)) \backslash /$ $[]\sim isInvoked(Payment)$. This formula has been proven to be not valid by MAUDE LTL-model checker in Fig. 11. The model-checker returns the expected counterexample.

Fig. 10

Checking Proper termination property under Maude

Fig. 11

Checking No dead service property under Maude

As the two properties Proper termination and No dead service are proved to be valid, therefore, the generated composite Web service is sound.

8 Conclusion

In this paper, an effecient and flexible approach for Web services composition has been proposed. This approach takes fully advantage of modular, distributed execution aspects of RECATNets formalism. The formal semantic of the composition operators is expressed easily in terms of RECATNets by providing a direct transformation of each operator in terms of RECATNets. In fact, the model of RECATNets is particularly adequate for handling the most advanced flow patterns such as dynamic creation of processes and specifying exceptional behaviors in WSC at design time. Also, our method allows the verification of some properties using the LTL model-checker of the Maude system. In the future, we plan to complete this work by developing a tool capable of making automatic the mapping WSDL-descriptions into RECATNets.