Simulation, Verification and Automated Composition

of Web Services

 

Srini Narayanan[1]

srini@ai.sri.com

Sheila McIlraith[2] 

sam@ksl.stanford.edu

 

Copyright is held by the author/owner(s).
WWW2002, May 7-11, 2002, Honolulu, Hawaii, USA.
ACM 1-58113-449-5/02/0005.


ABSTRACT

Web services -- Web-accessible programs and devices – are a key application area for the Semantic Web. With the proliferation of Web services and the evolution towards the Semantic Web comes the opportunity to automate various Web services tasks.  Our objective is to enable markup and automated reasoning technology to describe, simulate, compose, test, and verify compositions of Web services.  We take as our starting point the DAML-S DAML+OIL ontology for describing the capabilities of Web services.  We define the semantics for a relevant subset of DAML-S in terms of a first-order logical language.  With the semantics in hand, we encode our service descriptions in a Petri Net formalism and provide decision procedures for Web service simulation, verification and composition.  We also provide an analysis of the complexity of these tasks under different restrictions to the DAML-S composite services we can describe.  Finally, we present an implementation of our analysis techniques.  This implementation takes as input a DAML-S description of a Web service, automatically generates a Petri Net and performs the desired analysis.  Such a tool has broad applicability both as a back end to existing manual Web service composition tools, and as a stand-alone tool for Web service developers.

Categories and Subject Descriptors

I.2.4 [Artificial Intelligence]:  Knowledge Representation Formalisms and Methods - Representation languages, representations, Predicate logic, Frames and scripts.

General Terms

Algorithms, Design, Standardization, Languages, Theory,  Verification.

Keywords

Semantic Web, DAML, Ontologies, Web Services, Web Service Composition, Distributed Systems, Automated Reasoning.

 

1.  INTRODUCTION

The vision of the semantic Web [4] is to provide computer-interpretable markup of the Web’s content and capability, thus enabling automation of many tasks currently performed by human-beings.  A key application for semantic Web technologies is Web services – Web-accessible programs and devices that will proliferate the Web.   Examples of such Web services include the book-buying service at www.amazon.com, or the travel service at www.travelocity.com.  Semantic markup of the content and capability of Web services – what a service does, how to use it, what its effect will be – will enable easy automation of a variety of reasoning tasks, currently performed manually by human beings, or through arduous hand-coding that enables subsequent automation.  Such tasks include automated Web service discovery, automated invocation, automated interoperation, automated selection and composition, and automated execution monitoring [10,17,23].

 

In this paper, we are motivated by issues related to Web service composition.  Compositions of Web services are created in many different ways.  Many compositions are created manually by the service provider by taking simple Web-accessible programs, such as a form-validation program, or database lookup program, and composing them using typical procedural programming constructs such as if-then-else, sequence or while-loop.   The book-buying service at www.amazon.com is an example of a composite service.

 

A number of software systems are available to facilitate manual composition of programs, and more recently Web services.  Such programs, which include a diversity of workflow tools [1,12], and more recently service composition aids such as BizTalk Orchestration [20] enable a user to manually specify a composition of programs to perform some task.  Most recently, technologies have been proposed that use some form of semantic markup of Web services in order to automatically compose Web services to perform some desired task (e.g., [23,24,3,31]).  Regardless of how the compositions originated, we are interested here in describing and proving properties of these services – to test the system by simulating its execution under different input conditions, to logically verify certain maintenance and safety conditions associated with the service, and to automatically compose services.  In summary, our objective is to enable markup and automated reasoning technology to describe, simulate, automatically compose, test and verify Web service compositions. 

 

Our starting point is the DAML-S ontology for Web services [8,9], which we exploit to provide semantic markup of the content and capabilities of Web services.  In Section 3 we provide a semantics for a portion of the DAML-S language we require to describe compositions of Web services.  In Section 4, we provide an operational semantics using Petri Nets.  In Section 5, we describe decision procedures for Web services simulation, testing, composition, and verification.  We also provide an analysis of the complexity of these tasks under restricted classes of Web service compositions.  Finally in Section 6, we discuss our implementation of a software tool for performing the proposed automated reasoning tasks.  The theory and implementation presented in this paper has broad applicability both as a back end to enhance existing manual composition tools, and as a stand-alone tool for simulation, testing, verification and automated composition of Web services.

 

2.  DAML-S

Critical to the vision of the semantic Web is the provision of a markup language, (or in artificial intelligence (AI) terminology, a knowledge representation language), that has a well-defined semantics to enable unambiguous computer interpretation.  The language must also be sufficiently expressive to describe the properties and capabilities of Web services.  Over the last several years, a number of semantic Web markup languages have been proposed.  These include XML, RDF and RDF(S) and most recently DAML+OIL [13,17,30].  We have adopted DAML+OIL as our content language for describing Web services, and in particular we have adopted DAML-S.

 

DAML+OIL is an AI-inspired description logic-based language for describing taxonomic information. The DAML+OIL language builds on top of XML and RDF(S) to provide a language with both a well-defined semantics and a set of language constructs including classes, subclasses and properties with domains and ranges, for describing a Web domain.  DAML+OIL can further express restrictions on membership in classes and also restrictions on domains and ranges, including cardinality restrictions. 

 

DAML-S is a DAML+OIL ontology for Web services developed by a coalition of researchers[3], under the auspices of the DARPA Agent Markup Language (DAML) program.  The latest release of this ontology is located at [8] and an earlier version is described [9]. The DAML-S ontology describes a set of classes and properties, specific to the description of Web services.  The upper ontology of DAML-S comprises the service profile for describing service advertisements, the process model for describing the actual program that realizes the service, and the service grounding for describing the transport-level messaging information associated with execution of the program.  The service grounding is akin to the Web Service Description Language, WSDL.

 

It is the process model that provides a declarative description of the properties of the Web-accessible programs we wish to reason about. To illustrate the salient features of the DAML-S process model, we use the example of a fictitious book-buying service offered by the Web service provider, Congo Inc.  The Congo example was described in the original release of DAML-S, and its markup can be found at http://www.daml.org/services.  We use a variant of it here for illustration purposes.

 

The process model conceives each program as either an atomic  or composite process. It additionally allows for the notion of a simple process, which is used to describe a view, abstraction or default instantiation of the atomic or composite process to which it expands. We focus here on atomic and composite processes.

 

<daml:Class rdf:ID="Process">

  <daml:unionOf rdf:parseType="daml:collection">

    <daml:Class rdf:about="#AtomicProcess"/>

    <daml:Class rdf:about="#SimpleProcess"/>

    <daml:Class rdf:about="#CompositeProcess"/>

  </daml:unionOf>

</daml:Class>

An atomic process is a non-decomposable Web-accessible program.  It is executed by a single (e.g., http) call, and returns a response.  It does not require an extended conversation between the calling program or agent, and the Web service. 

 

<daml:Class rdf:ID="AtomicProcess">

  <daml:subClassOf rdf:resource="#Process"/>

</daml:Class>

An example of an atomic process is the LocateBook service that takes as input the name of a book and returns a description of the book and its price, if the book is in Congo’s catalogue.

 

<daml:Class rdf:ID="LocateBook">

  <rdfs:subClassOf 

          rdf:resource="&process;#AtomicProcess"/>

</daml:Class>

 

In contrast, a composite process is composed of other composite or atomic processes through the use of control constructs.  These constructs are typical programming language constructs such as sequence, if-then-else, while, fork, etc. that dictate the ordering and the conditional execution of processes in the composition.  We provide a subset of the markup below.

 

<daml:Class rdf:ID="CompositeProcess">

 <daml:intersectionOf

            rdf:parseType="daml:collection">

   <daml:Class rdf:about="#Process"/>

   <daml:Restriction daml:minCardinality="1">

     <daml:onProperty rdf:resource="#composedOf"/>

   </daml:Restriction>

 </daml:intersectionOf>

</daml:Class>

 

<rdf:Property rdf:ID="composedOf">

  <rdfs:domain rdf:resource="#CompositeProcess"/>

  <rdfs:range rdf:resource="#ControlConstruct"/>

</rdf:Property>

 

An example of a composite process might be the Find-n-Buy service that composes LocateBook, together with order request and financial transaction services.  The composition constructs allow for multiple different execution pathways to termination depending, in this case, on whether the book is sold by Congo, is in stock, and whether the user wishes to buy it.

 

Associated with each process is a set of properties. Using a program or function metaphor, a process has parameters to which it is associated.  Two types of parameters are the DAML-S properties input and (conditional) output.

 

<rdf:Property rdf:ID="parameter">

 <rdfs:domain rdf:resource="#Process"/>

 <rdfs:range 

   rdf:resource="http://www.daml.org/... #Thing"/>

 </rdf:Property>

 

<rdf:Property rdf:ID="input">

 <rdfs:subPropertyOf rdf:resource="#parameter"/>

</rdf:Property>

An input for LocateBook might be the name of the book.

<rdf:Property rdf:ID="bookName">

  <rdfs:subPropertyOf

             rdf:resource="&process;#input"/>

  <rdfs:domain rdf:resource="#LocateBook"/>

  <rdfs:range rdf:resource="&xsd;#string"/>[4]

</rdf:Property>

 

Inputs can be mandatory or optional.  In contrast, outputs are generally conditional.  This is important.  For example, when you search for a book in the Congo catalogue, the output may be a detailed description of the book, if Congo carries it, or it may be a “Sorry we don’t carry.” message.  Such outputs are characterized as conditional outputs. We define a conditional output class that describes both a condition and the output based on this condition.  An unconditional output has a zero cardinality restriction on its condition.

 

<rdf:Property rdf:ID="output">

 <rdfs:domain rdf:resource="#parameter"/>

 <rdfs:range rdf:resource="#ConditionalOutput"/>

</rdf:Property>

 

<daml:Class rdf:ID="ConditionalOutput">

 <daml:subClassOf

    rdf:resource="http://www.daml.org/...#Thing"/>

</daml:Class>

 

<rdf:Property rdf:ID="coCondition">

  <rdfs:comment>

     The condition of the conditional output.

  </rdfs:comment>

<rdfs:domain rdf:resource="#ConditionalOutput"/>

 <rdfs:range rdf:resource="#Condition"/>

</rdf:Property>

 

<rdf:Property rdf:ID="coOutput">

  <rdfs:comment>

     The output of the conditional output.

  </rdfs:comment>

  <rdfs:domain rdf:resource="#ConditionalOutput"/>

  <rdfs:range 

    rdf:resource="http://www.daml.org/...#Thing"/>

</rdf:Property>

 

In addition to the program or function metaphor, it is also useful to use an action, event or process metaphor to conceive services.  In this context we can consider services to have the properties precondition and (conditional) effect.  Preconditions and conditional effects are described analogously to inputs and conditional outputs.

 

Preconditions specify things that must be true of the world in order for an agent to execute a service.  A precondition of every process is that the agent knows the input parameters of the process.  For example, one precondition for LocateBook is that the agent Knows(bookName). Stipulating knowledge preconditions pertaining to the input parameters is redundant with the input parameters and are only distinguished as knowledge preconditions in the semantics.  Many Web services that are embodied as programs on the Web only have these preconditions.  At the level of abstraction we are modeling Web services, there are no physical preconditions to the execution of a piece of software on the Web.  In contrast, Web-accessible devices may have many physical preconditions such as bandwidth resources or battery power. 

 

<rdf:Property rdf:ID="precondition"> 

<rdfs:domain rdf:resource="#Process"/>

<rdfs:range 

   rdf:resource="http://www.daml.org/... #Thing"/>

</rdf:Property>

 

Conditional effects characterize the physical side-effects, execution of a Web-service has on the world.  An example of a conditional effect for a BuyBook service might be Own(bookName), when InStock(bookName).  Note that not all services have physical side-effects, in particular, services that are strictly information providing do not.  The DAML-S markup for conditional effects is analogous to that for conditional outputs.

 

3.  THE SEMANTICS OF DAML-S

The DAML-S DAML+OIL ontology provides a set of distinguished classes and properties for describing the content and capabilities of Web services.  The DAML+OIL language in which it is specified has a well-defined semantics, however the expressive power of DAML+OIL is not sufficient to restrict DAML-S to all and only the intended interpretations.  Our objective in this section is to describe a semantics for that portion of DAML-S that is relevant to our work on Web service composition.  In particular, we ascribe a semantics to the notion of atomic and composite processes.

 

One compelling way to do this, as has been done with the semantics of DAML+OIL [13], is to describe DAML-S in a more expressive language, such as first-order logic, and to add a set of axioms to this theory that constrains the models of the theory to all and only the intended interpretations.  Since DAML-S is actually a process modeling language, and its relationship to other process modeling languages is important to interoperability, an even more compelling way to ascribe a semantics to DAML-S is to map it to the US National Institute of Standard’s (NIST) Process Specification Language (PSL) [29].  PSL is a process specification ontology described in the situation calculus, a (mostly) first-order logical language for reasoning about dynamical systems [28].  PSL’s role is to serve as the lingua franca for all business and manufacturing process specification languages. Once the DAML-S language is stabilized, we should easily be able to translate the situation calculus description in Section 3.1 into the PSL ontology [15]. 

 

3.1  From DAML-S to Situation Calculus

The situation calculus language we use [28] is a first-order logical language for representing dynamically changing worlds in which all of the changes are the direct result of named actions performed by some agent.  Situations are sequences of actions, evolving from an initial distinguished situation, designated by the constant S0.  If a(y)[5] is an action and s, a situation, the result of performing a in s is the situation represented by the function do(a,s).  Functions and relations whose values vary from situation to situation, called fluents, are denoted by a predicate symbol taking a situation term as the last argument (e.g., Own(bookName,s)).  Finally, Poss(a,s) is a distinguished fluent expressing that action a is possible to perform in situation s.  

 

The dialect of the situation calculus that we use includes a means of representing knowledge.  In particular, there is a distinguished fluent K(s,s’) that describes the accessibility relation between situations. The notation Knows(f,s) denotes that the formula f is known in situation s (e.g., Knows(Owns(“On the Road”,s))). The notation Kwhether(f,s) is an abbreviation for a formula indicating that the truth value of f is known.  I.e., Kwhether(f,s) = Knows(f,s) Ú Knows(Øf,s).  Finally, the abbreviation Kref(j,s) abbreviates a formula indicating that the functional value of j is known.  The situation calculus is fully described in [28].  We dispense with further details and focus here on the salient features relevant to this paper.

 

Atomic processes in DAML-S are actions a(y) in the situation calculus.  The input parameters of an atomic process are the parameters y of action a. E.g., the atomic process BuyBook is the parameterized action BuyBook(bookName) .

 

Conditional effects and outputs:  The conditional effects of an atomic process are represented in the situation calculus as positive and negative effect axioms of the following form:

     Poss(a,s) Ù gF+(x,a,s)  ® F(x,do(a,s))

     Poss(a,s) Ù gF-(x,a,s)  ®  Ø F(x,do(a,s)).

 

gF(+/-)(x,a,s) contains all the different combinations of actions and conditions that would make fluent F (e.g., Own(bookName,s)) respectively true/false after execution of the action. The following is an example of a positive effect axiom for the BuyBook service with respect to its effect on Own(bookName).  In this example, gF+(x,a,s) is a=BuyBook(bookName) Ù Instock(bookName).

      Poss(a,s) Ù  a=BuyBook(bookName)  Ù  Instock(bookmane,s)

                                                              ® Own(bookName,do(a,s))

 

In our example, we do not illustrate a service that has a negative effect on the fluent Own. To make it more interesting, we add the following.

     Poss(a,s) Ù  a=SellBook(bookName)

                                                        ® Ø Own(bookName,do(a,s))

Although specified as outputs rather than effects in the DAML-S markup, the conditional outputs of an atomic process a are treated as knowledge effects semantically.  This is an important distinction captured in our semantics.  E.g.,

    Poss(a,s)  Ù

        a=LocateBook(bookName)   Ù  Incatalogue(bookName,s)

                                                  ®  Kref(Price(bookName),do(a,s))

 

The output of a service is the information the agent is being told.  Hence the effect will either be a Kref, Kwhether or Knows expression.

 

To address the frame problem representationally [28], effect axioms are compiled into successor state axioms, by appealing to a causal completeness assumption – that the effect axioms for a fluent F characterize all and only actions that cause a change in the (truth) value of fluent F.  Successor state axioms express all the conditions underwhich a fluent value can change.  This ensures that the models of the situation calculus represent all and only the intended interpretations.

 

Successor state axioms, one for each fluent in the language, are of the following form:

     F(x,do(a,s)) º gF+(x,a,s) Ú (F(x,s) Ù  Ø gF-(x,a,s))

I.e., the fluent F is true in do(a,s) iff an action made it true (i.e., gF+(x,a,s)) or it was already true and an action did not make it false (i.e., (F(x,s) Ù  Ø gF-(x,a,s))).

     Own(bookName,do(a,s)) º 

(a=BuyBook(bookName)  Ù Instock(bookName,s))

              Ú  (Own(bookName,s) Ù a ¹ SellBook(bookName))

 

Successor state axioms for knowledge are discussed in [28].

 

Preconditions and inputs:  DAML-S preconditions for an atomic process are represented as well-formed formula in the situation calculus.  Each precondition of an atomic process is expressed as a necessary condition for actions in the situation calculus.

     Poss(a,s)   ® pi

where pi  is a formula relativized to s.  E.g.,

     Poss(CheckGPS(location),s) ® Charged(GPSbattery,s)

 

For multiple preconditions, this generalizes to:

     Poss(a,s)   ® p1 Ù p2 Ù¼Ù pn

 

Just as outputs are treated as knowledge effects, so too are inputs treated as knowledge preconditions semantically.  The agent must know the value of the inputs to the service before it can execute the service. For example, in order to execute LocateBook, the agent must know the values of all the inputs.  Hence for every input ji, of an atomic process a,

     Poss(a,s) ®  Kref(j