Simulation, Verification and Automated Composition
of Web Services
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