Decomposing the Service Composition Problem

Many approaches to the Web service composition problem benefit from their use of formal methods to guarantee the correctness of the composite services that they produce, but these approaches often require the functionality of the composite service to be specified using one particular formalism (e.g., goal graphs, temporal logic, pre-/post-conditions). As a result, each of these existing approaches falls short in realizing a composite service when the required functionality cannot be fully expressed in the supported formalism. To overcome this problem, we propose a new formal meta-framework that (a) is capable of reusing any existing formalisms and (b) allows the use of functional requirements that are currently not expressible in any one formalism. Our technique assumes that any functional requirement can be decomposed and expressed as a boolean combination of "atomic" requirements, which are representable in at least one existing formalism. Based on this assumption, we use existing methods to identify sets of Web services that conform to the atomic requirements. Our meta-framework then identifies compositions that conform to the overall functional requirement by (a) employing satisfiability techniques to prune the (exponentially large) space of possible compositions and (b) building workable compositions from satisfiable sets of services. As a result, our meta-framework allows for easy and effective memorization of prior composition results, thereby enhancing the efficiency of generating new compositions.