Kamel Barkaoui
email: kamel.barkaoui@cnam.fr

Maryam Eslamichalandar

Meryem Kaabachi

A Structural Verification of Web Services Composition Compatibility

Keywords: Web service composition, Compatibility, Structure theory of Petri Nets

A fundamental feature of service oriented computing is that simple services need to be composed for generating complex services. This work focuses on the analysis and verification of behavior models of web services composition. In particular, we have to check that neither deadlock nor livelock occurs in this composition. Usually, the verification of such integration, with or without mediators, is achieved by using techniques based on state space exploration of a given service formal model. In this paper, we present an approach based on structure theory of Petri nets allowing the recognition of necessary and/or sufficient conditions ensuring compatible composition and a better understanding of the incompatibility sources.

Introduction

With the increasing use of the platform independent software architecture such as web-based applications, web services exist in distributed environments. Therefore a web service often depends on other web services which have been implemented by different vendors and their correct usage is governed by constraints specified on their interfaces. Whilst different languages such BPEL4WS [START_REF] Alves | Web Services Business Process Execution Language Version 2.0 (OASIS Standard). WS-BPEL TC OASIS[END_REF] have been proposed for describing and executing workflow specifications for a web service composition invocation, we still have a critical need of methods and tools to solve many problems related to service interaction [START_REF] Cheng | Research on Reachability Verification of Web Service Composition[END_REF][START_REF] Aalst | Service Interaction: Patterns, Formalization, and Analysis[END_REF][START_REF] Lohmann | Analyzing interacting WS-BPEL processes using flexible model generation[END_REF]. In this paper, we deal with the issue of verification of web services composition compatibility by using the structure theory of Petri nets formalism. A WS composition is called compatible if its underlying interaction service is such that each service can terminate properly. Our approach is mainly motivated by the fact that verification techniques particularly structural techniques and tools developed for Petri nets can be fully exploited in the context of web services described by BPEL4WS [START_REF] Dun | Transformation of BPEL Processes to Petri Nets[END_REF], or others. The main goal of this paper is to show how structure theory of Petri nets can provide some guidelines and solutions for ensuring the correctness of web services composition. This paper is organized as follows. Section 2 gives a brief summary of basics of Petri nets and of its related structure theory. Section 3 introduces the open nets as a formal model for web services and their composition. In Section 4, using recent results of structure theory of Petri, we deal with the correctness of the WS composition in particular with behavioral compatibility and provide new way of looking at interaction services permitting us the identification of some interface patterns ensuring compatibility between two or more services. Section 5 concludes this paper.

Basics of Petri nets

In this section, after giving basic definitions and properties of Petri nets, we present some recent structure theory results.

Definitions and notations

A Petri Net (P/T) N = (P, T, F, m 0 ) consists of :

-P a finite set of places and T a finite set of transitions with (P ∪ T) = ∅ and (P ∩ T = ∅), -F ⊆ (P × T) ∪ (T × P) is the flow relation -m 0 is the initial marking where a marking m is a mapping m : P → N.

Each node x ∈ P ∪ T of the net has a pre-set and a post-set defined respectively as follows : ˙x = {y ∈ P ∪ T / (y, x) ∈ F} and x ˙= {y ∈ P ∪ T / (x, y) ∈ F}.

The incidence matrix of the net is the matrix C indexed by P × T and defined by C(p, t) = W(t, p) -W(p, t) with W(u) = 1 if u ∈ F and W(u) = 0 otherwise.

An integer vector f = 0, indexed by P (f ∈ Z P ) is a P-invariant iff it satisfies t f•C = 0. An integer vector g , g = 0, indexed by T (g ∈ N T ) is a T-invariant iff it satisfies C•g = 0. we denote by f = {p ∈ P / f(p) = 0} the support of f ; f + = {p ∈ P / f(p) > 0} and f -= {p ∈ P / f(p)< 0}, if there exists a P-invariant f / f + = P then N is said to be conservative. and by m = {p ∈ P / m(p)> 0} the support of marking m .

A transition t is said to be enabled under m iff ˙t ⊆ m (i.e. there is a token on every place of ˙t). A transition t enabled under a marking m can be fired, leading to a new marking m such that : ∀p ∈ P : m (p) = m(p) + C(p, t). The set of reachable markings from a marking m in N is denoted by R(N, m).

We recall some behavioral properties of a Petri net N.

-A marking m* is a home state if and

only if ∀m ∈ R(N, m), m* ∈ R(N, m ). -N is reversible iff m 0 is a home state. -N is bounded iff ∀p ∈ P : ∃k ∈ N, ∀p ∈ R(N, m 0 ), m(p) ≤ k i.e. R(N, m 0 ) is finite. -N is structurally bounded iff N is bounded for any m 0 . -If N is conservative then N is structurally bounded. -N is quasi-live iff ∀ t ∈ T ,∃ m ∈ R (N, m 0 ) for which t is enabled. -N is deadlock-free (or weakly live) iff ∀ m ∈ R (N, m 0 ), ∃ t ∈ T enabled in m. -N is live iff ∀ t ∈ T , ∀ m ∈ R (N, m 0 ) ∃m ∈ R (N, m) for which t is enabled.
-N is structurally live iff ∃m 0 / (N, m 0 ) is live.

-A bounded and live Petri net is said to be well formed.

Basics of Structure Theory of P/T nets

Structure theory of Petri nets investigates the relationship between the behavior and the structure of the net. The use of structural methods for the analysis of systems present two major advantages with respect to other approaches : the state explosion problem inherent to concurrent systems is avoided , otherwise limited , and this relationship usually leads to a deep understanding of the system. A remarkable sub structure of Petri nets is that of Siphon. Let N be a P/T system. A non empty set S⊆ P is called a siphon if and only if ˙S⊆ S ˙. S is said to be minimal if and only if it contains no other siphon as a proper subset. Due to its structure a siphon which is unmarked will never becomes marked. In this case, transitions of S ˙cannot be live so S need to be controlled. S is said to be controlled if and only if S is marked at any reachable marking i.e. ∀ m ∈ R (N, m 0 ), ∃ p ∈ S / m(p) > 0. CS-property: N is said to be satisfying the controlled-siphon property if and only if all its minimal siphons are controlled. We recall below two well-known basic relations between liveness and the CSproperty [START_REF] Barkaoui | On the equivalence between liveness and deadlock-freeness in Petri nets[END_REF]. The first states that the CS-property is a sufficient deadlock-freeness condition while the second states that the CS-property is a necessary liveness condition.

Proposition 1. Let N be a P/T net. If N satisfies the CS-property then N is deadlockfree (weakly live). Proposition 2. Let N be a P/T net. If N is live then N satisfies the CS-property.

The following proposition recall the two structural (sufficient but not necessary) conditions permitting us to check if a given siphon is controlled or not. Proposition 3. Let S be a siphon of N satisfying one of the two following conditions, then S is controlled [START_REF] Barkaoui | On the equivalence between liveness and deadlock-freeness in Petri nets[END_REF] :

i) ∃ R ⊆ S such that R ˙⊆ ˙R and R ∩ m 0 = ∅ ii)∃ P-invariant f ∈ Z P such that S ⊆ f , f + ⊆ S and , p∈P [f(p). m 0 (p)]>0
K-Systems : P/T nets for which CS-property is not only necessary but also sufficient liveness condition, in other words , systems for which there is equivalence between liveness and CS-property are called K-systems [START_REF] Barkaoui | On the equivalence between liveness and deadlock-freeness in Petri nets[END_REF].

Root-place : Let t ∈ T be a transition of a P/T net N and r ∈ ˙t ; r is called a root place for t if and only if ∀ p ∈ ˙t , r ˙⊆ p˙. Ordered transition : A transition t ∈ T is said to be ordered if and only if ∀ p, q ∈ ˙t , p ˙⊆ q ˙or q ˙⊆ p ˙, an ordered transition has at least one root place. A transition admitting a root place is not necessarily ordered. We denote by:

-Root (t) the set of root places of t.

-T 0 (N) the set of ordered transitions of N.

-T R (N) the set of transitions of N admitting a root (i.e.

T O (N) ⊆ T R (N)). -Root (N) the set of root places of N. -The Root Component of N is the net R C (N) = (P C (N), T C (N), F C (N)
) defined as follows:

-

P C = Root (N), T C = T R (N). -F C is the restriction of F such that: (p,t) ∈ F C iff p ∈ Root(t) and (t, p) ∈ F C iff (t, p) ∈ F.
Two main subclasses of K-systems namely ordered nets and root nets can be recognized structurally and effectively [START_REF] Barkaoui | On the equivalence between liveness and deadlock-freeness in Petri nets[END_REF].

(1) N is called an Ordered net iff T O (N) = T (i.e. all its transitions are ordered).

(2) N is called a Root net iff T R (N) = T , (T O (N) = T ) and its root component R C (N) is bounded and strongly connected.

Note that by definition these two subclasses are disjoint.

Theorem 1. Let N be an Ordered net or a Root net. N is live if and only if it satisfies the CS-property [START_REF] Barkaoui | On the equivalence between liveness and deadlock-freeness in Petri nets[END_REF].

In particular for well known subclasses of ordered nets for which Root (t) = ˙t ∀ t ∈ T, (therefore R c (N) = N) such Extended Free Choice (EFC) nets, the cs-property ( by condition i) is a necessary and sufficient liveness condition . Moreover, if such nets are bounded then liveness property (i.e. here condition (i)) can be decided in polynomial time [START_REF] Barkaoui | A Polynomial Time Graph Algorithm to Decide Liveness of some basic classes of Bounded Petri Nets[END_REF]. Also as control by trap (i) is preserved after increasing marking (contrary to control by invariant (ii)), liveness property is monotonic for K-systems satisfying CS-property by condition (i). Based on these structural theoretical results , we show in the rest of the paper , how compatibility analysis and verification of web services composition can be under taken efficiently .

Modeling and Specification of web Service Composition

For specification and modeling services, we focus on the concepts which are independent of a given implementation language [START_REF] Alves | Web Services Business Process Execution Language Version 2.0 (OASIS Standard). WS-BPEL TC OASIS[END_REF][START_REF] Zhang | WS-Net: A Petri-net based specification model for web services[END_REF] . First of all, a service has a definition describing its behavior and its interface . An instance of a given service corresponds to an execution of the activities of this service .These activities are atomic units of work specified in the service definition. The interface of a service consists of a set of ports. A pair of ports can be connected using a channel, thus enabling the exchange of messages sent or received by services . In this work , we abstract from non-functional properties, data and information semantics. Hence , web service can be viewed as a control structure describing its behavior according to an interface to communicate asynchronously with other services in order to reach a final state (i.e. a state representing a proper termination). As for modeling of business processes and workflows, P/T nets are well appropriate to model such control perspective of web services. A web service is modeled by a P/T net called open net [START_REF] Aalst | Service Interaction: Patterns, Formalization, and Analysis[END_REF] which is an extension of a workflow net [START_REF] Barkaoui | Workflow soundness verification based on structure theory of Petri nets[END_REF] or service net [START_REF] Hamadi | A Petri net-based model for web service composition[END_REF] by adding, to the internal places, two specific disjoint sets of input and output places (called interface places) modeling the service interface. Services can be composed by connecting the interfaces. More precisely, each input place (i.e. with empty pre-set) corresponds to an input port of the interface (used for receiving messages from a distinguished channel) whereas an output place (i.e. empty post-set) corresponds to an output port of the interface (used for sending messages via a distinguished channel). Our definition of open nets is not restrictive . Indeed any P/T net N* with an initial marking defined on more than one initial place , or admitting a set of final markings ( with mutually exclusive supports ) , can be transformed easily to an equivalent open net. Also our open nets are not elementary communicating in the sense that a transition can be connected to more than one interface place.

The basic web services infrastructure provides simple interactions between a client and a web service. However, the implementation of a web services business needs generally the invocation of other web services. Thus it is necessary to combine the functionality of several web services. The process of developing a composite service is called service composition. Composite services are recursively defined as an aggregation of elementary and composite services. The composition of two or more services generates a new service providing both the original behavior of initial services and a new collaborative behavior for carrying out a new composite task [START_REF] Alves | Web Services Business Process Execution Language Version 2.0 (OASIS Standard). WS-BPEL TC OASIS[END_REF]. From a modeling point of view, a composite service can be described as a recursive composition of open nets [START_REF] Lohmann | Analyzing interacting WS-BPEL processes using flexible model generation[END_REF]. Communication between services takes place by exchanging messages via interface places. Thus, composing two open nets is modeled by merging their respective shared constituents which are the equally labeled input and output interface places. Such a fused interface place models a channel and a token on such a place corresponds to a pending message in the respective channel. As it is convenient to require that all communications are bilateral and directed, i. -P = P 1 ∪ P

2 ; T = T 1 ∪ T 2 ; F = F 1 ∪ F 2 ; -I = (I 1 ∪ I 2 ) \ (O 1 ∪ O 2 ) ; O = (O 1 ∪ O 2 ) \ (I 1 ∪ I 2 ) ; -m 0 = m 01 ⊕ m 02 ; m f = m f 1 ⊕ m f 2
Open net composition is commutative and associative i.e. for interface compatible open nets N1, N2 and N3 :

N 1 ⊕ N 2 = N 2 ⊕ N 1 and (N 1 ⊕ N 2 ) ⊕ N 3 = N 1 ⊕ (N 2 ⊕ N 3
). An open net with an empty interface (I = ∅ and O ˙= ∅) is called a closed net. By choreography , we refer to the coordination of messages between services involved in a composite service. Therefore a service choreography can be described as a closed net . The next section is devoted to check the verification of behavioral properties of a closed obtained by composing open nets.

Structural Verification of Composition Compatibility

A composite web service modeled as a closed net is a service that consists of coordination of several conceptually autonomous but interface compatible services. Although it is not easy to specify how this coordination should behave, we focus here on these three behavioral requirements :

-Weak-Compatibility . A closed net N is said to be weak-compatible iff N is deadlock-free. -Compatibility which excludes not only deadlocks but also livelocks. A closed net N is said to be compatible iff m f is home state(final state is always reachable). -Strong-Compatibility. A closed net N is said to be strong compatible iff N is compatible and quasi-live (proper termination and no dead activities).

Our contribution in this paper is to show how using recent results of structure theory of Petri nets (that can be interpreted as restrictions or operating guidelines on service interaction patterns), we can check or ensure structurally these behavioral properties.

Let us precise that a deadlock state m in a closed net N is a reachable state ( m = m f ) under which no transition is enabled. Obviously, compatibility implies weak compatibility.

Let N = N 1 ⊕ N 2 ⊕ . . . N k be a closed net. Let N i be an open net , N * i = (P i , T i , F i , m 0i , m f i
) is called the inner subnet of N i . We denote by N * * i the subnet obtained from N * i by connecting the initial place s i to the terminal place o i by an additional transition t * i . Let N = N 1 ⊕ N 2 ⊕ . . . N k we denote by θ(N) the net obtained by substituting in each N i , N * i by N * * i . First of all, from the two well known propositions (1) and ( 2), we can deduce easily the two following propositions :

Proposition 4. Let N = N 1 ⊕ N 2 ⊕ . . . N k be a closed net. If θ(N) satisfies the cs-property then N is weak compatible. Proposition 5. Let N = N 1 ⊕ N 2 ⊕ . . . N k . If N is strong compatible then θ(N)
satisfies CS property.(we prove that θ(N) is live )

Let us consider the closed net obtained by the two open nets of Fig. 1 described in [START_REF] Aalst | Service Interaction: Patterns, Formalization, and Analysis[END_REF] .As the cs-property , is not satisfied : the siphon S = (food , money, P7 , P3) is empty at m 0 , N cannot be live neither deadlockfree. Consequently N is not weak compatible. Now, Consider the two interface compatible open nets of Fig. 2 , the corresponding closed net N is such that θ(N) satisfies the cs-property therefore N is weak compatible.

However N is not compatible : indeed the final marking m f = p 4 +p 14 cannot be reached from the accessible marking m* = p 4 + p 14 + p 7 . From this two classes of open nets , we define a large subclass of closed nets called Root closed nets presenting realistic interfaces patterns and for which compatibility can be structurally decided. In this subclass we impose a restriction on the connection nature of interface places such that root internal places are preserved after composition i.e. an input interface place can be a root place but it cannot take the place of another internal one. A larger subclass of composite service can be obtained by applying the basic building process of Root closed nets in a recursive way, i.e. modules can be root closed nets or more complex nets defined in this way. Definition 6. A P/T system N = (P, T, F, m 0 ) is called a Root Closed net (or simply an RC net) if and only if P is the disjoint union P 1 , . . . , P n and B , T is the disjoint union T 1 , . . . , T n and the following holds: i) For every i ∈ {1, . . . , n}, let -N is deadlock free -N satisfies CS property -N is live Proof. Root Closed nets are , by construction , a subclass of Synchronized Dead Closed Systems (SDCS) [START_REF] Barkaoui | On the equivalence between liveness and deadlock-freeness in Petri nets[END_REF] which are a K-systems. Therefore this equivalence holds.

N i = < N * * i , I i , O i > be an open net such that : -( I i ∪ O i ) ⊆ B -N * * i = (P i , T i , F i , m 0i , m f i ) where F i ⊆ (P i * T i ) ∪ (T i * P i ) is
Corollary 1. Let N be a Root Closed net. If θ(N ) B satisfies cs-property then N is weak compatible. This means that N is deadlock free but some interface places can be unbounded. We consider now the closed net N obtained by composition of N 1 , N 2 andN 3 of Fig. 4 from [START_REF] Aalst | Service Interaction: Patterns, Formalization, and Analysis[END_REF]. N 1 ,N 2 and N 3 are sound ordered nets, moreover N satisfies cs-property.However as N is not a root closed net ( the input interface place CMoney does not preserve the root place of transition t*) we cannot claim that N is strong compatible. In fact N is compatible but not strong compatible ( t* is not live in N).

Conclusion

This paper presented a structural approach to verifying process interactions for coordinated web services composition. Using results of structure theory of Petri net , we have identified necessary and /or sufficient structural conditions on web services interfaces ensuring the composition compatibility. The main contribution of this paper is to provide a structural technique to check if two or more web services are compatible and a better understanding of the incompatibility sources. A direction for further work is to exploit these results to develop efficient solutions for the substitutability problem (i.e. the assurance that a given service can be replaced by another one as a better partner in a given composition).

Definition 1 .

 1 An open net N = (P, T, F, I, O, m 0 , m f ) consists of : A Petri net N* = (P, T, F, m 0 , m f ) such that : -m 0 = s ( the initial marking of the service) , ˙s = ∅ -m f = o ( the final marking of the service) , o ˙= ∅ with an interface places (I ∪ O ⊆ P ) such that : -∀ p ∈ I ∪ O, m f (p) = m o (p) = 0 -∀ p ∈ I , ˙p = ∅ (input interfaces places) -∀ p ∈ O , p˙= ∅ (output interface places)

  e. every interface place p ∈ (I ∪ O) has only one open net that sends into p and only one open net that receives from p. Thereby, open nets involved in a composition are pairwise interface compatible i.e. only input interface places of the one open net overlap with output interface places of the This interface compatibility is a basic and first requirement for services composition . Definition 2. Let N1 and N2 be two open nets with pairwise disjoint constituents except for the interfaces . If I =( I 1 ∩ I 2 ) = ∅ and (O 1 ∩ O 2 ) = ∅ then N 1 and N 2 are interface compatible. Definition 3. Let N1 and N2 two interface compatible open nets. Their composition N = N 1 ⊕ N 2 is the open net defined as follows:

Fig. 1 .

 1 Fig. 1. A not weak compatible closed net

  an ordered or root open net satisfying CS-property. ii)For every N * * i i ∈ {1, . . . , n}: ∀b ∈ B , b preserves the sets of root places of N * * i (i.e ∀t ∈ T i , Root(t) N i * * ⊆ Root(t) N i iii) There exists a subset B ⊆ B such that the sub net induced by the inner subnets ⊆ N * * i (i ∈ {1, . . . , n}) and B (denoted by θ(N ) B ) is conservative and strongly connected (if B = B , θ(N ) B = θ(N )) Theorem 3. Let N be a Root Closed net. The three following assertions are equivalent :

Corollary 2 .

 2 Let N be a Root Closed net such that B = B. If θ(N ) satisfies cs property, then N is strong compatible. Proof. Since B = B , θ(N ) is live and bounded. This means that N is deadlock free and the final marking is well a home state. Let us consider now the root closed net N = N 1 ⊕ N 2 of Fig.3 where N 1 (on the right) is a sound root open net and N 2 is a sound ordered open net. As θ(N ) satisfies the cs-property we can claim that N is strong compatible.

Fig. 3 .Fig. 4 .

 34 Fig. 3. A strong compatible root closed net