πRBT-calculus protocol for Web service long running transactions

Several existing research protocols have already studied long-running transactions within a formal context. Many of them seemed to use concepts which are not suitable. However, there still exists a great challenge to perform transactions in the loosely coupled environment. In this paper we formally model for compositional protocol with the asynchronous π-calculus with compensation and exception handling. We study the practice of π_RBT-calculus, by discussing few paradigmatic examples, its theory, by defining semantics and providing a correct encoding of π_RBT-calculus into asynchronous π-calculus. π_RBT-calculus is a business process modeling protocol and a distinctive feature of the language is its support for compensation. Compensation is an action taken to recover from error or cope with a change of plan, especially when rollback of a process is not possible.