The Formal Specification of Transaction Processing in Web Services by Rewriting Logic
Qi Zheng · Chinese Journal of Computers · 2005
With the popular of the transactions processing in Web Services, it is important to adopt a suitable formal method to specify and verify short and long running transactions in Web services but there is no such mature formal method. This paper proposes a new formal method based on Rewriting Logic related to transaction processing in Web Services. It provides a universal framework for Membrane Calculus by the Rewriting Logic tool called Maude. The rules in Maude are used to describe actions of transactions and compensations are introduced in long running transactions. The authors study a classical example deeply from the literature and provide the whole specification in Maude. So Linear Temporal Logic powered by Rewriting Logic can be used to study the properties of Web transactions in the near future.