Compensation Model For Web Services Transaction Based On π-Calculus

With the rapid development of Internet and Web technologies, it is necessary to integrate and interact heterogeneous applications which are cross-platform, language-independent, and loosely-coupled over the internet. Therefore, it sets a new demand on traditional dis-tributed computing technologies.Web services emerges as a new distributed computing paradigm, and becomes an effective mechanism for data and service integration on the Web.Services composition provides new value-added services by composing and interoper-ating some pre-existing available Web services.To satisfy the requirements of consistence and soundness of operational results among different Web services, it is necessary to support transaction processing. Web services transaction cannot be simply rolled back to recover execution of completed actions as conventional ACID transaction, so we need a compensa-tion mechanism to guarantee data consistency. According to different installation methods of compensations, the compensation models can be divided into two categories:static and dynamic compensation models.The compensations of static models are not dynamically built along with the execution of transactions.Such an approach lacks of flexibility, and is error-prone in a complicated network environment. Many dynamic compensation models are flow-based, namely they adopt centralized coordination mechanisms.Such a model does not provide mobility, so can not describe Web services systems whose structure will change constantly. A lot of compensation models are proposed, but the relationships between them are not clear, and comparison of the expressive power of proposed models has just started.With the development of Web services, using formalism to attack Web services becomes an important research content.π-calculus as a representative mobile process calculi is a suitable tool to study the behavior of interactive services, so it can be naturally applied to modeling and development of Web services.In this thesis, we mainly study the formal analysis of Web services transaction and compensation handling.The major work and contributions of this thesis are as following:1.A general dynamic compensation model for Web services transaction givenExtendingπ-calculus with{P:R}n,n,[P] and a(x)%[λX.Q].P, we present a Exπcalculus as the general dynamic compensation model for Web services transaction. The operational semantics are defined. It supports that inputs can trigger compensation update, so that compensation processes can be dynamically installed along with interac-tions among transactions.We add to Exπmodel a simple type system which guarantee the uniqueness of transactions. In order to illustrate expressiveness and flexibility of our model, a case of Web services is studied. Exπmodel is independent of language and proposal, so we can have a better understanding and grasp of properties about Web services and compensations for transactions.2.Comparison among expressiveness of different compensation modelsWe formally describe the static, parallel dynamic and general dynamic compensa-tion models using extendedπ-calculus. Exπcalculus is simplified, so any action can trigger compensation update. We call the simplified model as Exπ′model.We define the syntax of three categories of the compensation models in an incremental way, and the operational semantics are given. We discuss encoding conditions,and introduce weak bisimilarity and should testing equivalence. We present an encoding from paral-lel dynamic to static compensation calculus, showing that static and parallel dynamic compensation models have the same expressive power. Finally, we prove that there is no encoding of general dynamic into static compensation calculus,demonstrating that Exπ′model is more expressive than static and parallel compensation models.