《面向服务的多参与者协调建模验证》由会员分享，可在线阅读，更多相关《面向服务的多参与者协调建模验证（75页珍藏版）》请在金锄头文库上搜索。
1、南京航空航天大学 硕士学位论文 面向服务的多参与者协调建模验证 姓名：闫艳 申请学位级别：硕士 专业：计算机科学与技术 指导教师：黄志球 2010-12 南京航空航天大学硕士学位论文 I 摘 要 可靠的 Web 服务需要借助事务机制来保证， Web 服务的事务处理必需保障多个参与者服务 的执行具有可靠性和一致性，同时可以解决运行时发生的各种异常。由于 Web 服务自身的松散 耦合性、异构性、动态自治等特点，传统的事务处理机制无法直接应用到 Web 服务环境中。 WS-Transaction(WS-Tx)作为 Web 事务处理协议标准， 描述了一个为协调分布式应用程序行为提 供协议支持的可扩展框
2、架，可被用于支持多个业务流程实例的运行。但是该协议仅通过状态转 换图的形式简单描述了单协调器与单参与者之间接收不同消息之后的状态转换，没有给出多参 与者情况下，系统参与者间相互交互的具体描述。同时，形式化方法已成为 Web 服务组合和 事务研究的一个重要研究方向，现有研究工作主要围绕事务的形式化建模和协议的验证上，很 少关注 Web 服务事务协调行为的建模和分析。 本文针对以上问题， 提出基于 WS-Tx 协议的 Web 服务多参与者协调建模验证方法，主要工作如下： (1) 提出了基于 WS-Tx 协议的 Web 服务多参与者协调模型，将参与者间的依赖关系分为： 支配依赖，顺序依赖，并行依赖和
3、选择依赖四种，并针对每一种依赖关系给出了相应的具体协 调策略，完善了 Web 服务多参与者的协调处理； (2) 讨论了如何使用 Pi-演算描述 Web 服务多参与者协调模型。首先分析了 Web 服务多参 与者协调与 Pi-演算元素的映射关系， 然后在此基础上提出针对 BPEL 代码描述的业务流程建立 服务协调模型的方法，最后给出多参与者协调建模的算法描述。 (3) 给出了 Web 服务多参与者协调性质的形式化规约。由安全性和活性两方面对多参与者 协调性质进行讨论和分析， 给出在参与者不同依赖关系下， 安全性和活性性质的相应表现形式。 最后使用计算树逻辑(CTL)对安全性和活性性质进行形式化的描
4、述。 (4) 实现了基于 NuSMV 的 Pi-演算模型验证框架， 并通过机票预订的 Web 服务业务实例对 本文的研究成果进行验证和分析， 验证结果表明本文提出的 Web 服务多参与者协调建模验证方 法是正确可行的。 关键词：关键词：Web 服务，协调，Pi-演算，形式化，模型检验 面向服务的多参与者协调建模验证 II Abstract The reliability of Web services needs transaction. Due to some characteristics of Web services such as autonomy, flexibility, het
5、erogeneous and so on, the traditional transaction semantics and protocols have proven to be inappropriate. As Web Services Transaction standard, WS-Transaction(WS-Tx) specifications define mechanisms for transactional interoperability between Web services domains and provide a means to compose trans
6、actional qualities of service into Web services applications. WS-Tx illustrates the abstract behavior of the protocol between a coordinator and a participant through the abstract state diagram, without giving the specific strategy for a coordinator with multiple participants. Nowadays, describing an
7、d verfying Web services composition and transaction is an important research direction, but current research mainly revolves around the modeling of transaction and protocols, rarely focuses on the behavior of coordination. So in this thesis, an approach of modeling and verifying service-oriented mul
8、ti-participants coordination is proposed, the main research works can be listed as follows. First of all, the multi-participants coordination model of Web services based on WS-Tx protocol is proposed, which divides the dependency relations between participants into: Dominant, Dependent, Concurrent a
9、nd Exclusion. According to each relation, the specific coordination strategy is given; Secondly, considering the formal method, Pi-calculus is adopted, and the mapping table and modeling rules from Web services coordination elements to Pi-calculus syntax are given in this dissertation. On the basis
10、of mapping table between the coordination elements and Pi-calculus elemenets, the pi-calculus model of BPEL process can be obtained with algorithm description; After modeling of multi-participants coordination, safety and liveness are defined respectively in the coordination in terms of the dependen
11、cy relations between the participants, which are then represented in CTL (Computation Tree Logic). Finally, a framework for verification of Pi-calculus based on NuSMV is presented. Besides, an instance of this framework is given, Flight Reservation, the effectiveness and correctness of the proposed
12、approach in this thesis is validated. Keywords: Web Services, Coordination, Pi-calculus, Formalization, Model checking 南京航空航天大学硕士学位论文 V 图表清单 图 1.1 Web 服务多参与者协调的 Pi-演算形式化验证方法.4 图 1.2 论文组织结构 5 图 2.1 协调服务组成结构.8 图 2.2 WS-AT 协调过程 9 图 2.3 BusinessAgreementWithParticipantCompletion 状态转换图11 图 2.4 WS-BA 协调过程
13、.12 图 3.1 Web 服务参与者协调 16 图 3.2 参与者状态转换图.17 图 3.3 协调器状态转换图.19 图 3.4 顺序依赖 21 图 3.5 并行依赖 22 图 3.6 选择依赖 23 图 3.7 顺序依赖关系的 Pi-演算描述.24 图 3.8 并行依赖关系的 Pi-演算描述.25 图 3.9 选择依赖关系的 Pi-演算描述.25 图 3.10 旅行安排应用流图.30 图 4.1 Kripke 结构到计算树的转换.34 图 4.2 三种典型 CTL 运算符.35 图 4.3 安全性视角下参与者状态转换图.37 图 5.1 NuSMV 语言描述文件42 图 5.2 PiTo
14、NuSMV 基本架构.44 图 5.3 文本转换工具基本架构.44 图 5.4 Pi-演算的 EBNF.45 图 5.5 Pi-演算内存结构类图46 图 5.6 SMV 模块程序内存结构类图.47 图 5.7 SMV 模块程序代码生成程序.47 图 5.8 机票预订业务参与者交互图.49 图 5.9 机票预订系统检验结果.53 图 5.10 Pi-演算进程反例代码53 图 5.11 Pi-演算进程反例状态变迁路径54 表 2.1 WS-Coordination 基本概念.7 表 3.1 参与者消息发送与执行结果的对应关系.18 表 3.2 协调器发送消息与参与者发送消息对应关系.19 表 3.
15、3 协调器消息处理器与协调行为对应关系.20 表 3.4 参与者执行情况与消息交互对应关系.21 表 3.5 协调器协调行为与消息交互对应关系.21 面向服务的多参与者协调建模验证 VI 表 3.6 多参与者协调元素与 Pi-演算元素的映射关系.26 表 3.7 旅行安排参与者依赖关系表.31 表 3.8 协调器初始消息处理器的 Pi-演算描述.33 表 4.1 CTL 常用运算符35 表 5.1 NuSMV 系统模型常用模块列表43 南京航空航天大学硕士学位论文 VII 注释表 Web 服务服务(Web Services) 面向服务架构的技术，通过标准的 Web 协议提供服务，目的是 保证不
16、同平台的应用服务可以互操作。 WS-Tx(WS-Transaction) OASIS 的 Web 服务事务技术委员会制定的 Web 服务事务标准， 包括 WS-Coordination、WS-AtomicTransaction 和 WS-BusinessActivity 三部分。 WS-C(Web Services Coordination) Web 服务协调，是可扩展的事务协调框架。 WS-AT(Web Services AtomicTransaction) WS-Tx 定义的一种事务类型：短时间运行的原 子事务，具有“All-or-Nothing”属性。 WS-BA(Web Services BusinessActivity) WS-Tx 定义的一种事务类型： 长时间运行的业务事 务。 Pi-演算演算(Pi-Calculus) 一种移动进程代数，可用于描述并发和动态变化的系统。 CTL(Computation Tree Logic) 计算树逻辑，属于分支时序逻辑。 NuSMV 一种开源的模型检验工具， 用于验证有限状态系统是否满足时序逻辑
