| Abstract: | To provide an effective service-oriented solution for a given business problem, it is necessary to explore all available options for providing the required functionality while ensuring a flawless data transfer within the composed services. Existing service composition approaches fall short of this ideal, as functional requirements and data mediation are not considered in a unified framework. We propose a service composition framework that addresses both of these aspects by integrating existing techniques in formal methods, service oriented computing and data mediation. Our framework guarantees the correct interaction of services in a composition by verifying certain behavioral constraints, and resolving data mismatches at semantic, syntactic and structural levels, in a unifiedmanner. 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 choreographer. Data models, to detect and resolve data mismatches, are generated using WSDL documents and regular expressions. We also apply our framework to examples adapted from the existing service composition literature that provide strong testimony that the approach can be effectively applied in practical settings. |
