Formal Analysis of Web Service Compositions
Raman Kazhamiakin · 2007
One of the key ideas of Web service technology is the ability to create service compositions by combining pre-existing services using standard languages for the definition of the composition behavior. These compositions often span across the enterprise boundaries, involving various stakeholders with their own requirements and goals into the design process. The ability to detect requirements violations and resolve conflicts in the specifications of the composition behavior has been an important issue in the service-oriented design. This makes the automation of the correctness analysis a challenging research topic for the development of critical and reliable service-based applications. The formal analysis of the Web service compositions has to tackle several problems specific to this domain. First, the service communications are essentially asynchronous and rely on complex and heterogeneous message management systems. Second, the service specifications extensively use complex data structures and operations, often in a non-deterministic and partially defined manner. Third, the correctness of the service-based processes often relies on quantitative properties, especially on time aspects of the execution. These issues, however, are not systematically addressed by the existing approaches, and require specific methods and solutions. In this dissertation we present a formal framework for the analysis of Web service compositions that supports asynchronous interactions and complex data and time flow modelling. The framework relies on a formal model, where (i) services are defined as state transition systems equipped with data and time characteristics; (ii) services are composed using a parametric communication model, which allows for capturing a wide range of messaging systems; (iii) temporal logics are exploited for the specification of behavioral requirements, taking into account also quantitative time aspects. Based on this model we introduce new analysis approaches that deal with issues specific to the Web service domain. We develop a technique to associate with a Web service composition the most adequate communication model, i.e., the one that is sufficient to capture all the behaviors of the composition, while being as efficient as possible in the analysis, and allows for extracting minimal constraints on the underlying implementation. We propose an analysis approach that takes into account the data flow among the component process. The approach exploits abstraction techniques for modeling only relevant data flow aspects. We show that building the right abstraction corresponds to iterative extraction of certain assumptions on the partially defined or even unknown data manipulations performed by the component services. We also present a timed analysis approach that allows for the verification of complex time properties and for the computation of duration bounds where these properties are satisfied, using the duration calculus formalism. These techniques are implemented and integrated in a toolkit that allows for model checking Web service compositions, and are evaluated on a set of case studies.