Synthesis of Web Services Orchestrators in a Timed Setting

This paper presents a framework based on partial model checking technique, process algebra and logic for the synthesis of Web Services orchestrators in a timed setting, and automatically generates an orchestrator process as a model of the request.

Abstract

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.