IIT Home Page CNR Home Page

Synthesis of Web Services Orchestrators in a Timed Setting

In this paper we present a framework based on partial model checking technique, process algebra and logic for the synthesis of Web Services orchestrators in a timed setting. We suppose to have a network of services and a user’s request, expressed as a temporal logic formula by which also time constraints are specified. We define a process algebra operator, called orchestrating operator that permits us to manage services in order to satisfy the user’s request. In order to isolate the behavior that the orchestrator should have to manage the given services, we extend the definition of the partial model checking function to the orchestrating operator. By using this function we are able to reduce the starting problem to a satisfiability one that we solve by exploiting a satisfiability procedure for temporal logic. In this way we automatically generate an orchestrator process as a model of the request.


, LECTURE NOTES IN COMPUTER SCIENCE (00538S0), 2008

Authors: F. Martinelli, I. Matteucci
IIT authors:

Type: Article in proceedings of international peer-reviewed conference
Da pagina 124 a pagina 138

Activity: Architetture, protocolli e meccanismi di sicurezza per sistemi e servizi distribuiti