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

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

作　　者：戚正伟[1] 毛宏燕[1] 尤晋元[1] 

机构地区：[1]上海交通大学计算机科学与工程系,上海200030

出　　处：《计算机学报》2005年第4期661-666,共6页Chinese Journal of Computers

基　　金：国家自然科学基金 (60173033) ;国家"九七三"重点基础研究发展规划项目(2002CB312002) 资助.

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

关 键 词：WEB服务 事务处理 重写逻辑 形式化方法 细胞膜演算 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]