Unified management of control flow and data mismatches in web service composition

The two main aspects of the web service composition problem are control flow and data mismatches. Several approaches have been reported in the literature to tackle the former; while the latter, and equally relevant aspect for the correct compositional behavior, has either been ignored or addressed to a very limited extent. This paper describes a formal approach based on model checking, that guarantees the correct interaction of services in a composition by managing control flow and resolving data mismatches at semantic, syntactic and structural levels, in a unified manner. A tableau based algorithm is used to generate and explore compositions in a goal-directed fashion, that proves or disproves the existence of a service orchestrator. Successful synthesis of the orchestrator confirms that the required functionality is realizable. Data models to detect and resolve data mismatches are generated using WSDL documents and regular expressions. Experimental results provide strong testimony that the approach can be effectively applied in a practical setting.