Composing services makes sense only if they are compatible, i.e. composition does not lead to problems such as livelocks or deadlocks. In general, compatibility can be checked using state space explorations on any kind of formal models of services. Petri nets, one of the formal models in use, o er a rich theory for reasoning without exploring a state space. Among the techniques is the so-called state equation which forms a linear algebraic necessary condition for reachability of states. In this article, we show how the state equation can be applied for a necessary condition for compatibility. This way, the number of expensive state space based compatibility checks can be drastically reduced. The condition can be applied even if compatibility is achieved through the construction of a behavioral adapter (mediator).
Service behaviors are compatible if their composition forms a closed system (every outbound channel of a service is merged to an inbound channel of some other service) and all involved services can execute their control ow completely. Compatibility can be augmented with the requirement that all or certain activities in the participating services can occur or other semantical constraints.
In this paper we show an approach for alleviating the costs of the compatibility
check for services modeled with Petri nets using their state equation. The state
equation provides a necessary condition for reachability of the nal states of the
services in the composition under several constraints such as the enabling of
some events or choice covering. This result can be applied directly to adapter
synthesis [
In the remainder of this article, we rst introduce notations for Petri net models for services and the state equation. Section 3 gives the necessary conditions for compatibility and derives other necessary conditions for compatibility under some additional constraints. Section 4 presents a necessary condition to adaptability. Section 5 concludes the paper. b c d e a b c d e t1 N t3
t5 p0 t4 p t2 a b c d e
N 0
N 00
Let = fa; b; c; : : : g be a nite message type set, ? = f?a; ?b; ?c : : : g a nite set of receive events, and ! = f!a; !b; !c : : : g a nite set of send events. We also write ? =! and ? =? .
We consider services modeled as open nets. An open net [
De nition 1. An open net is a tuple N = (P [ Pi [ Po; T; F; m0; Mf ; l), where { P; Pi; Po are the pairwise disjunct nite sets of internal/input/output places; { T is the nite set of transitions so that (P [ Pi [ Po) \ T = ; which are labeled by the partial function l : T !? [! ; { F : ((P [ Pi [ Po) T ) [ (T (P [ Pi [ Po)) ! N represents the ow function so that F (p; t) = F (t0; p0) = 0, for all (p; t) 2 Po T and (t0; p0) 2 T Pi; { m0; Mf represent the initial state (marking) and the nite set of nal states, respectively. We consider states as vectors over the set of places.
An open net is called closed when its interface is empty, i.e. Pi [ Po = ;. The
projection of an open net on its transitions and internal places is a closed net
denoted by N . Open nets over ? [! are composed [
A transition t 2 T is enabled in a marking m if F (p; t) m(p) for all places p. An enabled transition may re yielding a (reachable) marking m0 so that m0(p) = m(p) F (p; t) + F (t; p) for all places p, which is denoted by m !t m0. The reachability relation can be extended to sequences of transitions 2 T , which is denoted by !. Two open nets are called compatible if their composition weakly terminates, i.e. from each state reachable from the initial state of the composition, it is possible to reach a nal state of the composition. A weaker notion of compatibility is deadlock-freedom, i.e. at each non- nal reachable state (in the composition) it is possible to re a transition.
Reachability analysis for Petri nets can be achieved by using typical structural
methods, e.g. methods which nd algebraic approximations of the state space
with nite representation. The state equation [
The incidence matrix CN 2 N(P [Pi[Po) T is de ned by CN (p; t) = F (t; p) F (p; t) for all (p; t) 2 (P [ Pi [ Po) T . Let 2 T be transition sequence. The Parikh vector of is a vector 2 NT whiPch assigns to each transition t 2 T its number of occurrences in . Let (a) = t2T :l(t)=a (a) denote the number of occurrences of all transitions labeled by a 2! [? . Given a ring sequence m ! m0 of N , the ring equations for all places of N and all transitions in can be written in matrix form m0 = m + C , which is called the state equation. Proposition 1 (Necessary condition for reachability). For every nite ring sequence m ! m0 of N , the state equation m0 = m + CN holds. 3
We state now a necessary condition for compatibility as weak termination of two composed open nets. The rst conditions represent the state equations of the open nets without their interface places. The last condition means that in all solutions to the equation the number of occurrences of receiving events should be equal to the number of occurrences for sending events for each such event. Corollary 1. If N and N 0 are compatible (w.r.t. weak termination), then the system LP(CNb; CNb0 ; m0; m00; mf ; m0f ; x; x0) imsffea=simble0.+ CNb x x 2 NT LP(CNb; CNb0 ; m0; m00; mf ; m0f ; x; x0) : m0f = m00 + CNb0 x0 x0 2 NT 0 x(a) = x0(a)
If the equation does not have any solution then the nal marking will not be reachable in the composition from the initial marking.
Remark 1. In case services have more nal states, separate systems of equations are solved for each possible combination. For the nets N and N 0 in Figure 1 LP(C b; CNb0 ; m0; m00; mf ; m0f ; x; x0) does not have any solution. Therefore, N
N and N 0 are incompatible. Note that the converse does not hold, e.g. the nets N and N 00 in Figure 1, x00(?a) = x(!a) = 2, x(?b) = x00(!b) = 1, x(!d) = x00(?d) = 1, x(!c) = x00(?c) = 0 and x(!e) = x00(?e) = 0 is a solution for LP(C b; CNb00 ; m0; m000; mf ; m0f0; x; x00), however N and N 00 are incompatible as we
N shall see in the remainder.
If N N 0 is deadlock-free then at each non- nal reachable marking in the composition there is an enabled transition, i.e. adding the disabling condition for each transition leads to an infeasible system. Several variations for compatibility notions have been introduced [6{8] which de ne behavioral constraints which can imposed on interacting services. Among these settings we mention transition cover and place cover.
Message and event cover De nition 2. We call an action a in ? [! covered locally/globally i a transition/all transitions labeled by a in the composition eventually becomes enabled in the composition. A message place (channel) p 2 Pi [ Po is called covered if m(p) > 0, for some reachable marking m in the composition.
Let N and N 0 be two open nets and a 2? [! . We state now conditions which should be added to LP(CNb; CNb0 ; m0; m00; mf ; m0f ; x; x0) to enforce local, global event cover, place and message cover. local event cover x(t) > 0 (t 2 T : l(t) = a) or x0(t0) > 0 (t0 [ T 0 : l(t) = a); place cover for p 2 P there exists a t 2 T so that F (p; t) > 0 and x(t) > 0 (similarly if p 2 P 0); global event cover x(t) > 0, for all t 2 T : l(t) = a or x0(a) > 0; message channel cover x(a) > 0 and x0(a) > 0.
In N N 00 in Figure 1, a is locally covered but not globally covered (transition
t1). The message channel e is covered neither in N N 0 nor in N N 00.
Free-choice sending cover Here, we want to strengthen the previously stated
condition by taking into account that compatibility does not refer to a single
execution (as the state equation would suggest). If an execution passes an
internal decision of one service then its partner needs to be able to react to all
possible outcomes for this decision. With the following consideration, we want to
incorporate this observation into our condition at least for so-called free-choice
decisions [
Let x 2 P [ T . The con ict cluster (x) of x is the smallest set satisfying (1) : x 2 (x), (2) : 8q 2 T : q \ (x) 6= ; =) q 2 (x) and (3) : 8q 2 P : q \ (x) 6= ; =) q 2 (x). We write when x is clear from the context. A con ict cluster (x) so that j (x)j > 2 is called a sending free-choice con ict cluster (SC) i for all t1; t2 2 \ T , t1 \ t2 6= ; implies t1 = t2 and l(t) 2! for all t 2 T \ . In Figure 1 fp; t1; t2g represents such a SC in N . Note that a SC in N is also a SC in N .
A SC in the composition of two nets N and N 0 is called covered if each transition of the SC is in some ring sequence from the initial marking to the nal marking of the composition. For compatible partners, every reachable SC in a service should be resolved by the partner.
Corollary 3. Let be a SC with \ T = ft1; t2g in N . If N and N 0 are compatible and is covered in N N 0, then CLP(CNb; CNb0 ; ) is feasible.
LP(C b; CNb0 ; m0; m00; mf ; m0f ; x; x0)
N LP(C b; CNb0 ; m0; m00; mf ; m0f ; x; x0)
N CLP(CNb; CNb0 ; ) : x(t1) > 0 ^ x0(t2) > 0 f 0 SC in N 0j 0 \ T 0 = ft01; t02g ^ x(t01) > 0 ^ x0(t02) > 0^
^l0(t01) = l(t1) ^ l0(t02) = l(t2)g
The last condition checks for the existence of a con ict cluster 0 receiving the messages sent by . The open nets N and N 00 in Figure 1 are incompatible as CLP(C b; CNb0 ; ) has no solutions (the choice between the transitions labeled
N by !a and !d in N 00 is not covered) even if LP(C b; CNb00 ; m0; m000; mf ; m0f0; x; x00) N has solutions.
Remark 2 (deadlock-freedom under constraints cover). We can relax the deadlockfreedom condition in Corollary 2 to express a necessary condition for local event (transition) cover and SC cover:
W t cover SC cover pW:FN N (p;t)>0(m + m0 + m00)(p) p:FN N (p;t)>0(m + m0 + m00)(p)
FN N0 (p; t), where t 2 T [ T 0;
FN N0 (p; t) for all t 2 .
Remark 3 (behavioral SC). The transition t4 of N in Figure 1 is dead and removing it from N does not in uence compatibility of N with any other partner. Hence we can consider \behavioral" SC's (e.g. fp0; t3; t5g) to be checked for cover. 4
The open nets N1 and N2 in Figure 2 do not satisfy the necessary condition in
Corollary 1, hence they are incompatible. Adapters are used to solve
incompatibilities between interacting services. We consider here the approach in [
A direct consequence of Corollary 1 is that compatible partners have a solution to their own state equation. We state this condition for the adapter setting. Corollary 4. If N1 and N2 are adaptable by the set of transformation rules R, then the state equation for N1 \AE N2 with initial marking m10 + m20 and nal marking mf1 + mf2 holds.
The state equation for N1 \AE N2, where AE is the partial adapter for the rules fr1; r3; r4g, does not yield any solution, thus N1 and N2 are not adaptable by fr1; r3; r4g.
In addition, we can formulate a necessary condition for transformation rule cover. Let r : ! 0. We add to the state equation of N1 \A N2 the constraint x(tr) > 0, where tr is the transition corresponding to the application of the rule. Thus, we can eliminate rules which will never be red in conjunction with a proper terminating execution. In Figure 2, r3 and r4 are redundant rules. 5
In this paper we stated some necessary conditions for service compatibility using
the state equation for Petri nets. The advantage of using this approach to state
space methods (e.g. [9{11]) is its lower computational complexity [
The approach presented in this paper allows for (in)compatibility to be
analyzed in a compositional way (incorrectness of a component can be used to
derive the incorrectness of the composition). This is complementary to structural
methods used in soundness analysis [