D14v0.2. Ontology-based Choreography and Orchestration of WSMO Services

WSMO Working Draft 5 September 2005

This version:

http://www.wsmo.org/TR/d14/v0.2/20050905/

Latest version:

http://www.wsmo.org/TR/d14/v0.2/

Previous version:

http://www.wsmo.org/TR/d14/v0.2/20050702/

Editors:

James Scicluna

Axel Polleres

Dumitru Roman

Cristina Feier

Co-Authors:

Dieter Fensel

This document is also available in non-normative PDF version.
Copyright © 2005 DERI®, All Rights Reserved. DERI liability, trademark, document use, and software licensing rules apply.

Table of contents

• 1. Introduction
• 2. Classical Abstract State Machines
• 2.1 Single-Agent ASM
• 2.1.1. Basic Transition Rules
• 2.1.2. Function Classification
• 2.1.3. Modularization
• 2.2 Multi-Agent ASM
• 3. WSMO Choreography
  • 3.1 State Signature
  • 3.1.1 State
  • 3.1.2 Roles of Concepts and Relations
  • 3.2 Transition Rules
• 4. WSMO Orchestration
• 5. Example
• 6. Future Work
• 7. Conclusions
• Appendix A: Definitions
• Appendix B: Amazon Web Service for Books
• References
• Acknowledgement

1. Introduction

This document describes the Choreography and Orchestration parts of the interface definition of a WSMO service description [Roman et al., 2005]. These parts of a WSMO description describe the behavior of the service from two orthogonal perspectives: communication (how to communicate with the service from the client side such that the service will provide its capability), and respectively collaboration (how the service collaborates with other WSMO services or which goals it needs to resolve in order to achieve its capability). Both views are separate abstractions of the actual implementation of the service.

The Choreography part of a service interface describes the behavior of the service from a client point of view; this definition is in accordance to the following definition given by W3C Glossary [W3C Glossary, 2004]: Web Services Choreography concerns the interactions of services with their users. Any user of a Web service, automated or otherwise, is a client of that service. These users may, in turn, may be other Web Services, applications or human beings.

The orchestration part of a service interface defines how the overall functionality of the service is achieved in terms of the cooperation with other service providers with the actual implementation. It describes how the service works from the provider's perspective (i.e. how a service makes use of other WSMO services or goals in order to achieve its capability). This complies with the W3C definition of Web Service Orchestrations [W3C Working Group]: An orchestration defines the sequence and conditions in which one Web Service invokes other Web Services in order to realize some useful function. That is, an orchestration is the pattern of interactions that a Web Service agent must follow in order to achieve its goal.

The aim of this document is to provide a core conceptual model for describing choreography and orchestration interfaces in WSMO. The state-based mechanism for describing WSMO choreography and orchestration interfaces is based on the Abstract State Machine [Gurevich, 1993] methodology. ASMs have been chosen as the underlying model for the following three reasons:

• Minimality: ASMs provide a minimal set of modeling primitives, i.e., enforce minimal ontological commitments. Therefore, they do not introduce any ad-hoc elements that would be questionable to be included into a standard proposal.
• Maximality: ASMs are expressive enough to model any aspect around computation.
• Formality: ASMs provide a rigid framework to express dynamics.

The remainder of this document is organized as follows: Section 2 provides an Overview of Abstract State Machines. Section 3 provides a core conceptual model for WSMO choreographies, Section 4 presents the conceptual model for WSMO orchestration interfaces, Section 5 provides an example based on the Amazon Web service, and finally Section 6 and Section 7 outline future work and draw conclusions with some remarks.

2. Classical Abstract State Machines

In this section, we give a brief overview of the main concepts of Abstract State Machines. Abstract State Machines (ASMs for short), formerly known as Evolving Algebras [Gurevich, 1995], provide means to describe systems in a precise manner using a semantically well founded mathematical notation. The core principles are the definition of ground models and the design of systems by refinements. Ground models define the requirements and operations of the system expressed in mathematical form. Refinements allow to express the classical divide and conquer methodology for system design in a precise notation which can be used for abstraction, validation and verification of the system at a given stage in the development process.

As described in [Börger & Stärk, 2003], Abstract State Machines are divided into two main categories, namely, Basic ASMs and Multi-Agent ASMs. The former express the behavior of a system within the environment. Multi-Agent ASMs allow to express the behavior of the system in terms of multiple entities that are collaborating to achieve a functionality. The latter can be further divided in two categories: Synchronous and Asynchronous Multi-Agent ASMs, both of which can be of a distributed or non-distributed nature. This classification is depicted in Figure 1 below.

Figure 1: Different types of Abstract State Machines

2.1 Single-Agent ASM

A single-agent ASM (most commonly known as Basic ASM) is defined in terms of a finite set of transition rules which are executed in parallel. It may involve non-determinism as described below.

2.1.1. Basic Transition Rules

f(t₁,...,t_n) := t

More complex transition rules are defined recursively, as follows. (Note that for the sake of clarity, we slightly deviate here from the original syntax used in [Börger & Stärk, 2003].) First, transition rules can be guarded by a Condition as follows:

if Condition then Rules endIf

Here, the Condtion is an arbitrary closed first order formula. Such a guarded transition rule has the semantics that the Rules in its scope are executed in parallel, whenever the condition holds in the current state.

Next, basic ASMs allow some form of universally quantified parallelism by transition rules of the form

forAll Variable with Condition do Rules(Variable) endDo

Here, the Variable is a variable occurring freely in Condition, with the meaning that the Rules[Variable/Value] are executed in parallel for all possible bindings of the Variable to a concrete Value such that the Condition[Variable/Value] holds in the current state. Here, Condition[Variable/Value] (and Rules[Variable/Value], resp.) stand for the condition (or rule, resp.) where each occurence of Variable is replaced by Value.

Similarly, basic ASMs allow for non-deterministic choice by transition rules of the form

choose Variable with Condition do Rules(Variable) endDo

Here, as opposed to the forAll rule, one possible binding of the Variable such that the condition holds is picked non-deterministically by the machine and the Rules are executed in parallel only for this particular binding.

A single ASM execution step is summarized as follows:

1. Unfold the rules, according to the current state and conditions holding in that state, to a set of basic updates.
2. Execute simultaneously all the updates.
3. If the updates are consistent (i.e. no two different updates update the same location with different values, which means that there must not be a pair of updates {(loc,v),(loc,v')} with v ≠ v' ), then the result of execution yields the next state.
4. All locations which are not affected by updates, keep their values.

These steps are repeated until no condition of any rule evaluates to true, i.e. the unfolding yields an empty update set. In case of inconsistent updates, the machine run is either terminated or an error is reported (or both).

2.1.2. Function Classification

ASMs define a classification for functions that can be subject to updates or used in conditions. All functions are either static or dynamic. On the one hand, static functions never change during a run of a machine. Dynamic functions can be classified in four other categories, namely, controlled, monitored (or in), interaction (or shared) and out. Controlled functions are directly updatable by the rules of the machine M only. Thus, they can neither be read nor updated by the environment. Monitored functions can only be updated by the environment and read by machine M and hence constitute the externally controlled part of the state. Shared functions can be read and updated by both the environment and the rules of the machine M. Out functions can be updated but not read by M, but can be read by the environment. Furthermore, ASMs define the so-called derived functions. Theres are functions neither updatable by the machine or the environment but which are defined in terms of other static and dynamic (and derived) functions.

As we will see later, we will base our model of the behavioral aspects of a single service on basic ASMs, operating on dynamic WSMO Ontologies, describing the state of the machine in terms of concepts, relations and their instances, where we can define the ontological axioms in terms of derived functions.

2.1.3. Modularization

In order to structure and modularize ASM descriptions, it is allowed to define modules which take the following form:

RuleName(Variable¹, ..., Variableⁿ) = {Rules}

2.2 Multi-Agent ASM

As described above, there are two types of Multi-Agent ASMs, namely, synchronous and asynchronous. A synchronous Multi-agent ASM consists of a set of basic ASMs each running their own rules and which are synchronized by an implicit global system clock. Such ASMs are equivalent to the set of all single-agent ASMs operating in the global state over the union of their state signatures. The global clock is considered as a step counter. Synchronous ASMs are particularly useful for analysing the interaction between components using precise interfaces over common locations. We consider this model insufficent for the description of the collaboration of Web services.

Asynchronous ASMs consist of a finite number of independent agents each executing a basic or structured ASM in its own local state. The problem which arises in such a scenario is that moves of the different agents cannot be compared due to different data, clocks and duration of execution. Furthermore, the global state is difficult to define since different agents may partially share the same state(s) or may not. The coherence condition for such ASMs is the well-definedness for a relevant portion of a state in which an agent is supposed to perform a step, thus providing the notion of "local" stable view of "the" state in which an agent makes a move.

3. WSMO Choreography

WSMO Choreography deals with interactions of the Web service from the client's perspective. We base the description of the behavior of a single service exposed to its client on the basic ASM model. WSMO Choreography interface descriptions inherit the core principles of such kind of ASMs, which summarized, are: (1) they are state-based, (2) they represents a state by a signature, and (3) it models state changes by transition rules that change the values of functions and relations defined by the signature of the algebra.

In order to define the signature we use a WSMO ontology, i.e. definitions of concepts, their attributes, relations and axioms over these. Instead of dynamic changes of function values as represented by dynamic functions in ASMs we allow the dynamic modification of instances and attribute values in the state ontology. Note that the choreography interface describes the interaction with respect to a single instance of the choreography.

Taking the ASMs methodology as a starting point, a WSMO choreography is state-based and consists of three elements which are defined as follows:

Class wsmoChoreography
      hasNonFunctionalProperties type nonFunctionalProperties
      hasStateSignature type stateSignature
      hasTransitionRules type transitionRules

Non-FunctionalProperties

Non-FunctionalProperties are the same as defined in [Roman et al., 2005] in Section 4.1.

State Signature

The State signature defines the state ontology used by the service together with the definition of the types of modes the concepts and relations may have.

Transition Rules

Transition rules that express changes of states by changing the set of instances.

The remainder of this section describes the main elements of the ASM-based choreography model. Section 3.1 describes the state signature and Section 3.2 describes the transition rules of the ASM.

3.1 State Signature

The signature of the machine is defined by (1) importing an ontology (possibly more than one) which defines the state signature over which the transition rules are executed, (2) a set of statements defining the modes of the concepts (Section 3.1.1) and a set of update functions (Section 3.1.2). The default mode for concepts of the imported ontologies not listed explicitly in the modes statements is static.

Class stateSignature
      hasNonFunctionalProperties type nonFunctionalProperties
      importsOntology type ontology
      hasIn type in
      hasOut type out
      hasControlled type controlled
      hasShared type shared
      hasStatic type static

3.1.1 State

The state for the given signature of a WSMO choreography is defined by all legal WSMO identifiers, concepts, relations and axioms. The elements that can change and that are used to express different states of a choreography, are instances of concepts and relations which are used similar to locations in ASMs. These changes are expressed in terms of creation of new instances or changes of attribute values.

3.1.2 Roles of Concepts and Relations

In a similar way to the classification of locations and functions in ASMs, the concepts and relations of an ontology are marked to support a particular role (or mode). These roles are of five different types:

• static - meaning that the extension of the concept cannot be changed. This is the default for all concepts and relations imported by the signature of the choreography.
• controlled - meaning that the extension of the concept is changed only by a choreography execution.
• in - meaning that the extension of the concept or relation can only be changed by the environment. A grounding mechanism for this item must be provided that implements write access for the environment.
• shared - meaning that the extension of the concept or relation can be changed by the choreography execution and the environment. A grounding mechanism for this item may be provided that implements read/write access for the environment and the service.
• out - meaning that the extension of the concept or relation can only be changed by the choreography execution. A grounding mechanism for this item must be provided that implements read access for the environment.

Since Web services deal with actual instance data, the classification inherits to instances of the respectively classified concepts and relations. That is, instances of controlled concepts and relations can only be created and modified by the choreography, instances of in concepts can only be read by the choreography, instances of out concepts can only be created by the choreography but not read or further modified after its creation. Instances of shared concepts and relations are supposed to be read and written by both the choreography and possibly the environment, i.e. can also be modified after creation. We suppose shared concepts particularly important for groundings alternative to WSDL which do not rely on strict message passing such as semantically enables TupleSpaces (cf. [Fensel D., 2004]), in the future.

3.2 Transition Rules

As opposed to basic ASMs, the most basic form of rules are not assignments, but we deal with basic operations on instance data, such as adding, removing and updating instances to the signature ontology. To this end, we define the atomic update functions to add and delete, as well as update instances, which allow us do add and remove instances to/from concepts and relations and add and remove attribute values for particular instances. In WSMO Choreography, these basic updates are defined as a set of fact modifiers which are of three different types:

• add(fact)
• delete(fact)
• update(fact_old => fact_new), or simply
• update(fact_new)

A fact can be either a membership fact (memberOf), an attribute fact (hasValue) or a combination in the form of a WSML molecule abbreviating conjunctions of membership and attribute facts (cf. [Bruijn et al., 2005]). The add modifier adds a new fact to the state unless it is already present. The delete modifier deletes a fact from the state, if present. The update modifier in its first form marks the combination of deleting an old fact and adding a new one. The second form of update deletes all class memberships or attribute values for a particular attribute and replaces these by the new fact. For a formal definition of the fact modifiers, please refer to Definition 3 of Appendix A.

More complex transition rules are defined recursively, analogous to classical ASMs by if-then, forAll-do and choose-do rules:

if Condition then Rules endIf

forAll Variables with Condition do Rules endDo

choose Variables with Condition do Rules endDo

Compared with basic ASMs, in WSMO choreography the following restrictions apply to Conditions and Variables:

• Variables are WSML variables as defined in [Bruijn et al., 2005]
• A (WSML Full) Condition is a WSML logical expression where all are variables are quantified or bound be enclosing choose or forall constructs
• A WSML Core Condition is a WSML Full logical expression which consists only of molecules built up from memberOf and hasValue atoms and the logical connectives and and or where all unbound variables are existentially quantified

4. WSMO Orchestration

It is envisioned that orchestration should make use of the Multi-Agent asynchronous ASM model to describe the interactions between Web services and Goals. These aspects are still to be further investigated and will be defined in future versions of this document.

5. Example: Amazon Web service for Books

In this section we will present a Web service which enables searching and shopping cart management for books based on the Amazon Web service (Appendix B). This service allows the following operations:

• Searching by title, author(s), keyword(s) and price range
• Searching by a specific ASIN (Amazon Standard Identification Number)
• Cart Creation
• Get a particular cart
• Adding of Items to the cart
• Clearing items off the cart

Listing 3 describes a simple book ontology. To keep our example concise, we will consider that this Amazon Web service handles only book-type items.

namespace {
_"http://www.wsmo.org/ontologies/amazon/bookOntology#",
  dc _"http://purl.org/dc/elements/1.1#",
  dt _"http://www.wsmo.org/ontologies/dateTime#",
  loc _"http://www.wsmo.org/ontologies/location#",
  xsd _"http://www.w3.org/2001/XMLSchema#",
  prs _"http://example.org/owlPersonMediator#",
  wsml _"http://www.wsmo.org/wsml/wsml-syntax#"
}

ontology _"http://www.wsmo.org/ontologies/amazon/amazonOntology"

  nonFunctionalProperties
    dc#title hasValue "Book Ontology"
    dc#creator hasValue {"James Scicluna"}
    dc#subject hasValue {"Book", "Book Buying"}
    dc#description hasValue "Simple Amazon Ontology for Searching and Buying Books"
    dc#publisher hasValue "DERI Innsbruck"
    dc#contributor hasValue {"James Scicluna"}
    dc#date hasValue "2005-08-03"
    dc#type hasValue _"http://www.wsmo.org/2004/d2#ontologies"
    dc#format hasValue "text/html"
    dc#identifier hasValue _"http://www.wsmo.org/ontologies/amazon/book"
    dc#source hasValue _"http://www.wsmo.org/ontologies/amazon/book"
    dc#language hasValue "en-US"
    wsml#version hasValue "$Revision: 1.80 $"
  endNonFunctionalProperties

  usesMediator _"http://example.org/owlPersonMediator"

  concept book
    nonFunctionalProperties
      dc#description hasValue "Defines a book concept"
    endNonFunctionalProperties
    isbn ofType (1) _string
    title ofType (1) _string
    editor impliesType (1 *) prs#person
    author impliesType (1 *) prs#person
    publisher ofType (0 1) publisher
    yearPublished ofType (1) _gyear
    edition ofType (0 1) _integer
    latestPrint ofType (0 1) _date
    keywords ofType _string
    website ofType _iri
    
  concept publisher
    nonFunctionalProperties
      dc#description hasValue "Defines the publisher of a book"
    endNonFunctionalProperties
    name ofType (1) _string
    address impliesType (1 *) loc#address
    phone ofType _int
    email ofType _string
    website ofType _iri

Listing 4 describes the ontology used by the Amazon Web service. This ontology marks also the state of the choreography description for the service.

namespace { _"http://www.wsmo.org/ontologies/amazon/amazonOntology#",
  dc _"http://purl.org/dc/elements/1.1#",
  dt _"http://www.wsmo.org/ontologies/dateTime#",
  loc _"http://www.wsmo.org/ontologies/location#",
  xsd _"http://www.w3.org/2001/XMLSchema#",
  wsml _"http://www.wsmo.org/wsml/wsml-syntax#"
}

ontology _"http://www.wsmo.org/ontologies/amazon/amazonOntology"

  nonFunctionalProperties
    dc#title hasValue "Ontology for a WSMO Amazon Web service"
    dc#creator hasValue {"James Scicluna"}
    dc#subject hasValue {"Book Search", "Book Buying"}
    dc#description hasValue "Simple Amazon Ontology for Searching and Buying Books"
    dc#publisher hasValue "DERI Innsbruck"
    dc#contributor hasValue {"James Scicluna, Jacek Kopecky"}
    dc#date hasValue "2005-06-30"
    dc#type hasValue _"http://www.wsmo.org/2004/d2#ontologies"
    dc#format hasValue "text/html"
    dc#identifier hasValue _"http://www.wsmo.org/ontologies/amazon/amazonOntology"
    dc#source hasValue _"http://keg.cs.tsinghua.edu.cn/ontology/travel"
    dc#language hasValue "en-US"
    wsml#version hasValue "$Revision: 1.80 $"
  endNonFunctionalProperties

  concept price
    nonFunctionalProperties
      dc#description hasValue "Price concept"
    endNonFunctionalProperties
    amount ofType (1) _int
    currencyCode ofType (1) _string
    
  concept item
    nonFunctionalProperties
      dc#description hasValue "An item handled by the Amazon Service"
    endNonFunctionalProperties
    id ofType _string
    image ofType _iri
    customerReviews ofType _string
    lowestNewPrice impliesType (1) price
    price impliesType (1) price

  concept cartItem
    nonFunctionalProperties
      dc#description hasValue "A cart item is described by a specific item and a quantity"
    endNonFunctionalProperties
    item impliesType (1) item
    quantity ofType _int
  
  concept cart
    nonFunctionalProperties
      dc#description hasValue "A cart is represented by an ID and a list of items"
    endNonFunctionalProperties
    id ofType (1) _int
    items impliesType (0 *) cartItem
    totalPrice impliesType (1) price
    
  concept itemSearch
    nonFunctionalProperties
      dc#description hasValue "A request to search for an item"
    endNonFunctionalProperties
    author ofType _string
    keywords ofType _string
    maxPrice impliesType (0 1) price
    minPrice impliesType (0 1) price
    title ofType _string
    
  concept itemLookup
    nonFunctionalProperties
      dc#description hasValue "A request to lookup for an item using an ASIN"
    endNonFunctionalProperties
    id ofType (1 10) _string
    
  concept additionToCart
    nonFunctionalProperties
      dc#description hasValue "A request to add items to a cart"
    endNonFunctionalProperties
    cartId ofType (1) _int
    items impliesType (1 *) cartItem
    
  concept cartGet
    nonFunctionalProperties
      dc#description hasValue "A request to get the Cart"
    endNonFunctionalProperties
    cartId ofType (1) _int

  concept itemContainer
    nonFunctionalProperties
      dc#description hasValue "Contains a list of items"
    endNonFunctionalProperties
    items impliesType item
    
  concept cartItemContainer
    nonFunctionalProperties
      dc#description hasValue "Contains a list of cart items"
    endNonFunctionalProperties
    items impliesType cartItem
    
  concept cartClearRequest
    nonFunctionalProperties
      dc#description hasValue "Request to clear the cart"
    endNonFunctionalProperties
    cartId ofType (1) _int

Listing 5 below describes the capability of Web service. This is captured by describing what the service is expecting (precondition) and by what it will produce (postcondition).

namespace { _"http://www.wsmo.org/webServices/amazonWS#",
  dc _"http://purl.org/dc/elements/1.1#",
  xsd _"http://www.w3.org/2001/XMLSchema#",
  am  _"http://www.wsmo.org/ontologies/amazon/amazonOntology#",
  wsml _"http://www.wsmo.org/wsml/wsml-syntax#"
}

webService _"http://www.wsmo.org/webServices/amazonWS"
  nonFunctionalProperties
    dc#title hasValue "WSMO for Amazon"
    dc#creator hasValue "James Scicluna"
    dc#subject hasValue {"Book", "Book Searching", "Book Buying"}
    dc#description hasValue "WSMO Web service for Book searching  and ordering for amazon"
    dc#publisher hasValue "DERI Innsbruck"
    dc#contributor hasValue {"James Scicluna","Jacek Kopecky", "Axel Polleres"}
    dc#date hasValue "2005-06-30"
    dc#type hasValue _"http://www.wsmo.org/2004/d2#webservice"
    dc#format hasValue "text/html"
    dc#identifier hasValue _"http://www.wsmo.org/webServices/amazonWS"
    dc#source hasValue _"http://www.wsmo.org/webServices/amazonWS"
    dc#language hasValue "en-US"
    dc#relation hasValue {
      _"http://www.wsmo.org/ontologies/amazon/amazonOntology",
      _"http://soap.amazon.com/schemas2/AmazonWebServices.wsdl"
    }
    dc#coverage hasValue "ID:7029392 Name:World"
    wsml#version hasValue "$Revision: 1.80 $"
    wsml#endpointDescription hasValue 
    _"http://webservices.amazon.com/AWSECommerceService/2005-03-23#wsdl.service(AWSECommerceService)"
  endNonFunctionalProperties

capability amazonWSCapability  
  nonFunctionalProperties
    dc#description hasValue 
    "The Amazon service offers:
     - Searching for Books with data related to title, author, key-words and price range
     - Lookup books with ASIN (Amazon Standard Identification Number)
     - Cart Management (Creation, Adding Items and Clearing)"
  endNonFunctionalProperties

  sharedVariables {?id, ?author, ?title, ?keywords, ?minPrice, ?maxPrice, ?cartId, ?newCartItems, ?cartItems}

  precondition
      nonFunctionalProperties
           dc#description hasValue 
           "The Amazon service handles requests for:
            - Searching request
            - Lookup request
            - Request to add items to a cart"
      endNonFunctionalProperties
      definedBy
        //A search by keywords
        ?searchRequest[
          title hasValue ?title
          author hasValue ?author
          keywords hasValue ?keywords
          minPrice hasValue ?minPrice
          maxPrice hasValue ?maxPrice
        ] memberOf am#itemSearch or
        //A search by ID
        ?lookupRequest[
          asin hasValue ?id
        ] memberOf itemLookupRequest or
        //A request to get the cart
        ?cartRequest[
          cartId hasValue ?cartId
        ] memberOf am#cartGet or
        //A request to create a cart
        ?cartCreateRequest[
          items hasValue ?cartItems
        ] memberOf am#cartItemContainer or
        //A request to add items to a cart
        ?addRequest[
          cartId hasValue ?cartId
          items hasValue ?newCartItems
        ] memberOf am#additionToCart or
        //A request to clear the cart
        ?clearRequest[
          cartId hasValue ?id
        ].

  postcondition
      nonFunctionalProperties
          dc#description hasValue "
           The Service can return:
            - a list of searched items
            - a cart"
      endNonFunctionalProperties
      definedBy
        //a container is returned for a search request
        ?container[
          items hasValue ?item
        ] memberOf am#itemContainer and
        ?item[
          bookItem hasValue ?book
          price hasValue ?price
        ] memberOf am#item and
        ?book[
          title hasValue ?title
          author hasValue ?author
          keywords hasValue ?keywords
        ] memberOf bk#book and
        ?price <= ?maxPrice and
        ?price >= ?minPrice or
        //a container is also returned for a search by ID
        ?container[
          items hasValue ?item
        ] memberOf am#itemContainer and
        ?item[
          id hasValue ?id
        ] memberOf am#item or
        //A cart is returned after a request for creation
        ?cart[
          items hasValue ?items
        ] memberOf am#cart or
        //A cart is returned if it is requested by its ID
        ?cart[
          cartId hasValue ?cartId
        ] memberOf am#cart or
        //A cart is returned if new items are added to it
        ?cart[
          cartId hasValue ?cartId
          items hasValue ?newCartItems
        ] memberOf am#cart

Listing 6 describes the choreography of the Web service. The state signature defines the state of the choreography by importing the relevant amazon ontology. The concepts which serve as input and output to and from the service are marked as in and out respectively in the state signature. Note that Listing 6 and Listing 7 are assumed to be in the same namespace as for Listing 5.

interface amazonWSInterface
  choreography amazonChoreography
    stateSignature
      importsOntology _"http://www.wsmo.org/ontologies/amazon/amazonOntology"
      
      in
        am#itemSearch withGrounding 
            _"http://webservices.amazon.com/AWSECommerceService/2005-03-23#wsdl.interfaceMessageReference(AWSECommerceServicePortType/ItemSearch/In)",
        am#itemLookupRequest withGrounding 
            _"http://webservices.amazon.com/AWSECommerceService/2005-03-23#wsdl.interfaceMessageReference(AWSECommerceServicePortType/ItemLookup/In)",
        am#addToCartRequest withGrounding 
            _"http://webservices.amazon.com/AWSECommerceService/2005-03-23#wsdl.interfaceMessageReference(AWSECommerceServicePortType/CartAdd/In)",
        am#cartClearRequest withGrounding 
            _"http://webservices.amazon.com/AWSECommerceService/2005-03-23#wsdl.interfaceMessageReference(AWSECommerceServicePortType/CartClear/In)",
        am#cartItemContainer withGrounding 
            _"http://webservices.amazon.com/AWSECommerceService/2005-03-23#wsdl.interfaceMessageReference(AWSECommerceServicePortType/CartCreate/In)"
        
      out
        am#itemContainer withGrounding {
          _"http://webservices.amazon.com/AWSECommerceService/2005-03-23#wsdl.interfaceMessageReference(AWSECommerceServicePortType/ItemSearch/Out)",
          _"http://webservices.amazon.com/AWSECommerceService/2005-03-23#wsdl.interfaceMessageReference(AWSECommerceServicePortType/ItemLookup/Out)"
        },
        
        am#cart withGrounding {
          _"http://webservices.amazon.com/AWSECommerceService/2005-03-23#wsdl.interfaceMessageReference(AWSECommerceServicePortType/CartGet/Out)",
          _"http://webservices.amazon.com/AWSECommerceService/2005-03-23#wsdl.interfaceMessageReference(AWSECommerceServicePortType/CartAdd/Out)",
          _"http://webservices.amazon.com/AWSECommerceService/2005-03-23#wsdl.interfaceMessageReference(AWSECommerceServicePortType/CartCreate/Out)",
          _"http://webservices.amazon.com/AWSECommerceService/2005-03-23#wsdl.interfaceMessageReference(AWSECommerceServicePortType/CartClear/Out)"
        }

The transitions are described in Listing 6 and are expressed as forall-do since the web service handles multiple instances from different requests.

    transitionRules rules
    
      /*
       * Search by keywords, author, title, price range and create a list of items
       */
      forAll {?searchRequest} with (?searchRequest memberOf am#itemSearch) do
        add(_# memberOf itemContainer)
      endForall
      hasCapability
        capability [...]
        
      endCapability
      
      /*
       * Lookup with an ASIN and return a list of items
       */
      forAll{?lookupRequest, ?asinId} with (?lookupRequest[
          id hasValue ?asinId
        ] memberOf am#itemLookupRequest) do
        add(?item[
          asin hasValue ?asinId
        ]memberOf am#itemLookupRequest)
        add(_#[
          items hasValue ?item
        ]memberOf am#itemContainer)
      endForall
      
      /*
       * Creation of a Cart
       */
      forAll{?cartRequest, ?cartId, ?cartItems} with (?cartRequest[
          items hasValue ?cartItems
        ] memberOf am#cartItemContainer) do
        add(?cart[
          cartItems hasValue ?cartItems
        ] memberOf am#cart)
      endForall
      
      /*
       * Get Cart
       */
      forAll{?cartGet, ?cartId, ?cart} with (?cartGet[
          id hasValue ?cartId
        ] memberOf am#cartGet and
        ?cart[
          id hasValue ?cartId
        ] memberOf am#cart) do
        // Here cart should be sent but how?
      endForall
        
      
      /*
       * add Items to a Cart
       */
      forAll {?addRequest, ?id, ?cartItems, ?cart} with (?addRequest[
          cartId hasValue ?id,
          cartItems hasValue ?cartItems
        ] memberOf am#addToCartRequest and
        ?cart[   //We need to check that there's such cart in the state
            cartId hasValue ?id
          ] memberOf am#cart) do
        add(?cart[
            items hasValue ?cartItems //add items to the cart
          ]memberOf am#cart)
      endForall
      
      /*
       * Clear items of a Cart
       */
      forAll {?clearRequest, ?id, ?cart, ?cartItems} with (?clearRequest[
          cartId hasValue ?id
        ] memberOf am#cartClearRequest and
        ?cart[   // We need to check that there's such cart in the state 
                 // and bind an items variable to delete them
            cartId hasValue ?id,
            items hasValue ?cartItems
          ] memberOf am#cart) do
        delete(?cart[items hasValue ?cartItems])
      endForall

6. Future Work

The integration of ASMs with ontologies is not an easy goal to achieve an thus the language and conceptual models should be further defined. The language should be more expressive and more readable in order to identify clearly what is happenning within the machine. Readability can be improved by introducing the notion of modules in ASMs which encapsulate rules in a procedure like construct. Also, the formal semantics for transition rules and ASM runs should be specified.

Orchestration descriptions should address interactions with Goals and Web services using an asynchronous scenario with multi-agent ASMs. Also, a higher level (and more expressive) language should be defined. This would allow easy readablity for Web service designers and more expressivity. Such language should be mappable to the ASM model defined in this document. Furthermore to this, a diagrammatic notation should be deifned in terms of either the above presented model or the higher order language. Such notation may be defined in terms of UML Activity Diagrams and work relating ASMs to this notation is already defined in [Börger & Stärk, 2003] but the usage of these diagrams to the model presented is yet to be investigated.

7. Conclusions

This document presented a core conceptual model for modeling WSMO Choreographies and Orchestrations based on the ASMs methodology. Single-Agent ASMs are used as the base model for choreography interfaces. The state of the machine is an ontology (or possibly a set of ontologies). The types of concepts are marked with in, out, shared, controlled and static definining the role of the particular concept in the machine. Finally, the simplest guarded transitions take the form of if Condition then Updates. Multi-Agent ASMs shall be used as the model for describing interactions between different Web services in the orchestration in order to achieve the required functionality.

Appendix A. Definitions

Definition 1: Basic WSMO Choreography

The basic WSMO Choreography is deifned by a set of Non-Functional Properties as defined in [De Bruijn et al., 2005] Section 2.2.3, a signature Σ and a set of transition rules Rule.

Definition 2: State Signature

The state signature å is defined by a set of WSMO state ontologies O and a set of Role definitions. The set of ontologies define the state onto which the conditions of the transition rules are evaluated and also onto which the updates are performed. The Role definitions mark concepts with in, out, shared, controlled or static which are "inherited" by variables and instances which are a member of the particular concept.

The state signature description is identified by an IRI followed by a header and role declarations. The state ontology (or ontologies) are declared via the importsOntology statement as part of the header. Roles are of two main categories, namely, grounded and un-grounded. The former are of type in, out and shared and the rest are static and controlled as defined below.

Definition 3: Rule

The current grammar presents three types of rules, namely, if-then, forall-do, choose-do and update-rule. Rules can also have attached to them capability footers whch describe the assumptions, preconditions, postconditions and effects of a single rule. Note that the choose-do has not yet been presented in the conceptual model of the current version of Choreography.

The rules "if", "choose" and "forall" allow to specify nested rules and the 'terminating' rule is an update-rule. The latter defines three types of modifiers, namely, add, delete and update and are defined as follows:

Facts can be of two different natures, namely membership facts (a memberOf b) and attribute facts (a[attr hasValue val] ). It is allowed also to specify multiple facts in a single modifier. In such case, there are two ways of specifying a membership fact which includes attribute facts, namely, a memberOf b[attr_fact_list] or a[attr_fact_list] memberOf b, the latter being the preferred one.

Notice that fact-update is only used for the update modifier since in such case, the old facts to be deleted and the new facts to be added can be specified.

Definition 4: Logical Expressions in basic WSMO Choreography

Conditions in the basic WSMO choreography are restricted from WSML-Core as defined in [De Bruijn et al., 2005] Section 3.6. For the sake of clarity, we will use the same notational symbols.

Definition 4.1: A vocabulary V of a WSML Language L(V) for logical expressions in choreography descriptions consists of the following:

• A set of Identifiers V_ID
• A set of object constructors V_O ⊆ V_ID
• A set of function symbols V_F⊆ V_O
• A set of datatype wrappers V_D⊆ V_O
• A set of data values V_DV ⊆ V_O which encompasses all string, integer and decimal values.
• A set of anonymous identifiers V_A⊆ V_Oof the form _#, _#1, _#2 etc.
• A set of concept identifiers V_C ⊆ V_ID
• A set of instance identifiers V_I⊆ V_ID
• A set of relation identifiers V_R⊆ V_ID
• A set of variable identifiers V_V⊆ V_IDof the form ?x

The following logical connectives are allowed: and, or, forAll, exists together with the auxilliary symbols '(', ')', '[', ']', ',', memberOf and hasValue.

Definition 4.2: Given the vocabulary V, the set of terms Term(V) in WSML is defined as follows:

• Any f ∈ V_O is a term
• Any v∈ V_v is a term
• If f ∈ V_F and t₁,...,t_n are terms, then f(t₁,...,t_n) is a term
• If f ∈ V_DV and d_v1,...,d_vn are in {V_DV ∪ V_V } terms, then f(d_v1,...,d_vn) is a term

Definition 4.3: Given a set of terms Term(V), the set of atomic formulae in L(V) is defined as follows:

Let:

• γ ∈ V_C , Γ be either an identifier in V_C or a list of identifiers in V_C
• φ ∈ V_I ψ be either an identifier in V_I or a list of identifiers in V_I
• Val be either a data value or a list of data values
• p ∈ V_RA such that V_RA is the set of Abstract Attributes
• s ∈ V_RC such that V_RC is the set of Concrete Attributes

The set of atomic formulae in L(V) is defined as follows:

• φ memberOf Γ is an atomic formula in L(V)
• φ[p hasValue ψ] is an atomic formula in L(V)
• φ[s hasValue Val ] is an atomic formula in L(V)

Similarly to WSML-Core logical expressions, only ground facts are allowed.

Let Var₁, Var₂, ... Var_k be arbitrary WSML variables. We call molecules of the form Var_i memberOf G as a-molecules , and molecules of the form, Var_i [ p hasValue Var_k] and Var_i[p hasValue {Var_k1, Var_k2, ...Var _kl}] as b-molecules , respectively. Thus, if an a-molecule is a formula F1 and a b-molecule is also a formula F2, then:

• F1, F2 are also a formula in L(V)
• F1 and F2 is a formula in L(V)
• F1 or F2 is a formula in L(V)

Appendix B. Amazon Web Service for Books

<?xml version="1.0" encoding="UTF-8"?>
<definitions xmlns="http://schemas.xmlsoap.org/wsdl/" 
  xmlns:soap="http://schemas.xmlsoap.org/wsdl/soap/" 
  xmlns:xs="http://www.w3.org/2001/XMLSchema" 
  xmlns:tns="http://webservices.amazon.com/AWSECommerceService/2005-03-23" 
  targetNamespace="http://webservices.amazon.com/AWSECommerceService/2005-03-23">
    <types>
  <xs:schema targetNamespace="http://webservices.amazon.com/AWSECommerceService/2005-03-23" 
    xmlns:xs="http://www.w3.org/2001/XMLSchema" 
    xmlns:tns="http://webservices.amazon.com/AWSECommerceService/2005-03-23" elementFormDefault="qualified">
    <xs:complexType name="ItemSearchRequest">
      <xs:sequence>
        <xs:element name="Author" type="xs:string" minOccurs="0"/>
        <xs:element name="Keywords" type="xs:string" minOccurs="0"/>
        <xs:element name="MaximumPrice" type="xs:nonNegativeInteger" minOccurs="0"/>
        <xs:element name="MinimumPrice" type="xs:nonNegativeInteger" minOccurs="0"/>
        <xs:element name="Title" type="xs:string" minOccurs="0"/>
      </xs:sequence>
    </xs:complexType>
    <xs:complexType name="ItemLookupRequest">
      <xs:sequence>
        <xs:element name="ItemId" type="xs:string" minOccurs="0" maxOccurs="unbounded"/>
      </xs:sequence>
    </xs:complexType>
    <xs:complexType name="CartGetRequest">
      <xs:sequence>
        <xs:element name="CartId" type="xs:string" minOccurs="0"/>
      </xs:sequence>
    </xs:complexType>
    <xs:complexType name="CartAddRequest">
      <xs:sequence>
        <xs:element name="CartId" type="xs:string" minOccurs="0"/>
        <xs:element name="Items" minOccurs="0">
          <xs:complexType>
            <xs:sequence>
              <xs:element name="Item" minOccurs="0" maxOccurs="unbounded">
                <xs:complexType>
                  <xs:sequence>
                    <xs:element name="ASIN" type="xs:string" minOccurs="0"/>
                    <xs:element name="Quantity" type="xs:positiveInteger" minOccurs="0"/>
                  </xs:sequence>
                </xs:complexType>
              </xs:element>
            </xs:sequence>
          </xs:complexType>
        </xs:element>
      </xs:sequence>
    </xs:complexType>
    <xs:complexType name="CartCreateRequest">
      <xs:sequence>
        <xs:element name="Items" minOccurs="0">
          <xs:complexType>
            <xs:sequence>
              <xs:element name="Item" minOccurs="0" maxOccurs="unbounded">
                <xs:complexType>
                  <xs:sequence>
                    <xs:element name="ASIN" type="xs:string" minOccurs="0"/>
                    <xs:element name="Quantity" type="xs:positiveInteger" minOccurs="0"/>
                  </xs:sequence>
                </xs:complexType>
              </xs:element>
            </xs:sequence>
          </xs:complexType>
        </xs:element>
        <xs:element name="ResponseGroup" type="xs:string" minOccurs="0" maxOccurs="unbounded"/>
      </xs:sequence>
    </xs:complexType>
    <xs:complexType name="CartClearRequest">
      <xs:sequence>
        <xs:element name="CartId" type="xs:string" minOccurs="0"/>
      </xs:sequence>
    </xs:complexType>
    <xs:element name="ItemSearchResponse">
      <xs:complexType>
        <xs:sequence>
          <xs:element ref="tns:Items" minOccurs="0" maxOccurs="unbounded"/>
        </xs:sequence>
      </xs:complexType>
    </xs:element>
    <xs:element name="ItemLookupResponse">
      <xs:complexType>
        <xs:sequence>
          <xs:element ref="tns:Items" minOccurs="0" maxOccurs="unbounded"/>
        </xs:sequence>
      </xs:complexType>
    </xs:element>
    <xs:element name="CartGetResponse">
      <xs:complexType>
        <xs:sequence>
          <xs:element ref="tns:Cart" minOccurs="0" maxOccurs="unbounded"/>
        </xs:sequence>
      </xs:complexType>
    </xs:element>
    <xs:element name="CartAddResponse">
      <xs:complexType>
        <xs:sequence>
          <xs:element ref="tns:Cart" minOccurs="0" maxOccurs="unbounded"/>
        </xs:sequence>
      </xs:complexType>
    </xs:element>
    <xs:element name="CartCreateResponse">
      <xs:complexType>
        <xs:sequence>
          <xs:element ref="tns:Cart" minOccurs="0" maxOccurs="unbounded"/>
        </xs:sequence>
      </xs:complexType>
    </xs:element>
    <xs:element name="CartClearResponse">
      <xs:complexType>
        <xs:sequence>
          <xs:element ref="tns:Cart" minOccurs="0" maxOccurs="unbounded"/>
        </xs:sequence>
      </xs:complexType>
    </xs:element>
    <xs:element name="Items">
      <xs:complexType>
        <xs:sequence>
          <xs:element ref="tns:Item" minOccurs="0" maxOccurs="unbounded"/>
        </xs:sequence>
      </xs:complexType>
    </xs:element>
    <xs:element name="Cart">
      <xs:complexType>
        <xs:sequence>
          <xs:element name="CartId" type="xs:string"/>
          <xs:element ref="tns:CartItems" minOccurs="0"/>
        </xs:sequence>
      </xs:complexType>
    </xs:element>
    <xs:element name="Item">
      <xs:complexType>
        <xs:sequence>
          <xs:element name="ASIN" type="xs:string"/>
          <xs:element name="MediumImage" type="tns:Image" minOccurs="0"/>
          <xs:element ref="tns:CustomerReviews" minOccurs="0"/>
        </xs:sequence>
      </xs:complexType>
    </xs:element>
    <xs:element name="CartItems">
      <xs:complexType>
        <xs:sequence>
          <xs:element name="SubTotal" type="tns:Price" minOccurs="0"/>
          <xs:element name="CartItem" type="tns:CartItem" maxOccurs="unbounded"/>
        </xs:sequence>
      </xs:complexType>
    </xs:element>
    <xs:complexType name="CartItem">
      <xs:sequence>
        <xs:element name="CartItemId" type="xs:string"/>
        <xs:element name="ASIN" type="xs:string" minOccurs="0"/>
        <xs:element name="Quantity" type="xs:string"/>
        <xs:element name="Title" type="xs:string" minOccurs="0"/>
        <xs:element name="Price" type="tns:Price" minOccurs="0"/>
                          <xs:element name="ItemTotal" type="tns:Price" minOccurs="0"/>
      </xs:sequence>
    </xs:complexType>
    <xs:complexType name="Price">
      <xs:sequence>
        <xs:element name="Amount" type="xs:integer" minOccurs="0"/>
        <xs:element name="CurrencyCode" type="xs:string" minOccurs="0"/>
      </xs:sequence>
    </xs:complexType>
    <xs:element name="ItemAttributes">
      <xs:complexType>
        <xs:sequence>
          <xs:element name="Author" type="xs:string" minOccurs="0" maxOccurs="unbounded"/>
          <xs:element name="ISBN" type="xs:string" minOccurs="0"/>
          <xs:element name="ListPrice" type="tns:Price" minOccurs="0"/>
          <xs:element name="Title" type="xs:string" minOccurs="0"/>
        </xs:sequence>
      </xs:complexType>
    </xs:element>
  </xs:schema>
    </types>
    <message name="ItemSearchRequestMsg">
      <part name="body" element="tns:ItemSearch"/>
    </message>
    <message name="ItemSearchResponseMsg">
      <part name="body" element="tns:ItemSearchResponse"/>
    </message>
    <message name="ItemLookupRequestMsg">
      <part name="body" element="tns:ItemLookup"/>
    </message>
    <message name="ItemLookupResponseMsg">
      <part name="body" element="tns:ItemLookupResponse"/>
    </message>
    <message name="CartGetRequestMsg">
      <part name="body" element="tns:CartGet"/>
    </message>
    <message name="CartGetResponseMsg">
      <part name="body" element="tns:CartGetResponse"/>
    </message>
    <message name="CartAddRequestMsg">
      <part name="body" element="tns:CartAdd"/>
    </message>
    <message name="CartAddResponseMsg">
      <part name="body" element="tns:CartAddResponse"/>
    </message>
    <message name="CartCreateRequestMsg">
      <part name="body" element="tns:CartCreate"/>
    </message>
    <message name="CartCreateResponseMsg">
      <part name="body" element="tns:CartCreateResponse"/>
    </message>
    <message name="CartClearRequestMsg">
      <part name="body" element="tns:CartClear"/>
    </message>
    <message name="CartClearResponseMsg">
      <part name="body" element="tns:CartClearResponse"/>
    </message>
    <portType name="AWSECommerceServicePortType">
       <operation name="ItemSearch">
           <input message="tns:ItemSearchRequestMsg"/>
           <output message="tns:ItemSearchResponseMsg"/>
       </operation>
       <operation name="ItemLookup">
           <input message="tns:ItemLookupRequestMsg"/>
           <output message="tns:ItemLookupResponseMsg"/>
       </operation>
       <operation name="CartGet">
           <input message="tns:CartGetRequestMsg"/>
           <output message="tns:CartGetResponseMsg"/>
       </operation>
       <operation name="CartAdd">
           <input message="tns:CartAddRequestMsg"/>
           <output message="tns:CartAddResponseMsg"/>
       </operation>
       <operation name="CartCreate">
           <input message="tns:CartCreateRequestMsg"/>
           <output message="tns:CartCreateResponseMsg"/>
       </operation>
       <operation name="CartClear">
           <input message="tns:CartClearRequestMsg"/>
           <output message="tns:CartClearResponseMsg"/>
       </operation>
    </portType>
    <binding name="AWSECommerceServiceBinding" type="tns:AWSECommerceServicePortType">
       <soap:binding style="document" transport="http://schemas.xmlsoap.org/soap/http"/>
       <operation name="ItemSearch">
           <soap:operation soapAction="http://soap.amazon.com"/>
           <input>
         <soap:body use="literal"/>
           </input>
           <output>
         <soap:body use="literal"/>
           </output>
       </operation>
       <operation name="ItemLookup">
           <soap:operation soapAction="http://soap.amazon.com"/>
           <input>
         <soap:body use="literal"/>
           </input>
           <output>
         <soap:body use="literal"/>
           </output>
       </operation>
       <operation name="CartGet">
           <soap:operation soapAction="http://soap.amazon.com"/>
           <input>
         <soap:body use="literal"/>
           </input>
           <output>
         <soap:body use="literal"/>
           </output>
       </operation>
       <operation name="CartCreate">
           <soap:operation soapAction="http://soap.amazon.com"/>
           <input>
         <soap:body use="literal"/>
           </input>
           <output>
         <soap:body use="literal"/>
           </output>
       </operation>
       <operation name="CartAdd">
           <soap:operation soapAction="http://soap.amazon.com"/>
           <input>
         <soap:body use="literal"/>
           </input>
           <output>
         <soap:body use="literal"/>
           </output>
       </operation>
       <operation name="CartClear">
           <soap:operation soapAction="http://soap.amazon.com"/>
           <input>
         <soap:body use="literal"/>
           </input>
           <output>
         <soap:body use="literal"/>
           </output>
       </operation>
    </binding>
    <service name="AWSECommerceService">
       <port name="AWSECommerceServicePort" binding="tns:AWSECommerceServiceBinding">
           <soap:address location="http://soap.amazon.com/onca/soap?Service=AWSECommerceService"/>
       </port>
    </service>
</definitions>

      

References

[Börger, 1998] Egon Börger: "High Level System Design and Analysis Using Abstract State Machines", Proceedings of the International Workshop on Current Trends in Applied Formal Method: Applied Formal Methods, p.1-43, October 07-09, 1998

[Börger & Stärk, 2003] Egon Börger and Robert Stärk: "Abstract State Machines: A Method for High-Level System Design and Analysis", Springer-Verlag, 2003

[Bruijn et al., 2005] J. de Bruijn, H. Lausen, R. Krummenacher, A. Polleres, L. Predoiu, M. Kifer, D. Fensel: The Web Service Modeling Language WSML. WSML Final Draft v0.2, 2005. Available from http://www.wsmo.org/TR/d16/d16.1/v0.2/.

[Gurevich, 1993] Yuri Gurevich: "Evolving Algebras 1993: Lipari Guide", Specification and Validation Methods, ed. E. Börger, Oxford University Press, 1995, 9--36.

[Fensel D., 2004] D. Fensel: Triple-space computing: Semantic Web Services based on persistent publication of information. Proc. of IFIP Int'l Conf. on Intelligence in Communication Systems 2004, Bangkok, Thailand, Nov 2004:43-53.

[Kopecky et. al., 2005]J. Kopecky, D. Roman (authors): WSMO Grounding, WSMO deliverable D24.2 version 0.1. available from http://www.wsmo.org/2005/d24/d24.2/v0.1/20050119/

[Roman et al., 2005] D. Roman, H. Lausen, and U. Keller (eds.): Web Service Modeling Ontology (WSMO), WSMO deliverable D2 version 1.1. available from http://www.wsmo.org/TR/d2/v1.2/

[W3C Glossary, 2004] Hugo Haas, and Allen Brown (editors): Web Services Glossary, W3C Working Group Note 11 February 2004, available at http://www.w3.org/TR/ws-gloss/

Acknowledgement