节点文献

基于细胞膜演算的Web服务事务处理形式化描述与验证

The Formal Specification and Verification of Transaction Processing in Web Services by Membrane Calculus

  • 推荐 CAJ下载
  • PDF下载
  • 不支持迅雷等下载工具,请取消加速工具后下载。

【作者】 戚正伟尤晋元

【Author】 QI Zheng-Wei YOU Jin-Yuan (Department of Computer Science and Engineering , Shanghai Jiaotong University , Shanghai 200030)

【机构】 上海交通大学计算机科学与工程系上海交通大学计算机科学与工程系 上海 200030上海 200030

【摘要】 采用细胞膜演算具体分析了当前比较主流的Web服务中原子事务协调协议WS-AT.针对WS-AT协议采用简单的状态转换表和转换图,无法描述协调者和多个参与者的复杂协调活动,采用细胞膜演算给出了其形式化描述,用于规范协调者和参与者的活动,并分析了该协议的活性和安全性,得到了38187个状态.模型检验的实验结果表明,该协议满足稳定性、一致性和非平凡性,而不满足非阻塞性.进而,分析出注册和协调协议混在一起是其不满足非阻塞性的原因.

【Abstract】 It is important to adopt a suitable formal method to specify and verify complex transactions in Web services. The authors have developed a formal method called Membrane Calculus to describe the abstract model in long running transactions. This paper extends Membrane Calculus to analyze the practical atomic transaction commit protocol WS-AT. Due to the simple State Transition Table and Chart, WS-AT can not describe the complex coordination activities between the coordinator and several participants. Membrane Calculus is used to formally specify the behavior of the coordinator and participants and analyze the Safety and Liveness of WS-AT. The Model Checking experiments show that there are 38,187 states in the authors’ model and Stability, Consistency, Non-Triviality are satisfied while Non-Blocking is not. The reason is that WS-AT mixes the registration and coordination protocols.

【基金】 本课题得到国家自然科学基金(60173033);国家“八六三”高技术研究发展计划项;目基金(2004AA104340,2004AA104280)资助
  • 【文献出处】 计算机学报 ,Chinese Journal of Computers , 编辑部邮箱 ,2006年07期
  • 【分类号】TP393.092
  • 【被引频次】18
  • 【下载频次】284
节点文献中: 

本文链接的文献网络图示:

本文的引文网络