=Paper=
{{Paper
|id=None
|storemode=property
|title=A Structural Verification of Web Services Composition Compatibility
|pdfUrl=https://ceur-ws.org/Vol-601/EOMAS10_paper3.pdf
|volume=Vol-601
}}
==A Structural Verification of Web Services Composition Compatibility==
https://ceur-ws.org/Vol-601/EOMAS10_paper3.pdf
A Structural Verification of Web Services
Composition Compatibility
Kamel Barkaoui , Maryam Eslamichalandar , Meryem Kaabachi
CEDRIC - CNAM Paris, France
kamel.barkaoui@cnam.fr
Abstract. 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 verifica-
tion 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 con-
ditions ensuring compatible composition and a better understanding of
the incompatibility sources.
Key words: Web service composition, Compatibility, Structure theory
of Petri Nets
1 Introduction
With the increasing use of the platform independent software architecture such
as web-based applications, web services exist in distributed environments. There-
fore a web service often depends on other web services which have been imple-
mented 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 ser-
vice 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 ter-
minate 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 correct-
ness 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
J. Barjis, M.M. Narasipuram, G. Rabadi, J. Ralyté, and P. Plebani (Eds.):
CAiSE 2010 Workshop EOMAS’10, Hammamet, Tunisia, pp. 30-41, 2010.
A Structural Verification of Web Services Composition Compatibility 31
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.
2 Basics of Petri nets
In this section, after giving basic definitions and properties of Petri nets, we
present some recent structure theory results.
2.1 Definitions and notations
A Petri Net (P/T) N = (P, T, F, m0 ) consists of :
– P a finite set of places and T a finite set of transitions with (P ∪ T) 6= ∅ and
(P ∩ T = ∅),
– F ⊆ (P × T) ∪ (T × P) is the flow relation
– m0 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 respec-
tively 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 6= 0, indexed by P (f ∈ Z P ) is a P-invariant iff it satisfies
t
f·C = 0.
An integer vector g , g 6= 0, indexed by T (g ∈ N T ) is a T-invariant iff it satisfies
C·g = 0.
we denote by kf k= {p ∈ P / f(p) 6= 0} the support of f ;
kf k+ = {p ∈ P / f(p) > 0} and kf k− = {p ∈ P / f(p)< 0}, if there exists a
P-invariant f /kf k+ = P then N is said to be conservative.
and by kmk = {p ∈ P / m(p)> 0} the support of marking m .
A transition t is said to be enabled under m iff ˙t ⊆ kmk (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 m0 such that : ∀p ∈ 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 ∀m0 ∈ R(N, m), m* ∈ R(N, m0 ).
– N is reversible iff m0 is a home state.
– N is bounded iff ∀p ∈ P : ∃k ∈ N, ∀p ∈ R(N, m0 ), m(p) ≤ k
i.e. R(N, m0 ) is finite.
– N is structurally bounded iff N is bounded for any m0 .
– If N is conservative then N is structurally bounded.
– N is quasi-live iff ∀ t ∈ T ,∃ m ∈ R (N, m0 ) for which t is enabled.
32 K. Barkaoui, M. Eslamichalandar, M. Kaabachi
– N is deadlock-free (or weakly live) iff ∀ m ∈ R (N, m0 ), ∃ t ∈ T enabled in m.
– N is live iff ∀ t ∈ T , ∀ m ∈ R (N, m0 ) ∃m0 ∈ R (N, m) for which t is enabled.
– N is structurally live iff ∃m0 / (N, m0 ) is live.
– A bounded and live Petri net is said to be well formed.
2.2 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 , other-
wise 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, m0 ), ∃ 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 CS-
property [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 neces-
sary) 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] :
i) ∃ R ⊆ S such that R ˙ ⊆ ˙R and R ∩ km0 k = 6 ∅
P
ii)∃ P-invariant
P f ∈ Z such that S ⊆ kf k, kf k+ ⊆ S
and , p∈P [f(p). m0 (p)]>0
K-Systems : P/T nets for which CS-property is not only necessary but also suf-
ficient liveness condition, in other words , systems for which there is equivalence
between liveness and CS-property are called K-systems [2].
A Structural Verification of Web Services Composition Compatibility 33
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.
– 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)) defined
as follows:
– PC = Root (N), TC = TR (N).
– FC is the restriction of F such that:
(p,t) ∈ FC iff p ∈ Root(t) and (t, p) ∈ FC iff (t, p) ∈ F.
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 TO (N) = T (i.e. all its transitions are or-
dered).
(2) N is called a Root net iff TR (N) = T , (TO (N) 6= T ) and its root compo-
nent RC (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 Rc (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 .
3 Modeling and Specification of web Service Composition
For specification and modeling services, we focus on the concepts which are in-
dependent 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
34 K. Barkaoui, M. Eslamichalandar, M. Kaabachi
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 termi-
nation). 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).
Definition 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 final marking of the service) , o ˙ = ∅
with an interface places (I ∪ O ⊆ P ) such that :
– ∀ p ∈ I ∪ O, mf (p) = mo (p) = 0
– ∀ p ∈ I , ˙p = ∅ (input interfaces places)
– ∀ p ∈ O , p˙ = ∅ (output interface places)
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 busi-
ness needs generally the invocation of other web services. Thus it is necessary
to combine the functionality of several web services. The process of develop-
ing 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
A Structural Verification of Web Services Composition Compatibility 35
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.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 other. 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 con-
stituents except for the interfaces . If I =( I1 ∩ I2 ) = ∅ and (O1 ∩ O2 ) = ∅
then N1 and N2 are interface compatible.
Definition 3. Let N1 and N2 two interface compatible open nets. Their compo-
sition N = N1 ⊕ N2 is the open net defined as follows:
– P = P1 ∪ P2 ; T = T1 ∪ T2 ; F = F1 ∪ F2 ;
– I = (I1 ∪ I2 ) \ (O1 ∪ O2 ) ; O = (O1 ∪ O2 ) \ (I1 ∪ I2 ) ;
– m0 = m01 ⊕ m02 ; mf = mf 1 ⊕ mf 2
Open net composition is commutative and associative i.e. for interface compat-
ible 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 in-
volved 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.
4 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 ser-
vices. Although it is not easy to specify how this coordination should behave,
we focus here on these three behavioral requirements :
36 K. Barkaoui, M. Eslamichalandar, M. Kaabachi
– 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 mf is home state(final state is always reach-
able).
– 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 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 , mf i ) 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 t∗i .
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) satisfies the
cs-property then N is weak compatible.
Proposition 5. Let N = N1 ⊕ N2 ⊕ . . . Nk . 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 de-
scribed in [5] .As the cs-property , is not satisfied : the siphon S = (food ,
money, P7 , P3) is empty at m0 , N cannot be live neither deadlockfree.
Consequently N is not weak compatible.
Now, Consider the two interface compatible open nets of Fig.2 , the corre-
sponding 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 mf = p4 +p14 cannot
be reached from the accessible marking m* = p4 + p14 + p7 .
A Structural Verification of Web Services Composition Compatibility 37
Fig. 1. A not weak compatible closed net
Fig. 2. A weak compatible (but not compatible) closed net
Theorem 2. Let N = N1 ⊕ N2 ⊕ . . . Nk be a closed net. If N is strong compatible
then all Ni∗ are sound.
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 ∈ 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.
38 K. Barkaoui, M. Eslamichalandar, M. Kaabachi
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 sub-
nets. We define now two classes of open nets namely Ordered open nets and
Root open nets for which soundness is equivalent to cs-property[6].
Definition 4. Let N be an open net. N is called an Ordered open net if and only
if N** is an ordered net.
Definition 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 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, 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 ∈ {1, . . . , n}, let Ni = < Ni∗∗ , Ii , Oi > be an open net such that :
– ( Ii ∪ Oi ) ⊆ B
– Ni∗∗ = (Pi , Ti , Fi , m0i , mf i ) where Fi ⊆ (Pi ∗ Ti ) ∪ (Ti ∗ Pi ) is an ordered or
root open net satisfying CS-property.
ii)For every Ni∗∗ i ∈ {1, . . . , n}: ∀b ∈ B , b preserves the sets of root places of
Ni∗∗ (i.e ∀t ∈ Ti , Root(t)N i∗∗ ⊆ Root(t)N i
iii)There exists a subset B 0 ⊆ B such that the sub net induced by the inner subnets
⊆ Ni∗∗ (i ∈ {1, . . . , n}) and B 0 (denoted by θ(N )B 0 ) is conservative and strongly
connected (if B 0 = B , θ(N )B 0 = θ(N ))
Theorem 3. Let N be a Root Closed net. The three following assertions are
equivalent :
– 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.
A Structural Verification of Web Services Composition Compatibility 39
Corollary 1. Let N be a Root Closed net. If θ(N )B 0 satisfies cs-property then N
is weak compatible. This means that N is deadlock free but some interface places
can be unbounded.
Corollary 2. Let N be a Root Closed net such that B 0 = B. If θ(N ) satisfies cs
property, then N is strong compatible.
Proof. Since B 0 = 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 = 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 )
satisfies the cs-property we can claim that N is strong compatible.
We consider now the closed net N obtained by composition of N1 , N2 andN3
of Fig.4 from [5]. N1 ,N2 and N3 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).
Fig. 3. A strong compatible root closed net
40 K. Barkaoui, M. Eslamichalandar, M. Kaabachi
Fig. 4. A compatible (but not strong compatible )closed net
5 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 solu-
tions 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).
References
1. Cheng Y., Wang Z.: Research on Reachability Verification of Web Service Compo-
sition. World Congress on Software Engineering. pp. 233237 (2009).
2. Barkaoui K., Couvreur J.M., Klai K.: On the equivalence between liveness and
deadlock-freeness in Petri nets. Lecture Notes in Computer Science. 3536, 90 107
(2005).
A Structural Verification of Web Services Composition Compatibility 41
3. Dun H., Xu H., Wang L.: Transformation of BPEL Processes to Petri Nets. Theoret-
ical Aspects of Software Engineering, 2008. TASE’08. 2nd IFIP/IEEE International
Symposium on. pp. 166173 (2008).
4. Hamadi R., Benatallah B.: A Petri net-based model for web service composition.
Proceedings of the 14th Australasian database conference-Volume 17. p. 200 (2003).
5. Aalst, W.M., Mooij, A.J., Stahl, C., Wolf, K.: Service Interaction: Patterns, For-
malization, and Analysis. Formal Methods for Web Services. p. 88 (2009).
6. Barkaoui, K.; Ben Ayed R.; Sbai, Z.: Workflow soundness verification based on
structure theory of Petri nets. International Journal of Computng and Information
sciences (IJCIS) Vol.5, n1, April 2007.
7. Alves, A., Arkin, A., Askary, S., Barreto, C., Bloch, B., Curbera, F., Ford, M.,
Goland, Y., Gu?zar, A., Kartha, N., Liu, C., Khalaf, R., Koenig, D., Marin, M.,
Mehta, V., Thatte, S., Rijn, D., Yendluri, P., Yiu, A.: Web Services Business Process
Execution Language Version 2.0 (OASIS Standard). WS-BPEL TC OASIS (2007),
http://docs.oasis-open.org/wsbpel/2.0/wsbpel-v2.0.html.
8. Lohmann, N., Massuthe, P., Stahl, C., Weinberg, D.: Analyzing interacting WS-
BPEL processes using flexible model generation. Data and Knowledge Engineering
64(1), 38-54 (2008).
9. J.Zhang,J-Y.Chung,C. K.Chang,and S.Kim.WS-Net: A Petri-net based specification
model for web services. Proc. ICWS,pp. 420-427.IEEE,2004.
10. K.Barkaoui et M.Minoux.A Polynomial Time Graph Algorithm to Decide Liveness
of some basic classes of Bounded Petri Nets. In Application and theory of Petri
Nets.LNCS 616.pp.62-75,Springer Berlin / Heidelberg.1992