The greater and greater quantity of services that are available over the web causes a growing attention to techniques that facilitate their reuse. A web service specification can be quite complex, including various operations and message exchange patterns. In this work, we focus on the problem of retrieving a web service, which can play a given choreography role, preserving at the same time a condition of interest (the goal to satisfy which the service is sought). We show that current semantic matchmaking techniques do not guarantee goal preservation. We also show an approach for overcoming these limits, which exploits the choreography definition. This work is based on an action-based representation of the operations of a service: each operation is described in terms of its preconditions and effects, without taking into account the ontology layer which is not functional to the aims of the work.
Web services have a platform-independent nature, that endeavors enterprises to
develop new business processes by combining existing services, retrieved over
the web [
The need of adding a semantic layer to service descriptions brought to
initiatives like the development of the language OWL-S [
Semantic annotation allows the discovery of services, whose descriptions do
not exactly match with the corresponding queries. Intuitively, they allow the
retrieval of services, which have been developed for a (slightly) different purpose
but that can however be used for the aims of the current query. Therefore, these
techniques facilitate software reuse. So-called semantic matchmaking techniques
(e.g. [
Semantic matchmaking focuses on the discovery of single services, in the sense
that a service is considered as corresponding to a single operation. In general,
however, the use of a web service implies the execution of a sequence of operations
in a particular order, which might even involve other services [
On the other hand, the need of describing compositions of services, which
have to interact according to (complex) patterns of interaction, ruled by
conversation protocols, has lead to the development of choreography languages like
WS-CDL [
The task of selecting a web service, that should play a role in a
choreography (rather than using the choreography as the design of a new set of services),
implies verifying two things: the conformance of the service to the specification
of a role of interest, and that the use of that service allows the achievement
of the goal, that caused its search. Conformance guarantees the
interoperability of the service with the players of the other roles [
In [
The article is organized as follows. Section 2 introduces a simple representation for services, that is based on a declarative language, to abstract away from the details of implementation. Section 3 reports the main results of the work: we introduce the notions of conservative and of uninfluential substitution, and we show that it is possible to exploit the choreography to select services in such a way that a goal of interest is preserved. Throughout these sections we will use a same running example (introduced little by little), that is centered on the interaction ruled by the simple purchase-flight protocol in Figure 1. Such protocol captures the interaction between a flight ticket seller and one of its clients. In the various sections we will see the how the protocol specification is given, in the declarative language that we have adopted, as well as some implementations associated to specific services, discussing about them. Related works (Section 4) and conclusions end the paper. 2
In this section, we briefly summarize the notation that we use to represent
services, introduced in [
Service representation
A service description is defined as a triple hO, G, Pi, where O is a set of
operations, G is a set of actions that allow to receive messages, and P (policy) is a
description of the interactive behavior of the service. The name “policy” derives
from the literature concerning conversation protocols [
– The set O contains the descriptions of a set of service operations. An
operation is an atomic action. As such, it is described in terms of its executability
preconditions and effects, the former being a set of fluents (introduced by
the keyword possible if) which must be contained in the service state in
order for the operation to be applicable, the latter being a set of fluents
(introduced by the keyword causes) which will be added to the service
state after the operation execution. Formalized in these terms, operations,
when executed, trigger a revision process on the actor’s beliefs. Since we
describe web services from a subjective point of view (i.e. taking the
perspective of a specific service, by representing and reasoning on the service
policies), we distinguish between the case when the service is either the
initiator or the servant of an operation by further decorating the operation
name with a notation inspired by [
As an example, let’s consider search flight, an operation of a flight reservation service, which is offered by a seller and can be invoked by a client to search information about flights with given departure and arrival locations. From the point of view of the client, the operation search flight is represented as: search flightÀ(seller, Date, Start, Dest)
possible if {BStart, BDest, BDate} search flightÀ(seller, Date, Start, Dest)
causes {Bwill get of f er} This notation captures the preconditions and the effects of the operation: the precondition is that the departure location is known (BStart), that the destination is known (BDest), and that the day of departure is also known (BDate); the effect is that after the execution the invoker (the client) expects that an offer will be sent (Bwill get of f er).
Last but not least, a service can also have internal operations, which can be included in its policy but are not visible from outside. Each operation is represented again as an atomic action, specified by its preconditions and its effects. Formally, it is defined as: operation(content) causes {E1, . . . , En} operation(content) possible if {P1, . . . , Pt} where Ei, i ∈ [1, n], and Pj , j ∈ [1, t], denote respectively the fluents, which are expected as effect of the execution of an operation and the precondition to its execution, while content denotes possible additional data that is required by the operation. Notice that such operations can also be implemented as invocations to other services. As an example, here is the description of the eval offer internal operation of a possible client for the flight-purchase interaction: eval offer possible if {Bof f er(f light)} eval offer causes {Beval rst(Y )} eval offer applies when an offer for a flight is available and produces an evaluation that can be used for taking internal decision. The variable Y ranges over the set {business, no business} depending on the kind of ticket that is being considered. – Besides operations, we explicitly represent actions that allow the reception of information. We call them get-answer actions (set G). The range of possible answers is supposed to be finite, in the sense that the interlocutor is supposed to use a message out of a finite and predefined set of alternatives: if a different message is sent the service is not able to handle it. We imagine the reception of a piece of information as a “one-way” operation that is invoked over the recipient. Actually, for technical reasons in our formalization, each possible alternative answer corresponds to a different operation of this kind. Formally, they are represented as:
receive act(interlocutor, content) receives I where interlocutor is the partner in the interaction, content is used to store the received message, and I is a set of alternative action invocations each allowing the reception of one of the alternative messages. As an example get answer, reported hereafter, allows the reception of either a not available¿ answer or of an offer through the execution of one of the two actions not available¿ and offer¿. The decision of which of the two actions will be executed is up to the interlocutor that decides which message to send.
get answer(Seller) receives [not available¿(Seller) or offer¿(Seller)] In this example we do not use the content. – P encodes the behavior for the service; it is a collection of clauses of the kind:
p0 is p1, . . . , pn where p0 is the name of the procedure and pi, i = 1, . . . , n, is either an atomic action (operation), a get-answer action, a test action (denoted by the symbol ?), or a procedure call. Procedures can be recursive and are executed in a goal-directed way, similarly to standard logic programs, and their definitions can be non-deterministic as in Prolog. As an instance, here we report the booking procedure: booking(Seller, Date, Start, Dest) is search flightÀ(Seller, Date, Start, Dest), get answer(Seller),
Bof f er(not avail)? booking(Seller, Date, Start, Dest) is search flightÀ(Seller, Date, Start, Dest), get answer(Seller),
Bof f er(f light)?, eval offer, finalize(Seller) It is defined by a set of two clauses, the former capturing the case when the ticket is not available, the latter the normal situation when an offer for a ticket is actually returned. In this case, the offer is evaluated and the purchase is finalized by invoking another procedure.
A choreography is made of a set of interacting roles, a role being a subjective view of the interaction that is encoded. When a service plays a role in a choreography, its policy will contain some operations which are not of the service itself but belong to some other role of the choreography, with which it interacts. In other words, O can be partitioned in two sets: a set of bound operations and a set of unbound operations, that must be supplied by some counterpart(s). Until the counterpart(s) service is (are) not defined, such operations will be those specified in the choreography. We assume that they are represented in a way that is homogeneous with the representation of operations, i.e. by means of preconditions and effects. The binding will be possible only when the partner in the interaction will be found. The fact that the former service is taking a given role in the choreography is due, in our proposal, to the fact that it knows that a certain goal condition will be true after the execution of the role. When a possible partner is identified for the latter role, after the binding has taken place, it is necessary to check if the goal condition is preserved. The reasons for which this could not happen are explained in the following section; hereafter, we formalize the notion of substitution that we interpret as the binding.
Let Sd = hO, G, Pi a service description, and let Ou be a subset of O, containing unbound operations that are to be supplied by a same counterpart Si. Let OSi be the set of operations in Si that we want Sd to use, binding them to Ou. We represent the binding by the substitution θ = [OSi /Ou] applied to Sd, i.e.: Sdθ = hOθ, Gθ, Pθi, where every element of Ou is substituted by/bound to an element of OSi . Notice that not all elements of OSi are, instead, necessarily bound. An example is reported in Example 3.
Example 1. Let us introduce, as an example, a simple choreography (see
Figure 1) that rules a flight reservation protocol, inspired to [
Let us consider a service b1 that is conformant to the role Buyer. Following the proposed notation, we describe it as hO, G, Pi, where P = {booking, finalize}, O = {search flightÀu, not available¿u, eval offer, offer¿u, ackÀu, n ackÀu}, G = {get answer}. Notice that all the operations but eval offer are unbound and depend on the service that will actually play the other role. Instead, eval offer is an internal action of the buyer, that is used to decide whether accepting or refusing an offer. The procedures in P are described by the following clauses: booking(Seller, Date, Start, Dest) is search flightÀu(Seller, Date, Start, Dest), get answer(Seller),
Bof f er(not avail)? booking(Seller, Date, Start, Dest) is search flightÀu(Seller, Date, Start, Dest), get answer(Seller),
Bof f er(f light)?, eval offer, finalize(Seller) finalize(Seller) is
Beval rst(business)?, ackÀu(Seller) finalize(Seller) is
Beval rst(no business)?, n ackÀu(Seller) get answer(Seller) receives [not available¿u(Seller) or offer¿u(Seller)] The only get message action in G is described by: Finally, the operations in O are described as: eval offer causes {Beval rst(Y )} eval offer possible if {Bof f er(f light)} search flightÀu(Seller, Date, Start, Dest)
causes {Bwill get of f er} search flightÀu(Seller, Date, Start, Dest)
possible if {Bstart, Bdest, Bdate} not available¿u(Seller) causes {Bof f er(not available)} not available¿u(Seller) possible if {} offer¿u(Seller) causes {Bof f er(f light)} offer¿u(Seller) possible if {} ackÀu(Seller) causes {Bbooked(f light)} ackÀu(Seller) possible if {} n ackÀu(Seller) causes {B¬booked(f light)} n ackÀu(Seller) possible if {} where X ranges on the set {not available, f light} and Y ranges on the set {business, no business}. All the above definitions, but the one of eval offer, are supplied by the choreography. ¤ In the outlined framework, it is possible to reason about goals by means of queries of the form:
Fs after p where Fs is the goal (represented as a conjunction of fluents), that we wish to hold after the execution of a policy p. Checking if a formula of this kind holds corresponds to answering the query: “Is it possible to execute p in such a way that the condition Fs is true in the final state?”. When the answer is positive, the reasoning process returns a sequence of atomic actions that allows the achievement of the desired condition. This sequence corresponds to an execution trace of the procedure and can be seen as a plan to bring about the goal Fs. Such a plan can be conditional because whenever a get-answer action is involved, none of the possible answers from the interlocutor can be excluded. In other words, the trace will contain a different execution branch for every option.
This form of reasoning is known as temporal projection. Temporal projection fits our needs because, as mentioned in the introduction, in order to perform the selection we need a mechanism that verifies if a goal condition holds after the interaction with the service has taken place. Fs is the set of facts that we would like to hold “after” p.
Let Sd = hO, G, Pi be a service description. The application of temporal projection to P returns, if any, an execution trace, that makes a goal of interest become true. Let us, then, consider a procedure p belonging to P, and denote by G the query Fs after p. Given a state S0, containing all the fluents that we know as being true in the beginning, we denote the fact that G is successful in Sd by:
(hO, G, Pi, S0) ` G The execution of the above query returns as a side-effect an execution trace σ of p. The execution trace σ can either be linear, i.e. a terminating sequence a1, . . . , an of atomic actions, or it can contain branches, that are due, as we have mentioned, to the presence of get-message actions.
Example 2 (Flight-purchase, second part). Let us suppose that the initial state of the service b1 is S0 = {Bdate, Bstart, Bdest, Bsmoking f light}, (all the other fluents truth value is “unknown”). This means that b1 assumes a date, a departure location, an arrival location and that on the flight it is allowed to smoke. The goal of b1 is that the following condition holds: G = {Bbooked(f light), Bsmoking f light} after booking(seller, date, start, dest) Intuitively, the buyer expects that, after the interaction, it will have a reservation on a smoking flight.
By reasoning on its policy and by using the definitions of the unbound operations that are given by the choreography, b1 can identify an execution trace, that leads to a state where G holds: σ = search flightÀu(seller, date, start, dest); offer¿u(seller);
eval offer; ackÀu(seller) This is possible because in a declarative representation specifications are executable. Moreover notice that this execution does not influence the belief about the smoking flight, which persists from the initial through the final state and is not contradicted. ¤ 3
When the matching process is applied for selecting a service that should play a role in a (partially instantiated) choreography, the desire is that the substitution (of the service operations to the specifications contained in the choreography) preserves the properties of interest. Let us formalize this notion.
Definition 1 (Conservative substitution). Let us consider a service Si = hO, G, Pi which plays a role Ri in a given choreography, and a query G such that, given an initial state S0, Consider a substitution θ = [OSj /Ouσ(Rj)], where Ou(Rj) = {ou ∈ O | o occurs in σ} σ is the set of all unbound operations that refer to another role Rj , j 6= i, of the same choreography, that are used in the execution trace σ. θ is conservative when the following holds:
(hOθ, Gθ, Pθi, S0) ` G w.a. σθ
In the above definition, θ can be any kind of association between the
operations of a service with the operations described in a choreography. In practice is
the result of a matching process. In the literature it is possible to find many match
algorithms, many of them (in the case of semantic web services) are grounded
into the work by Zaremski and Wing [
Zaremski and Wing propose a formal specification to describe the behavior of software components, and to determine if two components match. Each software component has precondition Precs(s) and postcondition Effs(s). Their specifications are matched against a requirement, coherently specified as having precondition Precs(r) and postcondition Effs(r). Five kinds of relaxed match between r and s are defined, that we rephrase hereafter, to adapt them to our framework: – EM (Exact Pre/Post Match): Precs(r) = Precs(s) ∧ Effs(r) = Effs(s) – PIM (Plugin Match): Precs(r) ⊇ Precs(s) ∧ Effs(s) ⊇ Effs(r) – POM (Plugin Post Match): Effs(s) ⊇ Effs(r) – GPIM (Guarded Plugin Match): Precs(r) ⊇ Precs(s) ∧ ((Precs(s) ∪ Effs(s)) ⊇
Effs(r)) – GPOM (Guarded Post Match): ((Precs(s) ∪ Effs(s)) ⊇ Effs(r))
Exact pre/post match states the equivalence of r and s. Plugin match is weaker:
s must only be behaviorally equivalent to r when plugged-in to replace r. Plugin
post match relaxes the former: only the postcondition is considered. Guarded
matches focus on guaranteeing that the desired postcondition holds when the
precondition of s holds, not necessarily in general. The different matches can
be organized according to a lattice [
It is immediate to see that any substitution, obtained by applying the exact pre/post match, satisfies Definition 1. However, this is not true for the other kinds of match. Let us show this with the help of a simple example. Example 3. The buyer service b1 (see previous examples) is looking for another service, which can play the role of the Seller, to reserve a flight seat. This service must provide a set of operations that will substitute the unbound operations of the buyer role. Let us choose the plugin match as matching rule. Let us consider the candidate s1, a service that is conformant to the protocol w.r.t. the role Seller. The set of operations of the seller represented in the knowledge base of the buyer includes the following definition for operation search flightÀ: search flightÀ(Seller, Date, Start, Dest)
possible if {Bstart, Bdest, Bdate} search flightÀ(Seller, Date, Start, Dest)
causes {Bwill get of f er, B¬smoking f light} while all the other operations are defined exactly as in Example 1.
By applying the plugin match, we obtain the substitution θP IM , which includes, among the others, also [search flightÀ/search flightÀu] 1. By applying the substitution θP IM we obtain the set of policies PθP IM : booking(Seller, Date, Start, Dest) is search flightÀ(Seller, Date, Start, Dest), get answer(Seller),
Bof f er(not avail)? booking(Seller, Date, Start, Dest) is search flightÀ(Seller, Date, Start, Dest), get answer(Seller),
Bof f er(f light)?; eval offer; finalize(Seller) finalize(Seller) is
Beval rst(business)?; ackÀ(Seller) finalize(Seller) is
Beval rst(no business)?; n ackÀ(Seller) By using this policy, the query (hOθP IM , GθP IM , C, PθP IM i, S0) ` G fails: in fact, the additional effect B¬smoking f light of the service search flightÀ prevents the buyer to achieve a part of its goal, i.e. to book a smoking flight. ¤ Theorem 1. The class of PIM, POM, GPIM and GPOM substitutions are not conservative.
Proof. The proof is given by the counterexample in Example 3. In fact, θ, besides being a PIM substitution, is also an instance of all the other kinds of substitution that we have listed, i.e. it is also a POM, a GPIM, and a GPOM substitution. In order for a substitution to be conservative, it must take into account also the overall structure, encoded by the choreography. The locality of the matches used in the matchmaking phase, indeed, seriously limits the possibility of re-using services by selecting and composing them in an automatic way.
In the remainder of this section, we focus on the plug-in match. The plugin match is one of the most used matches and it immediately follows the exact match in the lattice (it is the strongest of the flexible matches). We show how to enrich it so to allow the construction of conservative substitutions. To this aim, we take into account the dependencies between actions, which produce as effects fluents, that are used as preconditions by subsequent action. Intuitively, the idea is to verify that the “causal chain” which allows the execution of the sequence of actions, is not broken by the differences between capabilities/services and requirements, as instead happens in the example. The obvious hypothesis is that we have a choreography and that we know that it allows to achieve the goal of interest, i.e. that there is an execution σ of the role specification, which allows the achievement of the goal. We will use this trace for defining the additional properties for the match. 1 For the sake of brevity, we omit to specify the substitutions when the operations exactly match the specifications.
Let us start by introducing the notions that define dependencies between actions and dependency sets for fluents. Consider a service description S = hO, G, Pi, and suppose that, given the initial state S0, the goal G = Fs after p succeeds, thus obtaining as answer the successful sequence of actions σ = a1; a2; . . . ; an, which is an execution trace of p.2 We denote by σ the sequence of actions a0; a1; a2; . . . ; an; an+1, where a0 and an+1 are two fictitious actions that will be used respectively to represent the initial state S0 and the set of fluents Fs, which must hold after σ. That is, we assume a0 has no precondition and Effs(a0) = S0, and that an+1 has no effect but Precs(an+1) = Fs.
Consider two indexes i and j, such that j < i, i, j = 0, . . . , n + 1. We say that in σ the action ai depends on aj for the fluent Bl, written aj ÃhBl,σi ai, iff Bl ∈ Effs(aj), Bl ∈ Precs(ai), and there is not a k, j < k < i, such that Bl ∈ Effs(ak). Given a fluent Bl and a sequence of actions σ, we can, therefore, define the dependency set of Bl as Deps(Bl, σ) = {(j, i) | aj ÃhBl,σi ai}.
Let [s/ou] be a specific substitution of a service operation s to an unbound operation ou, that is contained in θP IM , we say that a fluent Bl ∈ Effs(s) − Effs(ou) (i.e. an additional effect of s w.r.t. the effects of ou) is an uninfluential fluent w.r.t. the sequence σθP IM iff for all pairs (j, i) ∈ Deps(B¬l, σ), identifying by k the position of ou in σ, we have that k < j or i ≤ k, Intuitively, this means that the fluent will not break any dependency between the actions which involve the inverse fluent because either it will be overwritten or it will appear after its inverse has already been used. Note that σ and σθP IM have the same length and are identical as sequences of actions but for the fact that in the latter the selected service operations substitute unbound operations. For this reason, we can reduce to reasoning on σ for what concerns the action positions.
A substitution θP IM is called uninfluential iff for any substitution [s/ou] in θP IM , all beliefs in Effs(s) − Effs(ou) are uninfluential fluents w.r.t. σ. Now we are in position to prove that a substitution which exploits the plugin match and which is also uninfluential, is conservative.
Theorem 2. Let us consider a service Si = hO, G, Pi which plays a role Ri in a given choreography, and a query G such that, given an initial state S0, (hO, G, Pi, S0) ` G w.a. σ Consider an uninfluential substitution θP IM = [OSj /Ouσ(Rj)], where Ou(Rj) = σ {ou ∈ O | o occurs in σ} is the set of all unbound operations that refer to another role Rj, j 6= i, of the same choreography, that are used in the execution trace σ. Then, the following holds:
(hOθP IM , GθP IM , PθP IM i, S0) ` G w.a. σθP IM
Proof. The proof is by absurd and it uses the proof theory introduced in [
G w.a. σθP IM . Since, by hypothesis, for any substitution [o/ou] in θP IM , Effs(o) ⊆ Effs(ou) holds, there exists a fluent F such that a0, a1, . . . , ai−1 ` F but (a0, a1, . . . , ai−1)θP IM 6` F , where σ = a0, a1, . . . , ai−1, ai, . . . , an and F ∈ Precs(ai). Now, since a0, a1, . . . , ai−1 ` F , there exists j ≤ i − 1, such that a0, a1, . . . , aj ` F and F ∈ Effs(aj) but (a0, a1, . . . , aj)θP IM 6` F , that is F 6∈ Effs(ajθP IM ). This is absurd due to the hypothesis that θP IM is an uninfluential substitution. ¤ Example 4. Let us now consider the goal and the service description specified in Example 1, and let us also consider another service s2, that is conformant to the role Seller. Let s2 be equivalent to the role specification but for the service that implements search flightÀu, which is specified as: search flightÀ(Seller, Date, Start, Dest)
possible if {Bstart, Bdest, Bdate} search flightÀ(Seller, Date, Start, Dest)
causes {Bwill get of f er, Bveg meals} Differently than the one of s1, this service does not compromise the achievement of the goal, even though it provides some additional information (Bveg meals). This information is not used in the interaction that we are considering but we must take into account the fact that s2 might be conformant also to other protocols, in which this information is relevant. It is realistic that the service will not be re-implemented each time if not strictly necessary. ¤
The verification that a substitution is uninfluential involves the derivation σ, and it is based on checking whether the chains of dependencies between actions for the various fluents are not interrupted by some opposite fluent. Obviously, if the domain is such that no fluent, once asserted, can be negated, any θP IM will be conservative. This can be verified statically on the choreography and the set of unbound operations, by checking that every fluent (that appears as effect of some action) is always positive or negative, including the initial state and the goal in the verification. Indeed, the application domains in which actions produce knowledge are of this kind. 4
In this work we have studied the relation between the matchmaking rules and
the achievement of a goal in a choreography, within the process of selecting a
service for playing a role. We have shown that, when the adoption of a role is due
to the desire of reaching a goal, the matches performed on single operations (but
the exact match) are not adequate and it is necessary to introduce a verification
that takes into account the context given by the choreography. Afterwards, we
have presented an extension of the plugin match that takes into account also the
choreography. To the best of our knowledge, the selection of a service based on a
kind of match that takes into account context of application of the sought services
(i.e. the choreography in which it will be immersed) has not been yet tackled in
the literature, with the only exception of the work by Biswas [
The literature related to matchmaking is wide and it is really difficult to be
exhaustive. The matches proposed in [
WSMO (Web Service Modeling Ontology) [
The idea of synthesizing a policy from an abstract specification is also stated
in [
Works like [
The next step of this research will be to test the presented method, by
implementing it in a real system and applying it to real cases. In particular, for
what concerns the representation we mean to explore the use of SAWSDL [
This research has partially been funded by the European Commission and by the Swiss Federal Office for Education and Science within the 6th FP project REWERSE number 506779 (cf. http://rewerse.net), and by MIUR PRIN 2005 “Specification and verification of agent interaction protocols” national project. Claudio Schifanella is partially supported by the fellowship program “Fondazione CRT - Progetto Lagrange” (cf. http://www.progettolagrange.it).