Process Based Matchmaking of Web Services

The aim of service discovery is to find services that satisfy user requests in a precise and effective manner. An important aspect of service discovery is service matchmaking, which constitutes the mechanism to map appropriate services to requests. The aim of this project is to develop novel service matchmaking methods that especially use internal process models of services. An internal process model precisely describes internal working mechanism of a service. Main idea of our research is to use service process models as primary source of knowledge for service matchmaking. Our matchmaking methods use model checking as the base reasoning mechanism.

We implement and test PBMS under Linux using Python and SPIN. However, it should also run without any problem on other systems.

Stable Version of Process Based Semantic Matchmaker

PBSM v0.1

The Web Service Matchmaking Test Suite

WSTS v0.1

PBSM is implemented in Python and uses SPIN as a model checker. Before using PBSM both of these software packages must be installed to your system and set to classpath.

• Python 2.5.2 or higher http://www.python.org/download
• SPIN 5.2.0 or higher http://spinroot.com/spin/Bin/index.html

The PBSM does not require any installation. Just extract the PBSM package to an appropriate directory and follow the instructions in the next section. As the result of the extraction, there will be one directory called “data”, which involves example service descriptions and example service requests (see Example Definitions for details) and two files called makerepo.py and match.py.

To run PBSM on example services, follow the steps below.

Open a terminal window and change into the directory that you extracted the PBSM package. Then type the following command to create the service repository for the example service descriptions.

$ cd <extraction_directory>
$ ./makerepo data/repository data/claim <destination_directory>

The first parameter points to the repository file that involves path definitions to each service description file. To use your own service descriptions you can edit this file or create a new one.

The second parameter points to the claim file that involves a set of LTL formula, which represents a service consumers request. To create your own service request you can edit this file or create a new one.

The last parameter is the path of the directory of the created repository, which is used by the next instruction.

Now, we have a service repository and a service request. So we are ready to execute the actual matchmaking process. To do this type the following command.

$ ./match -f <destination_directory>/services

By executing this command, you will see the results of the matchmaking process. In the result set, first the matchmaking results of each individual required property for each service is presented. Then a total degree of match value is presented for each service.

There are three requested properties and five services in the examples. The requested properties are:

1. G(payment → hotelVouchered): If there is a payment, the in each state the payment is true, hotelVouchered must also be true.
2. G(payment → payment U hotelVouchered || payment U refunded): The service must be in such a state, either there is a payment and hotelVaucher or the payment is refunded.
3. G(secureConnection → secureConnection U payment || !payment): The payment must be done in a sercure way, or the service must not attempt to receive any payment.

The example services are five different versions of a base hotel reservation service. The first and fifth services satisfy all the required properties. Second, third and fourth services can satisfy only some of the properties. Following images show detailed graphical representations of the service models.