- We present a vision of smart, goal-oriented web services that reason about other services' policies and evaluate the possibility of future interactions. We assume web services whose interface behaviour is specified in terms of reactive rules. Such rules can be made public, in order for other web services to answer the following question: “is it possible to inter-operate with a given web service and achieve a given goal?” In this article we focus on the underlying reasoning process, and we propose a declarative and operational abductive logic programming-based framework, called WAVe.
I. INTRODUCTION
Service Oriented Computing (SOC) is rapidly emerging as
a new programming paradigm, propelled by the wide
availability of network infrastructures, such as the Internet, and by
the success of its predecessor, Object Oriented programming
paradigm. Web service-based technologies are an
implementation of SOC, aimed at overcoming the intrinsic difficulties of
integrating different platforms, operating systems, languages,
etc., into new applications. It is then in the spirit of SOC to
take off-the-shelf solutions, like web services, and compose
them into new applications. Service composition is very
attractive for its support to rapid prototyping and possibility
to create complex applications from simple elements. It is
the philosophy followed, e.g., by BPEL [
If we adopt the SOC programming paradigm, how to exploit the potential of a growing base of web services becomes one of our strategic issue. In a domain in which being more competitive means knowing more and using all available information at best, how shall we cope with the proliferation of new services? How shall we decide to use a web service rather than another one? when new ones become available, shall we go for them? are there new opportunities that were not there before? It is a necessary, never-ending, heavy and thus potentially very costly decision process, but it could also be very rewarding, if we had the proper tools.
A partial answer to these questions is given by service discovery. As new services become available, they are published, for instance by registration on some yellow-pages server; existing services can then become aware of the new ones and exploit them. This solves part of the problem: as through discovery we only know that there are some services, which possibly follow some standards, but understanding whether interacting with them will be profitable or detrimental, is far from being a trivial question. For one, it is not possible to think to try and invoke all newly discovered services and analyze the results. Beside being highly error-prone, such a method would require expensive rollbacks that are often unaffordable at runtime. Thus, alternative approaches have to be developed. This is what we intend to address in this article.
The focus of this article is the following problem: how to dynamically understand if two web services can interoperate, without them having a-priori knowledge of each other’s capabilities, but by reasoning about policies exchanged at run-time.
We present a vision of smart, goal-oriented web services that reason about other services’ specifications, with the aim to separate out those that can lead to a fruitful interaction, without resorting to trial and error. We envisage a two-phase discovery activity on the side of web services. First, web services collect information about other web services, and try and understand by reasoning which ones can lead to a fruitful interaction. This activity is carried out off-line, beforehand. Then they use the available information to interact with each other. It is the same philosophy of search engines: before, collect information through web spiders, then use it when requested by the user.
In this article we focus on the reasoning involved in the offline phase, assuming that a new web service has been found, and we must decide about the possibility to interact with it. We assume that each web service publishes, alongside with its WSDL, its interface behaviour specifications. By reasoning on the information available about other web services’ interface behaviour, each web service can verify which goals can be reached by interaction.
To achieve our vision, we propose a proof theoretic approach, based on computational logic – in fact, on abductive logic programming. In particular, we formalise policies for web services in a declarative language which is a modification of the SCIFF language originally defined in the context of the EU IST-2001-32530 project, to specify and verify social-level agent interaction.
In this new language, policies can be defined by way
WAVe Gws' KBws' ICws'
RIF decoder/encoder
Reasoning Knowledge
Rules Interchange
Format of social integrity constraints (ICs): a sort of reactive rules used to generate and reason about expectations about possible evolutions of a given interaction setting.
As claimed in [
Moreover, we believe that, as advocated by Alferes et al.
[
Based on the SCIFF framework we propose a new declarative semantics and a new proof-procedure that combines forward, reactive reasoning with backward, goal-oriented reasoning, and is tailored to the discovery activity’s off-line phase’s verification problem. We have called this new framework WAVe(Web-service Abductive Verification).
In order to support the exchange of rules between web services in a standard format, we also propose a RuleML encoding for our language.
We start by showing the abstract architecture of WAVe. In Sect. III we introduce a running on-line shopping scenario. In Sect. IV, we briefly introduce the language used in the framework, and in Sect. V we show how the scenario can be modeled in WAVe in terms of ICs. Sect. VI presents the declarative and operational semantics of WAVe, and Sect. VII proposes the application of WAVe to the verification problem in the reference scenario. Sect. VIII discusses the encoding of WAVe rules in RuleML. A brief discussion, also with respect to related work, follows.
Fig. 1 depicts our general reference architecture. Arrows indicate the flow of policies between web services. The layered architecture of a web service, e.g. ws, has WAVe at the top of the stack, performing reasoning based on its own knowledge and on the policies obtained from other web services, e.g. ws0. The functionalities of the various elements of the knowledge will be explained in Sect. IV. For the moment, we say that policies are identified with the ICws component. The architecture is symmetric. We represented with thick borders the modules involved in the operations carried out by ws, and its output. In order for ws0 to pass ICws0 on to ws (and
WAVe Gws KBws ICws
RIF
decoder/encoder
policies
policies
network
vice versa), a Rule Interchange Format (RIF) is adopted. One
possibility for such a RIF could be RuleML [
Fig. 1 does not show control elements, but only information flows. We assume that suitable interaction protocols are defined to control the flow of information (e.g. policies) between the web services. In particular, in a more comprehensive setting, ws and ws0 could negotiate the exchange of policies in an incremental way, or could use the result C of this reasoning activity to perform the second, on-line phase of service interaction we mentioned in the introduction. All this is outside of this picture, and of this article’s scope.
This scenario is inspired to the one described by the
Working Group on Rule Interchange Format [
Before alice buys an item from eShop, alice checks whether her policies and eShop’s policies are compatible, i.e., if they allow a successful transaction. During this process, it turns out that eShop accepts credit card payments, besides other payment methods, and that alice can only pay by credit card; in this case, in order to proceed with the payment, she requires evidence of the shop’s membership to some trusted “Better Business Bureau” (BBB) association. We assume that the shop is able and ready to provide such a piece of evidence. We can thus define eShop’s and alice’s policies as follows: 1In this simplified scenario, we identify alice and eShop with their representative software counterparts which will carry out transactions on their behalf. (shop1) if a customer wishes to buy an item, then (s)he should pay it either by credit card, or by cash, or by cheque; (shop2) if a customer wishes to buy an item, and (s)he has paid it either by credit card, or by cash, or by cheque, then eShop will deliver the item; (shop3) if a customer wishes to receive a certificate about eShop’s membership to the BBB, then the shop will send it; (alice1) if a shop requires that alice pays by credit card, alice expects that the shop provides evidence of its membership to the BBB; (alice2) if a shop requires that alice pays by credit card, and the shop has provided evidence of its membership to the BBB, then alice will pay by credit card;
In this example, we can identify two kinds of policy rules. shop1 and alice1 express requirements, i.e., what is needed in order to proceed with accomplishing some request. shop2, shop3 and alice2 represent the effect of requests, i.e., they tell what has to be expected if some conditions hold and some request is received.
Using this scenario, we want to demonstrate the possibility of reaching an agreement through rules exchange. Besides, we want to show how policies support backward and forward reasoning, in the following way. Backward, pro-active reasoning starts from goals to produce (expectations about) actions or events that should be generated in order to achieve the goals. Forward, reactive reasoning starts from events and is used to generate (expectations about) actions that represent reactions to such events.
In this scenario, the goal of alice interacting with eShop is to obtain an item from eShop. Actions are all the messages exchanged between the two web services.
The steps that we envisage are as follows: 1) alice wants to obtain a device. She knows that she can have it if eShop delivers it to her. Thus, she sends eShop a request, by which she wants to know eShop’s policies regarding the delivery of that device; 2) eShop considers alice’s request, and composes a set of rules related to alice’s request (its policies), possibly deriving/filtering them from a larger set. In this example, the set contains shop1, shop2, and shop3. Once such a set is put together, eShop communicates it to alice; 3) alice reasons on (1) her goal, (2) her own policies (alice1 and alice2), and (3) eShop’s policies. Two are the possible outcomes: • either alice infers that she and eShop can have a successful transaction that satisfies each other’s policies and that achieves her goal, • or alice infers that there is no such a possibility. 4) possibly, at a later point, alice and eShop may engage in a transaction which (hopefully) makes alice achieve her goal.
Points (1) through (3) represent the off-line phase of service discovery/interaction, whereas point (4) represent the actual transaction occurring between alice and eShop. The reasoning involved in (3) is the subject of this article.
In WAVe, the observable behaviour of the web services is represented by events. Since we focus on (explicit) interaction between web services, events always represent exchanged messages.
WAVe considers two types of events: those that one can control and those that one cannot. Typically, from the standpoint of a web service ws, an event such as a message generated by ws himself will fall into the first category, a message that ws is expecting from another fellow web service ws0 will fall instead into the second one. We use two different functors to keep these two categories of messages distinct from each other. Atoms denoted by functor H will stand for events that a web service expects to be producing itself; atoms denoted by functor E will stand for events that a web service is expecting, and over which it does not have any control. Since WAVe is about reasoning on possible future courses of events, both kinds of events represent hypotheses that a web service can make on possibly happening events. The notation is: H(ws, ws0, M, T ), for messages (M ) that a web service ws is expecting to send to ws0 at time T , and E(ws0, ws, M, T ) for messages (M ) expected by ws from ws0 for time T .
Web service specifications in WAVe are relations among
expected events, expressed by an Abductive Logic Program
(ALP). In general, an ALP [
Definition 4.1 (Web service interface behaviour specification): Given a web service ws, its web service interface behaviour specification Pws is an ALP, represented by the triplet
Pws ≡ hKBws, Ews, ICwsi where: • KBws is ws’s Knowledge Base, • Ews is ws’s set of abducible predicates, and • ICws is ws’s set of Integrity Constraints.
KBws is a set of clauses which declaratively specifies pieces of knowledge of the web service. Note that the body of KBws’s clauses may contain E expectations about the behaviour of the web services, as defined above. KBws’s syntax is summarised in Eq. (1). [ Clause ]? Atom ← Cond ExtLiteral [ ∧ ExtLiteral ]? Atom | true | Expect | Constr
E(Atom, Atom, Atom, Atom)
Ews includes E expectations, H events, and predicates not defined in KBws.
ICws ::=
IC ::=
Body ::= BodyLit ::=
Head ::= Disjunct ::=
Expect ::= Event ::= [ IC ]? Body → Head (Event | Expect) [∧BodyLit]? Event | Expect | Atom | Constr Disjunct [ ∨ Disjunct ]? | false (Expect | Event | Constr) [ ∧ (Expect | Event | Constr)]? E(Atom, Atom, Atom, Atom)
H(Atom, Atom, Atom, Atom)
Integrity Constraints (ICs) are forward rules, of the form
Body → Head (Eq. (2)). The Body of ICs is a conjunction
of literals and expected events; the Head instead is a
disjunction of conjunctions of expectations, events and literals, or
false. The syntax of ICws is a modification of the integrity
constraints in the SCIFF language [
Intuitively, the operational behaviour of integrity constraints is similar to forward rules: whenever the body becomes true, the head is also made true.
In this section, we demonstrate web service policy modelling in WAVe by showing the specification of alice and eShop. The first three rules represent eShop’s policies.
→E(alice, eShop, pay(Item, cc), Tcc) ∧ Tcc < Ts ∨E(alice, eShop, pay(Item, cash), Tca) ∧ Tca < Ts ∨E(alice, eShop, pay(Item, cheque), Tch) ∧ Tch < Ts (shop1) IC shop1 says that, if alice expects eShop to deliver an Item, then eShop expects alice to pay by credit card, cash, or cheque, and that payment must be made before delivery.2 In that case, the abducibles in the head are expectations, because they represent actions that should be performed by alice: from eShop’s viewpoint, they can only be expected.
E(eShop, alice, deliver(Item), Ts) ∧ H(alice, eShop, pay(Item, How), Tp) ∧ Tp < Ts (shop2) ∧ How::[cc, cash, cheque]) →H(eShop, alice, deliver(Item), Ts).
2The alternative in the head could alternatively be expressed via a variable with domain: E(alice, eShop, pay(Item, How), T ) ∧ How::[cc, cash, cheque] ∧ T < Ts, where “::” represents a domain constraint. (1) (2)
IC shop2 says that, if alice expects eShop to deliver the Item, and alice has paid for it, then eShop will actually deliver it to alice. In that case, the abducible in the head is an event, because it represents an action that eShop should perform, and therefore it assumes that it will indeed happen (since it is its own responsibility).
→H(eShop, alice, give guarantee, Tg). (shop3) IC shop3 says that if alice expects to receive a guarantee, then eShop will send it. The following two rules represent alice’s policies.
(alice1) →E(eShop, alice, give guarantee, Tg) ∧ Tg < Tp.
IC alice1 says that, if eShop expects alice to pay for an Item by credit card, then alice expects that eShop will have provided a guarantee by the time she pays.
∧ H(eShop, alice, give guarantee, Tg) ∧ Tg < T(palice2) →H(alice, eShop, pay(Item, cc), Tp).
IC alice2 says that, if eShop expects alice to pay for an Item by credit card, and eShop has provided alice with a guarantee, then alice will pay the Item by credit card. Finally, the following clause is part of KBalice have(alice, Item, T ) ← E(eShop, alice, deliver(Item), Td) ∧ Td ≤ T. (alice3) Clause alice3 says that, in order for alice to have an Item at time T , then alice expects eShop to deliver the Item by time T .
VI. DECLARATIVE AND OPERATIONAL SEMANTICS We have assumed that all web services have their own interface behaviour specified in the language of ICs. This interface behaviour could be thought of as an extension of WSDL, that could be used by other fellow web services to reason about the specifications, or to check if inter-operability is possible.
Another approach would be to obtain web services’ interface behaviour through an appropriate request protocol, in which ICs are (interactively) exchanged so that each web service may disclose ad hoc, customised information on demand.
In this work, we make the simplifying assumption that all information regarding the interface behaviour is provided at once. The web service will then try and prove that a fruitful interaction is possible based on what it receives.
The web service initiating the interaction has a goal G, which is a given state of affairs. A typical goal could be to access a resource, to retrieve some information, or to obtain a service from another web service. G will often be an expectation (of obtaining a service, accessing a resource, or gathering information), but in general it can be any conjunction of expectations, CLP constraints, and any other literals, in the syntax of ICws Head Disjuncts (Eq. 2).
The verification of a web service ws about the possibility to achieve a goal G by interacting with another fellow web service ws0 makes use of KBws, ICws, G, and of the information obtained about ws0’s policies, ICws0 (see Fig. 1). The idea is to obtain, through abductive reasoning, a set of expectations about a possible course of events that together with KBws entails ICws ∪ ICws0 and G.
Note that we do not assume that ws knows KBws0 , as the KB is not part of the interface. However, in general integrity constraints can involve predicates defined in the knowledge base. For example, they can contain predicates defining parameters, deadlines, coefficients, etc., or other knowledge only available to ws0. If the interface behaviour provided by ws0 involves predicates defined in KBws0 , unknown to ws, we have two alternatives: • either ws0 provides ws with the necessary information, e.g. with (part of) its KBws0 ; • or ws will have to make assumptions about such unknown predicates.
We take the second option, and consider unknowns that are neither H events nor E expectations as literals that can be abduced, and we keep them in a set Δ. We then have the following two equations that define the set of abductive answers representing possible interaction between ws and ws0 achieving G:
KBws ∪ HAP ∪ EXP ∪ Δ KBws ∪ HAP ∪ EXP ∪ Δ |= G |=
ICws ∪ ICws0 (3) (4) where HAP is a conjunction of H atoms, EXP is a conjunction of E atoms, and Δ a conjunction of abducible atoms.
We can now proceed with defining what kind of interaction is possible/fruitful, given two web services and a goal.
Definition 6.1 (Possible interaction about G): A possible interaction about a goal G between two web services ws and ws0 is an A-minimal set HAP ∪ EXP ∪ Δ such that Eq. 3 and 4 hold.
Among all possible interactions about G, some of them are fruitful, and some are not. An interaction only based on expectations which will not be matched by corresponding events is not a fruitful one: for example, the goal of ws might not have a corresponding event, thus the goal is not actually reached, but only expected. Or, one of the web services could be waiting for a message from the other fellow, which will never arrive, thus undermining the inter-operability.
We select, among the possible interactions, those whose history satisfies all the expectations of both the web services. After the abductive phase, we have a verification phase in which there are no abducibles, and in which the previously abduced predicates H and E are now considered as defined by atoms in HAP and EXP, and they have to match. If among the possible interactions there exists one satisfying
Definition 6.2 (Possible interaction achieving G): Given two web services, ws and ws0, and a goal G, a possible interaction achieving G is a possible interaction about G satisfying Eq. 5.
Intuitively, the “→” implication in Eq. 5 avoids situations in which a web service waits forever for an event that the other web service will never produce. The “←” implication avoids that one web service sends unexpected messages, which in the best case may not be understood (and in the worst scenarios it may lead to faulty, unpredictable behaviour of the parties involved).
A. Operational Semantics
The operational semantics is a modification of the SCIFF
proof-procedure [
T ≡ hR, CS, P SIC, ΔA, PEND, HAP, FULF, VIOLi
The set of expectations EXP is partitioned into the fulfilled
(FULF), violating (VIOL), and pending (PEND)
expectations. The other elements are: the resolvent (R), the abduced
literals that are not expectations (ΔA), the constraint store
(CS), a set of implications, inherited from the IFF [
A classical application of SCIFF is on-line checking of
compliance of agent interaction to protocols. In fact, SCIFF
was initially developed to specify and verify agent interaction
protocols on-the-fly, under the assumption of open agent
environments adopted by other noteworthy agent research
work [
WAVe extends SCIFF and abduces H events as well as expectations. The events history is not taken as input, but all possible interactions are hypothesised. Moreover, in WAVe events not matched by an expectation (which are perfectly acceptable in the multi-agent scenario addressed by SCIFF) cannot be part of a possible interaction achieving the goal.
The two phases in the declarative semantics (generation of possible interactions and their test for conformance) are condensed into one single derivation process, thanks to a new transition adopted in WAVe. The expected transition, symmetrical to fulfilment, labels each H events with an expected flag as soon as an expectation matching it is abduced. At the end of the derivation, H with expected status = false will cause failure.
Given the guarantee, alice will pay by credit card (rule (alice2) fires):
EXP4a ={E(eShop, alice, deliver(device), Ts) ∧ Ts < 50 ∧E(alice, eShop, pay(device, cc), Tcc) ∧ Tcc < Ts ∧E(eShop, alice, give guarantee, Tg) ∧ Tg < Tcc HAP4a ={H(eShop, alice, give guarantee, Tg) ∧ Tg < Tcc ∧H(alice, eShop, pay(device, cc), Tcc) ∧ Tcc < Ts}
(by (alice2))
Having received the payment, eShop’s policy would be to deliver the device:
EXP5a ={E(eShop, alice, deliver(device), Ts) ∧ Ts < 50 ∧E(alice, eShop, pay(device, cc), Tcc) ∧ Tcc < Ts ∧E(eShop, alice, give guarantee, Tg) ∧ Tg < Tcc} HAP5a ={H(eShop, alice, give guarantee, Tg) ∧ Tg < Tcc ∧H(alice, eShop, pay(device, cc), Tcc) ∧ Tcc < Ts ∧H(eShop, alice, deliver(device), Ts) ∧ Ts < 50} (by (shop2))
Otherwise, if the WAVe derivation in a program P for a goal G succeeds with set of expectation EXP ∪ HAP ∪ Δ, we write P `EXP∪HAP∪Δ G.
Soundness and completeness results. WAVe is a
conservative modification of the SCIFF proof-procedure, which
is sound and complete under reasonable assumptions [
We will next demonstrate the operational functioning of verification in WAVe in the alice & eShop scenario.
In the following, the sets EXPN and HAPaN represent a the evolution of alice’s expectations and events as WAVe’s derivation progresses; N is an incremental index. Let g be the following goal of alice’s: g ← have(alice, device, 50). (goal)
EXP0a ={E(eShop, alice, deliver(device), Ts) ∧ Ts < 50} (6) (by (alice3))
To this expectation, eShop will react by expecting a payment: EXP1a ={E(eShop, alice, deliver(device), Ts) ∧ Ts < 50 ∧(E(alice, eShop, pay(device, cc), Tcc) ∧ Tcc < Ts ∨E(alice, eShop, pay(device, cash), Tca) ∧ Tca < Ts ∨E(alice, eShop, pay(device, cheque), Tch) ∧ Tch < Ts) (by (shop1))
Since the expectation containing the payment by cc is the only one which generates an expectation matching a rule of alice ((alice1)), the first expectation among the three payment alternatives is selected (the other branches eventually fail by Eq. 5, because no matching H is abduced). This choice triggers (alice1):
EXP2a ={E(eShop, alice, deliver(device), Ts) ∧ Ts < 50 ∧E(alice, eShop, pay(device, cc), Tcc) ∧ Tcc < Ts ∧E(eShop, alice, give guarantee, Tg) ∧ Tg < Tcc}
(by (alice1))
Then (shop3) fires, and abduces the happening of give guarantee event. We then have:
EXP3a ={E(eShop, alice, deliver(device), Ts) ∧ Ts < 50 ∧E(alice, eShop, pay(device, cc), Tcc) ∧ Tcc < Ts ∧E(eShop, alice, give guarantee, Tg) ∧ Tg < Tcc}
(by (alice1)) HAP3a ={H(eShop, alice, give guarantee, Tg) ∧ Tg < Tcc} (by (shop3)) (7) (8) (9) (10) (11) (12)
Summarising, alice devised the following set of events, which should let her achieve her goal (have the desired device) while respecting both of alice’s and eShop’s policies.
Ca ={H(eShop, alice, give guarantee, Tg) ∧ Tg < Tp ∧H(alice, eShop, pay(device, cc), Tp) ∧ Tp < Ts ∧H(eShop, alice, deliver(device), Ts) ∧ Ts < 50)}
In WAVe, the ICs can be exchanged between web services,
as well as advertised together with their WSDL. For this
reason, a mark-up language is necessary for the rules in ICs.
RuleML [
SCIFF was implemented in SICStus Prolog: SICStus
contains an implementation of the PiLLoW library [
WAVe is a framework intended for describing declaratively the behavioural interface of web services, and for testing operationally the possibility of fruitful interaction between them. WAVe answers the question “does there exist a viable interaction, between two given web services, which achieves a given goal G?” In case of success, WAVe produces a set of expectations about events. WAVe is particularly suitable for highly dynamic environments, in which interoperability is an unknown that has to be checked.
WAVe uses and extends a technology initially developed for
online compliance verification of agent interaction to protocols
[
Another direction of current work relates to the actual use of the answers of WAVe by web services after they manage a successful derivation. In principle, the sequence of events produced by WAVe could be instantiated into a concrete sequence of messages, which will guarantee the achievement of G, under ideal external conditions. But this is true only if the policies disclosed by both web services are a faithful representation of their actual behaviour. This may not be the case, as for example policies may depend on sensible data, and web services may be not allowed to disclose full information to the outside. In that case nothing warrants that the course of action produced by WAVe will be satisfactory for either web service. We might then have to resort to further steps. For example both web services could “formally” agree that a 3See http://lia.deis.unibo.it/research/sciff. certain course of events in an acceptable option, possibly after another mutual verification phase. This is subject of ongoing work. Finally, we are currently investigating the exchange of policies between web services, for which a suitable interaction protocol needs to be devised. We are thinking of specifying such a protocol for exchanging the policies in the same language WAVe uses to specify policies.
In this work, we do not address the problem of reasoning
about ontologies: rather, we focus on the reasoning process,
given the policies of both the peers involved in the interaction.
Many other approaches instead focus on the former issue:
hence our proposal could be seen as a complementary
functionality, that could further improve the discovery process. For
instance, in [
In [
Foster et al. [
The outcome of the reasoning process performed by WAVe
could be intended as a sort of “contract agreement” between
the client and the discovered service, provided that each peer
is tightly bounded to the policies/knowledge bases he/she has
previously published. For example, the dynamical agreement
about contracts (e-contracting) is addressed in [
This work has been partially supported by the MIUR PRIN 2005 projects Specification and verification of agent interaction protocols and Vincoli e preferenze come formalismo unificante per l’analisi di sistemi informatici e la soluzione di problemi reali, and by the MIUR FIRB project Tecnologie Orientate alla Conoscenza per Aggregazioni di Imprese in Internet. for semantic web services workflow composition and enactment. In Sheila A. McIlraith, Dimitris Plexousakis, and Frank van Harmelen, editors, International Semantic Web Conference, volume 3298 of Lecture Notes in Computer Science, pages 425–440. Springer, 2004.