I/O-Automata based formal approach to Web Services Choreography

Abstract

<p><i>Web Services</i> are heterogeneously developed software components invoked over the network viz. the internet. Their main objective is to provide desired outputs in exchange of specified inputs. In the setting of service oriented architecture, Web services play a vital role by allowing computations to be carried out in a distributed fashion via communication between services over the network. This is commonly referred to as <i>Web service composition</i>. This amounts to investigating whether (and how) various services can be utilized in tandem to develop new services desired by a client.</p> <p>A wide range of problems needs to be addressed before service composition can be deployed in practice. These problems range from developing standard language representation for composite services to resolving semantic/vocabulary mismatch between services participating in a composition. In this dissertation we study the problem of synthesis of a <i>mediator/choreographer</i> in Web service composition</p> <p>for a given set of services and a goal. Services and goal are represented using i/o automata.</p> <p>The central theme of our technique relies on generating i/o automata representation of all possible choreographed behaviors of existing services (captured in form of universal service automaton, a concept introduced) and verifying that the goal can be simulated by the universal set of choreographed behaviors. Such a technique is subject to state-space explosion. In light of this, we have developed a tabled logic programming technique which generates and explores compositions in a goal-directed fashion to prove/disprove the existence of choreographer and to infer whether the desired functionality is realizable. We present a prototype implementation and show the practical applicability of our technique using composition problems with the corresponding computational savings in terms of number of states and transitions explored.</p> <p>However, such a centralized choreography mechanism can involve communication/computation overhead that can be reduced through its decentralized realization. With this as motivation, we next</p> <p>study the problem of synthesizing a decentralized choreography strategy that will have an optimum overhead for service composition by developing a set of site-specific choreographers working concurrently to implement a desired goal service. Each communication/computation is quantified by a cost. We develop algorithms that takes as input the existing services, the goal service, the costs and produces as an output a set of site-specific choreographers that optimally realize the goal service using the</p> <p>existing services. The optimization would be different in cases of the goal automaton without loops (workflow) or with loops (certain operations can be repeated any number of times).</p> <p>The contribution of this work lies in the automata-theoretic formal approach to the formulation and the systematic solution of the choreographer synthesis problem as well as formulation of the optimal decentralized choreographer synthesis problem and its solution. The contributions include a methodology for computing cost of automata (with or without cycles), given cost of its transitions, and a generalized solution of the optimized decentralization service composition problem.</p>