Static Verification of Control and Data in Web Service Compositions

The data exchanged among the web services participating to a composition are clearly very relevant for a correct behavior of the composition. Nevertheless, most of the approaches existing in the literature for the static verification of web service compositions ignore data, or require very small ranges to be associated to the data types. In this paper, we propose an approach for the verification of web service compositions that takes into account the data flows among the component process. The approach exploits abstraction techniques for modeling those aspects of data that are relevant for the correctness of the composition and hiding the aspects that are irrelevant. We show that building the right abstraction corresponds to defining those assumptions on the data manipulations performed by the component services which are crucial for the correctness of the composition.