面向服务的多参与者协调建模验证

摘要

可靠的Web服务需要借助事务机制来保证，Web服务的事务处理必需保障多个参与者服务的执行具有可靠性和一致性，同时可以解决运行时发生的各种异常。由于Web服务自身的松散耦合性、异构性、动态自治等特点，传统的事务处理机制无法直接应用到Web服务环境中。WS-Transaction(WS-Tx)作为Web事务处理协议标准，描述了一个为协调分布式应用程序行为提供协议支持的可扩展框架，可被用于支持多个业务流程实例的运行。但是该协议仅通过状态转换图的形式简单描述了单协调器与单参与者之间接收不同消息之后的状态转换，没有给出多参与者情况下，系统参与者间相互交互的具体描述。同时，形式化方法已成为Web服务组合和事务研究的一个重要研究方向，现有研究工作主要围绕事务的形式化建模和协议的验证上，很少关注Web服务事务协调行为的建模和分析。本文针对以上问题，提出基于WS-Tx协议的Web服务多参与者协调建模验证方法，主要工作如下： (1) 提出了基于WS-Tx协议的Web服务多参与者协调模型，将参与者间的依赖关系分为：支配依赖，顺序依赖，并行依赖和选择依赖四种，并针对每一种依赖关系给出了相应的具体协调策略，完善了Web服务多参与者的协调处理； (2) 讨论了如何使用Pi-演算描述Web服务多参与者协调模型。首先分析了Web服务多参与者协调与Pi-演算元素的映射关系，然后在此基础上提出针对BPEL代码描述的业务流程建立服务协调模型的方法，最后给出多参与者协调建模的算法描述。 (3) 给出了Web服务多参与者协调性质的形式化规约。由安全性和活性两方面对多参与者协调性质进行讨论和分析，给出在参与者不同依赖关系下，安全性和活性性质的相应表现形式。最后使用计算树逻辑(CTL)对安全性和活性性质进行形式化的描述。 (4) 实现了基于NuSMV的Pi-演算模型验证框架，并通过机票预订的Web服务业务实例对本文的研究成果进行验证和分析，验证结果表明本文提出的Web服务多参与者协调建模验证方法是正确可行的。

目录

文摘

英文文摘

论文说明:图表目录、注释表

声明

第一章 绪论

第二章 Web服务事务问题描述

第三章 Web服务多参与者协调建模

第四章 Web服务多参与者协调性质规约

第五章 Web服务多参与者协调模型检验

第六章 总结与展望

参考文献

致 谢

在学期间的研究成果及发表的学术论文

附录