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 orchestratorsin a timed setting. We suppose to have a network of services and a user?srequest, expressed as a temporal logic formula by which also time constraintsare specified. We define a process algebra operator, called orchestrating operatorthat permits us to manage services in order to satisfy the user?s request. In orderto isolate the behavior that the orchestrator should have to manage the givenservices, we extend the definition of the partial model checking function to theorchestrating operator. By using this function we are able to reduce the startingproblem to a satisfiability one that we solve by exploiting a satisfiability procedurefor temporal logic. In this way we automatically generate an orchestratorprocess as a model of the request.