Modeling And Analyzing Web Transactions

Web services are the current most promising paradigm to achieve universal interoperability between applications across organizational boundaries. The XML related standards drive services to be published, described and accessed. Among these standards, web services composition has received much interest to support enterprize application integration. Apart from interactions and flow coordination, the task of web service composition requires web transactions to truly increase the consistency and reliability of composite services. Current technologies have been found lacking efficient support for web transactions. Because web transactions have distinct features, such as long-lived, autonomous and interactive, the traditional automatic mechanisms of resource locking and rollback are proved to be inappropriate.In this thesis, we formally address the issue of web transactions. At first, a novel transactional language called t-calculus is proposed to construct web transactions through a series of compensable transactions, using the concept of compensation to recover from failure so as to ensure a relatively relaxed atomicity. This language permits composing compensable transactions in a variety of ways. Not only traditional operators have been extended to support compensation, but several new constructs have been further studied to enhance reliability and flexibility. This language considers the combination of backward and forward recovery techniques. Besides, compensations are treated as compensable transactions too in which a uniform manner is provided to manage both forward and compensating flow.Then we supply this language with semantic models, in which the transactional flow and compensation mechanism are well formalized. Three kinds of semantic models are provided in order to help designers to investigate web transactions from different perspectives. Algebraic semantics is useful for supporting transaction transformation and optimization through a set of algebraic laws. The algebraic semantics is explored based on normal forms, where each compensable transaction can be re-written as a kind of head normal form. Operational semantics provides the foundation of simulation by a set of transition rules. In this semantic model, the equivalence relation of transactions is defined based on the concept of bisimulation which carefully takes compensation into consideration. Denotational semantics studies the transactional behavior on the basis of mathematical models. Here, the denotational semantics is explored relying on the notion of trace pair.These semantic models are not separately defined. In order to avoid semantics conflicts, the linking theory between different semantic models is well built based on the well-known theory of UTP. To be specific, we first define the algebraic model accompanied by a set of algebraic laws for expressing equivalent transactions. Then the operational model is derived from the algebraic model based on a set of well-defined derivation rules. Similarly, the denotational model is derived from the operational model. In addition, all the algebraic laws are then proved to be valid both under the operational and denotational models. By defining semantics in this way, the assurance of correctness of the semantic model itself is further enhanced.At last, the transactional language is expanded by adding data manipulations and interactions so as to specify real case studies. This enriched language is equipped with a clear observation-oriented semantics used to reflect different kinds of behavioral transformation, including data state, communication traces and transactional status. In addition, the refinement relation between compensable transactions is formally explored, which is useful for reasoning properties and supporting stepwise service design.To sum up, by adopting formal method to study web transactions, the opaque points or inconsistencies are cleared and developers are able to understand the compensation mechanism intensively. On the other hand, it provides a foundation for the development of testing or verification tools.