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 [7] 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 [1,5,8]. 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 [3], 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.
In this section, after giving basic definitions and properties of Petri nets, we present some recent structure theory results.
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
-N is structurally live iff ∃m 0 / (N, m 0 ) is live.
-A bounded and live Petri net is said to be well formed.
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 [2]. 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 [2] :
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 [2].
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.
) defined as follows:
-
Two main subclasses of K-systems namely ordered nets and root nets can be recognized structurally and effectively [2].
(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 [2].
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 [10]. 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 .
For specification and modeling services, we focus on the concepts which are independent of a given implementation language [7,9] . 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 [5] which is an extension of a workflow net [6] or service net [4] 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 [7]. From a modeling point of view, a composite service can be described as a recursive composition of open nets [8]. 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
Open net composition is commutative and associative i.e. for interface compatible open nets N1, N2 and N3 :
). 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.
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.
) 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 :
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 [5] .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) [2] which are a K-systems. Therefore this equivalence holds.
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 [5]. 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).
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).