Modeling Web service composition using symbolic transition systems

Web services are software entities which provide a set of functionalities that can be accessed over the Web. In general, the valuations of variables appearing in various functions provided by the service are not known before execution. Consequently, to analyze the behavior of a service, all possible valuations need to be considered, making the whole system infinite-state. Against this background, we propose a framework for modeling and composing Web services where desired (goal) and pre-existing (component) services exhibit infinite-state behavior. Our approach finitely represents such services using Symbolic Transition Systems (STSs) which are transition systems augmented with guards over infinite-domain variables. We develop a sound and complete logical approach for identifying the existence of composition of available component-STSs, such that the resulting composition is "simulated" by the goal-STS. In the event that the goal service cannot be realized from the existing components, our technique can also identify the cause for the failure and guide the user to achieve appropriate refinement of the goal specification, thereby paving the way for incremental development of composite services.