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 veri cation of behavior models of web services composition. In particular, we have to check that neither deadlock nor livelock occurs in this composition. Usually, the veri cation 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 su cient conditions ensuring compatible composition and a better understanding of the incompatibility sources.
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 di erent vendors and their correct usage is governed by constraints
speci ed on their interfaces. Whilst di erent languages such BPEL4WS [
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 identi cation of some interface patterns ensuring compatibility between two or more services. Section 5 concludes this paper.
In this section, after giving basic de nitions and properties of Petri nets, we present some recent structure theory results.
A Petri Net (P/T) N = (P, T, F, m0) consists of : { P a nite set of places and T a nite set of transitions with (P [ T) 6= ; and (P \ T = ;), { F (P T) [ (T P) is the ow relation { m0 is the initial marking where a marking m is a mapping m : P ! N.
Each node x 2 P [ T of the net has a pre-set and a post-set de ned respectively as follows : _ x = fy 2 P [ T / (y, x) 2 Fg and x _ = fy 2 P [ T / (x, y) 2 Fg.
The incidence matrix of the net is the matrix C indexed by P T and de ned by C(p, t) = W(t, p) - W(p, t) with W(u) = 1 if u 2 F and W(u) = 0 otherwise.
An integer vector f 6= 0, indexed by P (f 2 ZP ) is a P-invariant i it satis es tf C = 0.
An integer vector g , g 6= 0, indexed by T (g 2 N T ) is a T-invariant i it satis es C g = 0. we denote by kf k= fp 2 P / f(p) 6= 0g the support of f ; kf k+= fp 2 P / f(p) > 0g and kf k = fp 2 P / f(p)< 0g, if there exists a P-invariant f /kf k+ = P then N is said to be conservative. and by kmk = fp 2 P / m(p)> 0g the support of marking m .
A transition t is said to be enabled under m i _t kmk (i.e. there is a token on every place of _t). A transition t enabled under a marking m can be red, leading to a new marking m0 such that : 8p 2 P : m0(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 8m0 2 R(N; m), m* 2 R(N; m0). { N is reversible i m0 is a home state. { N is bounded i 8p 2 P : 9k 2 N; 8p 2 R(N; m0); m(p) k
i.e. R(N; m0) is nite. { N is structurally bounded i N is bounded for any m0. { If N is conservative then N is structurally bounded.
{ N is quasi-live i 8 t 2 T ,9 m 2 R (N, m0) for which t is enabled. { N is deadlock-free (or weakly live) i 8 m 2 R (N, m0), 9 t 2 T enabled in m. { N is live i 8 t 2 T , 8 m 2 R (N, m0) 9m0 2 R (N, m) for which t is enabled. { N is structurally live i 9m0 / (N, m0) 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. 8 m 2 R (N, m0), 9 p 2 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 [
Proposition 1. Let N be a P/T net. If N satis es the CS-property then N is deadlockfree (weakly live).
Proposition 2. Let N be a P/T net. If N is live then N satis es the CS-property.
The following proposition recall the two structural (su cient 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 [
Ordered transition : A transition t 2 T is said to be ordered if and only if 8 p, q 2 _ 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. { T0(N) the set of ordered transitions of N. { TR(N) the set of transitions of N admitting a root (i.e. TO(N) TR(N)). { Root (N) the set of root places of N. { The Root Component of N is the net RC (N) = (PC (N), TC (N), FC (N)) de ned as follows: { PC = Root (N), TC = TR(N). { FC is the restriction of F such that: (p,t) 2 FC i p 2 Root(t) and (t, p) 2 FC i (t, p) 2 F.
Two main subclasses of K-systems namely ordered nets and root nets can be
recognized structurally and e ectively [
(1) N is called an Ordered net i TO(N) = T (i.e. all its transitions are ordered).
(2) N is called a Root net i TR(N) = T , (TO(N) 6= T ) and its root component RC (N) is bounded and strongly connected.
Note that by de nition 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
satis es the CS-property [
In particular for well known subclasses of ordered nets for which
Root (t) = _ t 8 t 2 T, (therefore Rc(N) = N) such Extended Free Choice
(EFC) nets, the cs-property ( by condition i) is a necessary and su cient liveness
condition . Moreover, if such nets are bounded then liveness property (i.e. here
condition (i)) can be decided in polynomial time [
For speci cation and modeling services, we focus on the concepts which are
independent of a given implementation language [
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). De nition 1. An open net N = (P, T, F, I, O, m0 , mf ) consists of : A Petri net N* = (P, T, F, m0 , mf ) such that : { m0 = s ( the initial marking of the service) , _s = ; { mf = o ( the nal marking of the service) , o _ = ; with an interface places (I [ O
{ 8 p 2 I [ O; mf (p) = mo(p) = 0 { 8 p 2 I , _p = ; (input interfaces places) { 8 p 2 O , p_ = ; (output interface places)
Our de nition of open nets is not restrictive . Indeed any P/T net N* with an initial marking de ned on more than one initial place , or admitting a set of nal 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 de ned 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 [
From a modeling point of view, a composite service can be described as a
recursive composition of open nets [
De nition 2. Let N1 and N2 be two open nets with pairwise disjoint constituents except for the interfaces . If I =( I1 \ I2) = ; and (O1 \ O2) = ; then N1 and N2 are interface compatible.
De nition 3. Let N1 and N2 two interface compatible open nets. Their composition N = N1 N2 is the open net de ned as follows: { P = P1 [ P2 ; T = T1 [ T2; F = F1 [ F2; { I = (I1 [ I2) n (O1 [ O2) ; O = (O1 [ O2) n (I1 [ I2) ; { m0 = m01 m02; mf = mf1 mf2 Open net composition is commutative and associative i.e. for interface compatible open nets N1, N2 and N3 : N1 N2 = N2 N1 and (N1 N2) N3 = N1 (N2 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 veri cation 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 i N is deadlock-free. { Compatibility which excludes not only deadlocks but also livelocks. A closed net N is said to be compatible i mf is home state( nal state is always reachable). { Strong-Compatibility. A closed net N is said to be strong compatible i 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 6= mf ) under which no transition is enabled.
Obviously, compatibility implies weak compatibility.
Let N = N1 N2 : : : Nk be a closed net.
Let Ni be an open net , Ni = (Pi; Ti; Fi; m0i; mfi) is called the inner subnet of Ni . We denote by Ni the subnet obtained from Ni by connecting the initial place si to the terminal place oi by an additional transition ti .
Let N = N1 N2 : : : Nk we denote by (N) the net obtained by substituting in each Ni, Ni by Ni .
First of all, from the two well known propositions (1) and (2), we can deduce easily the two following propositions : Proposition 4. Let N = N1 N2 : : : Nk be a closed net. If (N) satis es the cs-property then N is weak compatible.
Proposition 5. Let N = N1 N2 : : : Nk. If N is strong compatible then (N) satis es 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 [
Now, Consider the two interface compatible open nets of Fig.2 , the corresponding closed net N is such that (N) satis es the cs-property therefore N is weak compatible.
However N is not compatible : indeed the nal marking mf = p4 + p14 cannot be reached from the accessible marking m* = p4 + p14 + p7.
Proof. Suppose there exists Ni not sound, i.e. Ni is not live or not bounded. Case (1): Ni is not live i.e. there is transition t 2 Ti not live in Ni . As (input) interface places only limit the behavior of the associated open net Ni , t remains not live in (N), thus N cannot be strong compatible. Case (2): Ni live but not bounded, thus mf cannot be a home state and N is not compatible.
According to previous results, strong compatibility of open nets requires not
only interface compatibility of open nets but also soundness of their inner
subnets. We de ne now two classes of open nets namely Ordered open nets and
Root open nets for which soundness is equivalent to cs-property[
De nition 5. Let N be an open net. N is called a Root open net if and only if N** is a Root net.
From this two classes of open nets , we de ne 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 de ned in this way.
De nition 6. A P/T system N = (P, T, F, m0) is called a Root Closed net (or simply an RC net) if and only if P is the disjoint union P1; : : : ; Pn and B , T is the disjoint union T1; : : : ; Tn and the following holds: i) For every i 2 f1, . . . , ng, let Ni = < Ni ; Ii; Oi > be an open net such that : { ( Ii [ Oi) B { Ni = (Pi; Ti; Fi; m0i; mfi) where Fi (Pi Ti) [ (Ti Pi) is an ordered or root open net satisfying CS-property. ii)For every Ni i 2 f1; : : : ; ng: 8b 2 B , b preserves the sets of root places of
Ni (i.e 8t 2 Ti, Root(t)Ni Root(t)Ni iii)There exists a subset B0 B such that the sub net induced by the inner subnets
Ni (i 2 f1; : : : ; ng) and B0 (denoted by (N )B0 ) is conservative and strongly
connected (if B0 = B , (N )B0 = (N ))
Theorem 3. Let N be a Root Closed net. The three following assertions are
equivalent :
{ N is deadlock free
{ N satis es CS property
{ N is live
Proof. Root Closed nets are , by construction , a subclass of Synchronized Dead
Closed Systems (SDCS) [
Corollary 2. Let N be a Root Closed net such that B0 = B. If (N ) satis es cs property, then N is strong compatible.
Proof. Since B0 = B , (N ) is live and bounded. This means that N is deadlock free and the nal marking is well a home state.
Let us consider now the root closed net N = N1 N2 of Fig.3 where N1(on the right) is a sound root open net and N2 is a sound ordered open net. As (N ) satis es the cs-property we can claim that N is strong compatible.
We consider now the closed net N obtained by composition of N1; N2andN3
of Fig.4 from [
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 identi ed necessary and /or su cient 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 e cient 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).