In this work we consider modeling of services with work ow modules, which are a subclass of Petri nets. The service compatibility problem is to answer the question, whether two Web services t together, i.e. whether the composed system is sound. We study complementarity of service produced/consumed resources, that is a necessary condition for the service compatibility. Resources, which are produced/consumed by a Web service, are described as a multiset language. We de ne an algebra of multiset languages and present an algorithm for checking the conformance of resources for two given structured work ow modules.
Service-Oriented Computing is an emerging computing paradigm that supports the modular design of (software) systems. Complex systems are designed by composing less complex systems, called services.
A service consists of a control structure describing its behavior and of an interface to communicate asynchronously with other services. An interface is a set of (input and output) channels. In order that two services can interact with each other, an input channel of the one service has to be connected with an output channel of the other service.
The problem of checking services compatibility draws attention of many
researchers [
Checking semantical correctness, e.g. deadlock freedom, for composition of two services is a hard problem. Even when a property is decidable, its complexity makes it almost intractable. So, nding relatively easy to check necessary conditions for correctness of services composition may help to nd some bugs for low costs and avoid further veri cation.
In this paper we study services resource conformance, notably whether two services have complementary runs, such that all outputs of one service are consumed by and enough for another service and vice versa.
Services are modeled with work ow modules, also called open work ow nets
| WF-nets (see e.g. [
Since we study services compatibility we suppose control work ow nets to be sound WF-nets. The soundness property guarantees proper termination of autonomous work ow processes (not taking modules interactions into account, so that resources can be generated or consumed during a process execution without any restrictions). Moreover, we restrict ourselves to structured WFmoduls | an important subclass of work ow modules with control WF-nets sound by construction.
The paper is organized as follows. Section 2 contains some basic de nitions and notions, including formal de nitions of work ow nets, work ow modules and composition of work ow modules. In Section 3 a motivating example of two work ow modules, modeling a part of credit allowence system, is given. In Section 4 we de ne and study a language of quasi regular expressions for describing a work ow module resource interfaces. In Section 5 we present an algorithm for checking resource compatibility of two structured work ow modules. Section 6 contains some conclusions. 2
Let S be a nite set. A multiset m over a set S is a mapping m : S ! Nat, where Nat is the set of natural numbers (including zero), i. e. a multiset may contain several copies of the same element.
For two multisets m; m0 we write m m0 i 8s 2 S : m(s) m0(s) (the inclusion relation). The sum and the union of two multisets m and m0 are de ned as usual: 8s 2 S : m + m0(s) = m(s) + m0(s); m [ m0(s) = max(m(s); m0(s)). By M(S) we denote the set of all nite multisets over S.
Non-negative integer vectors are often used to encode multisets. Actually, the set of all multisets over nite S is a homomorphic image of NatjSj.
Let P and T be disjoint sets of places and transitions and let F : (P T ) [ (T P ) ! Nat. Then N = (P; T; F ) is a Petri net. A marking in a Petri net is a function M : P ! Nat, mapping each place to some natural number (possibly zero). Thus a marking may be considered as a multiset over the set of places. Pictorially, P -elements are represented by circles, T -elements by boxes, and the ow relation F by directed arcs. Places may carry tokens represented by lled circles. A current marking M is designated by putting M (p) tokens into each place p 2 P . Tokens residing in a place are often interpreted as resources of some type consumed or produced by a transition ring.
For a transition t 2 T an arc (x; t) is called an input arc, and an arc (t; x) | an output arc; the preset t and the postset t are de ned as the multisets over P such that t(p) = F (p; t) and t (p) = F (t; p) for each p 2 P .
A transition t 2 T is enabled in a marking M i 8p 2 P M (p) F (p; t). An enabled transition t may re yielding a new marking M 0 =def M t + t , i. e. M 0(p) = M (p) F (p; t) + F (t; p) for each p 2 P (denoted M !t M 0, or just M ! M 0). We say that M 0 is reachable from M i there is a sequence of rings M = M1 ! M2 ! ! Mn = M 0. For a Petri net N by R(N; m) we denote the set of all markings reachable in M from the marking m, by R(N; m) | the set of all markings reachable in M from its initial marking.
Work ow nets (WF-nets) is a special subclass of Petri nets designed for
modeling work ow processes [
A work ow net has one initial and one nal place, and every place or transition in it is on a directed path from the initial to the nal place. De nition 1. A Petri net N is called a work ow net (WF-net) i 1. There is one source place i 2 P and one sink place f 2 P s. t. i = f = ;; 2. Every node from P [ T is on a path from i to f . 3. The initial marking in N contains the only token in its source place.
By abuse of notation we denote by i both the source place and the initial marking in a WF-net. Similarly, we use f to denote the nal marking in a WF-net N , de ned as a marking containing the only token in the sink place f .
An important correctness property for WF-nets is soundness. Classical
WFnets are called sound if one can reach the nal marking from any marking
reachable from the initial marking [
De nition 2. A WF net N with a source place i and a sink place f is called sound i 1. For every marking m reachable from the initial marking i, there exists a ring sequence leading from m to the nal marking f : 8m 2 R(N ) : (i ! m) ) (m ! f ); 2. The marking f is the only marking reachable from i with at least one token in place f : 8m 2 R(N ) : m f ) m = f ; 3. There are no dead transitions in N :
t 8t 2 T 9m; m0 : i ! m ! m0.
For an arbitrary WF net soundness is decidable, but it is EXPSPACE-hard
[
Modeling work ow consists of modeling case management with the help of sequential routing, parallelism, iteration, and conditional routing. To express it explicitly building blocks such as the AND-split, AND-join, OR-split and OR-join can be used. The AND-split and the AND-join are used for parallel routing. The OR-split and the OR-join are used for conditional routing. All these constructs can be easily expressed in Petri net formalism. (a) (b) (c) (d)
To guarantee, that we get 'good' work ows, we are to balance
AND/ORsplits and AND/OR-joins. Clearly, two parallel ows initiated by an AND-split,
should not be joined by an OR-join. Two alternative ows created via an
ORsplit, should not be synchronized by an AND-join. When we follow these rules
we obtain structured WF-nets (see [
De nition 3. An atomic WF-net is a WF-net, consisting of one source place i, one sink place f and one transition, for which i is the only input place, and f is the only output place.
A WF-net is called a structured WF-net i it can be obtained from atomic WF-nets by successive application of routing operations, shown in Fig. 1.
It was shown in [
Following P. Martens [
De nition 4. A Petri net M = (P; T; F ) is called a work ow module (WFmodule) i 1. The set P of places is a disjoint union of three sets: internal places P N , input places P I , and output places P O. 2. The ow relation is divided into internal ow F N (P N T ) [ (T P N ) and communication ow F C (P I T ) [ (T P O). 3. The net P M = (P N ; T; F N ) is a WF-net. 4. No transition is connected both to an input place and an output place.
Within a WF-module M , the work ow net P M is called the internal process of M and the tuple I(M ) = (P I ; P O) is called its interface. Places belonging to the interface I(M ) are called ports. We suppose that each port in I(M ) has a unique name. A work ow module is called structured i its internal process is a structured WF-net.
A composition of WF-modules, modeling Web services interaction, is de ned as follows.
De nition 6. Let M1; M2 be two WF-modules. A composition M1 M2 of M1 and M2 is a net N obtained from M1 and M2 by merging input ports of M1 with output ports of M2 with the same names, and similarly output ports of M1 with input ports of M2, i.e. p1 2 I(M1) and p2 2 I(M2) are merged i they have the same name and one of them is an input port, while the other is an output port.
An example of two WF-modules composition is shown in the next section.
A composition M1 M2 of two WF-modules M1 and M2 can be easily transformed into a WF-module as follows. Let i1; i2 be source places in M1 and M2 correspondingly, and f1; f2 be their output places. Add to M1 M2 a new source place i, a new sink place f , and two new transitions ti; tf , s.t. ti = fig, ti = fi1; i2g, and tf = ff g, ti = ff1; f2g.
We say that a composition M1 M2 is sound i its corresponding WF-module is sound. 3
As a motivating example we consider a model of credit allowance. The model describes two services, represented by two WF-modules.
The WF-module WFM1 in Fig. 2 models a service of a bank credit system, that allows to estimate whether it is reasonable to loan money to this or that person. In this model work startes from the position \p 1", where one token is placed in the initial state. Then service sends client information to the credit bureau (\t 1") and is waiting for the response (\p 2"). When bank system takes the credit rating and is analyzed it (\t 3"), decision makes in position \p 3", service can goes to the \p 1" through \t 2" for the repetition of request , or can goes to the operation of the payment. There are two ways for that (\t 5" and \t 6"). First, pay all accounts, which were obtained from the credit bureau (\t 7"). Second, send information about the client, when he will pay the loan. At the end of the each possible way bank system sends E to report about the competition of conversation(\t 9", \t 10") and stops in position \p 8".
Fig. 3 shows a WF-module, modeling a credit bureau. It is a company that collects information from various sources and provides consumer credit information on individual consumers for a variety of uses. Here there are four internal places and four interface places. \p 10" is starting position, where service is waiting for the client information from the external bank system. When it receives necessary data from \CD", transition \t 11" res, client credit rating is calculated, and service goes to the position \p 12". If position \CR" is enabled, that means that bank is requesting for the credit rating. In that case credit bureau sends this information (\CR") to the partner service(\t 12"), after that sends an account (\A") to the bank (\t 13") and goes to the place \p 10" again. Otherwise, if credit bureau receives end request (\E"), it goes to the nal position \p 13" and stops.
Interaction of these two services is modeled by the composition of the corresponding WF-modules, depicted in Fig. 4. Services communicate with each other in the following way: the bank sends all information about the person to the credit bureau, this information is analyzed, and basing on all data credit bureau provides a credit rating of a de nite client to the bank. This sequence of actions may be repeated several times.
While each of WF-modules WFM1 and WFM2 is sound, their composition WFM1 M WFM2 is not sound. These services are resource incompatible, i.e. for these services there is no executions without pending inputs and/or outputs. In the next sections we show, how to nd out such incompatibilities. 4
Let M be a structured WF-module with two disjoint sets P I of input places and P O output places. Consider then some run for M | a sequence of states and transition rings, starting from the initial state and coming to the nal state of M . For each run the pair of input and output resources R( ) = (RI ( ); RO( )), where RI ( ) 2 M(P I ) and RO( ) 2 M(P O), are de ned as multisets of inputs/outputs consumed/produced in the course of execution. By (M ) we denote the set of all pairs of resources for all runs in M . More formally: De nition 7. Let M be a structured WF-module with input ports P I and output ports P O. Then for RI 2 M(P I ) and RO 2 M(P O) we de ne (RI ; RO) 2 (M ) i f + RO 2 R(M; i + RI ).
It is easy to note, that a pair of multisets over non-intersecting sets of places
can be considered as just one multiset. Thus for a work ow module a resource
is a multiset language [
For describing resources of structured work ow modules we de ne a special language of quasi-regular expressions.
De nition 8. Let Atom be a nite set of atoms (letters). The language of quasiregular expressions over Atom is de ned by induction as follows: 1. 2 L; 2. a 2 L, if a 2 Atom; 3. e1 e2 2 L, if e1; e2 2 L; 4. e1 e2 2 L, if e1; e2 2 L; 5. e 2 L, if e 2 L.
Semantics of L maps a quasi-regular expression e to a multiset language (e), i.e. a set of multisets over Atom according to the following rules: (e1); m2 2
(e2)g; [ (en) : : : , where e0 = , en = e en 1 for 1. ( ) = ;; 2. (a) = [a] for a 2 Atom; 3. (e1 e2) = fm1 + m2jm1 2 4. (e1 e2) = (e1) [ (e2); 5. (e ) = (e0) [ (e1) [ (e2)
n 1.
De nition 9. We say that a quasi-regular expression e is in the standard form, i e = e1 en, where n 1, e1; : : : ; en do not contain and nested . Proposition 2. Every quasi-regular expression can be transformed to an equivalent quasi-regular expression in the standard form by applying equations (1{12). Proof (Sketch). To take -operation outside we use equations 8 and 11. Equations 10, 12 allow taking -operation outside in subexpressions without . Nested are eliminated with the help of equation 10.
Now we show, that for a structured WF-module M a quasi-regular expression e(M ), describing interface resources (M ), can be e ectively constructed.
Recall, that structured work ow nets are constructed from atomic transitions by sequential application of four control structures: sequential routing, conditional routing, parallel routing and iteration.
Algorithm 1. (Constructing a quasi-regular expression representing interface resources of a WF-modul).
For a structured work ow module M a quasi-regular expression e(M ) can be constructed by induction on the structure of internal process N of M : { for an atomic net N | a transition with input resource places p1; : : : ; pk and output resource places q1; : : : ; qn, de ne e(N ) =?p1 ?pk !q1 !qn; { for N being sequential composition of N1 and N2 de ne e(N ) = e(N1) e(N2); { for N being parallel composition of N1 and N2 de ne e(N ) = e(N1) e(N2); { for N being selective composition of N1 and N2 de ne e(N ) = e(N1) e(N2); { for N being an iteration of N1 and N2 de ne e(N ) = e(N1) (e(N2) e(N1)) . Proposition 3. Let M be a structured WF-module, and let e(M ) be a quasiregular expression, obtained for M according to the Algorithm 1. Then e(M ) = (M ).
The proof of this proposition is straightforward by induction on the structure of the internal process of a given WF-module. 5
We say, that two work ow modules are resource compatible, if they may execute runs with producing/consuming mutually complimentary resources. If the composition of two work ow modules is sound, then they are resource compatible. However, it could be that for resource compatible modules their composition is not sound, since resources may be outputted in a wrong order. So, resource compatibility is a necessary, but not su cient condition for the correctness of services composition.
De nition 10. Let M1; M2 be two WF-modules with source places i1; i2 and sink places f1; f2 correspondingly. We say that M1 and M2 are resource compatible i f1 + f2 2 R(i1 + i2) in M1 M2.
Immediately from the de nition we get that if M1 M2 is sound, then M1 and M2 are resource compatible.
We show that resource compatibility is decidable for structured WF-modules.
Algorithm 2. (checking resource compatibility of two structured WF-modules). Let M1; M2 be structured WF-modules.
Step 1. Construct quasi-regular expressions e(M1); e(M2).
Step 2. Reduce e(M1); e(M2) to standard forms es(M1); es(M2) correspondingly.
Step 3. Construct a complementary expression es 1(M1) by changing ? for ! and vice versa in es(M1).
Step 4. Check whether (es 1(M1)) \ (es(M2)) is not empty. If (es 1(M1)) \ (es(M2)) is not empty, output \YES", otherwise output \NO".
Proposition 4. Let M1; M2 be two structured WF-modules. Modules M1 and M2 are resource compatible i the output of the Agorithm 2 for M1; M2 is \YES".
All steps of the Algorithm 2 except for Step 4 are already described. Checking, whether the intersection of multiset languages (es 1(N1)) and (es(N2)) is empty, can be reduced to solving a set of linear equations.
We illustrate this algorithm by applying it to our motivation example from Section 3.
First we build quasi-regular expressions for bank and credit bureau services: e(WFM1) = (!CD ?CR) ((?A !E) (!CD !E)); e(WFM2) =?CD (!CR !A ?CD) ?E.
Then we are to reduce these expressions to regular forms. Note, that e(WFM2) is already in a regular form, and hence e(WFM2) = es(WFM2). To reduce e(WFM1) it is su cient to apply distributivity law (equation 8): es(WFM1) = ((!CD ?CR) ?A !E) ((!CD ?CR) !CD !E). Then es 1(WFM1) = ((?CD !CR) !A ?E) ((?CD !CR) ?CD ?E).
Now r 2 es 1(WFM1) i r = n1 ?CD + n1 !CR + n2 !A+?E, or r = (n1 + 1) ?CD + n1 !CR+?E for some natural n1; n2 0.
Similarly, r 2 es(WFM2) i r = (n + 1) ?CD + n !CR + n !A+?E for some natural n 0.
The multiset (es 1(WFM1)) \ (es(WFM2)) is not empty i at least one of the following sets of simultaneous equations is consistent.
Set 1 of equations (corresponds to the rst summand in es 1(WFM1): n1 = n + 1 (factors of ?CD), n1 = n (factors of !CR), n2 = n (factors of !A), 1 = 1 (factors of ?E).
Set 2 of equations (corresponds to the second summand in es 1(WFM1): n1 = n + 1 (factors of ?CD), n1 = n (factors of !CR), 0 = n (factors of !A), 1 = 1 (factors of ?E).
Both these sets of equations are obviously inconsistent. So, we can immediately conclude, that the services of our bank example in Section 3 are not comparable.
Note, that Algorithm 2 has a polynomial on the size of WF-module time complexity. 6
In this paper we have presented a new approach for detecting incompatibility of Web services by analysis of resource compatibility of their structured work ow models. The resource compatibility is a necessary condition for soundness of composition of work ow models.
We introduce a language of quasi-regular expressions for describing multiset languages, and use this language for representing interface resources of structured work ow modules. Checking resource compatibility is then reduced to checking emptiness of intersection of multiset languages, represented by quasi-regular expressions. Thus checking resource compatibility can be solved in polynomial time.
Though resource compatibility is not su cient for correct Web service interaction, the proposed procedure may be helpful for e cient detecting in consistences on the early stages of analysis of Web services.