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

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

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

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.