基于重写逻辑的Web服务事务处理形式化描述

Web服务的事务处理研究越来越活跃，对于Web服务中的长、短事务进行形式化描述与验证是很重要的，但目前还没有成熟的方法．该文提出了一种基于重写逻辑的Web服务事务处理形式化描述方法，采用重写逻辑工具Maude，对于描述Web事务的细胞膜演算，给出一个事务处理的通用框架，采用重写逻辑中的规则描述事务的具体活动，并且引入事务补偿机制刻画长事务的运行；并应用该模型形式化描述文中的Web事务经典例子，得到一个可执行的重写逻辑模型，便于以后采用Maude线性时序逻辑分析器进行形式化分析．

The Formal Specification of Transaction Processing in Web Services by Rewriting Logic

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.