基于时间自动机的Web服务模型检测-计算机应用技术专业论文.docx

摘 摘 要 摘 摘 要 万方数据 万方数据 – – PAGE IV – 万方数据 摘 要 Web服务技术给企业的应用程序集成带来了方便，但是分布的单个Web服务功能 简单有限，因此有必要将它们进行组合。Web服务的这种组合方式使得各原子服务间 产生了大量复杂的信息交互。为了保障组合Web服务的正确性，有必要对其运行过程 进行检测。模型检测技术以其自动化程度高，在Web服务的形式化验证中倍受关注。 传统的模型检测方法不能保证带有严格时间约束的实时组合Web服务的正确性。 本文将带有时间约束的组合Web服务建模为一组时间自动机，并用基于时间自动机的 模型检测工具验证了组合Web服务实时的时态逻辑特性、组合Web服务中存在的特征 冲突问题及组合Web服务的时态认知逻辑特性。为了系统的研究组合Web服务，还提 出了一种执行代价较小的Web服务组合方法。本文的工作主要体现在以下几个方面： (1)提出了用基于时间自动机的模型检测技术对组合Web服务进行形式化验证的 方法。将组合Web服务建模成一组相互通信的时间自动机，并用UPPAAL模拟其运行 过程，验证其系统的一些实时时态逻辑特性。以两个组合Web服务为例阐述了该验证 过程，并发现其中一个服务存在死锁问题；通过分析死锁产生的路径完善了该服务的 协议，从而消除了死锁。此外，首次采用该技术对组合Web服务的特征冲突问题进行 了分析和检测。发现了在线股票交易系统的特征冲突现象，验证了该服务的特征冲突 属性。 (2)提出了用基于Verics的有界模型检测技术对组合Web服务系统的时态认知逻 辑特性进行验证。将组合Web服务建模成时间自动机，用模型检测工具Verics对其系 统特性进行分析，验证了传统模型检测工具无法检测的时态认知逻辑；以旅游预订票 系统为例阐述了该验证过程。 (3)提出了一种执行代价较小的Web服务反向链组合算法。该方法根据用户的输入 和期望的输出，在兼顾Web服务执行代价的同时，动态生成一个执行代价较小以BPEL 语言描述的Web服务组合方案；该方案考虑了Web服务的组合效率和执行代价，并且 可以采用上述模型检测方法对其进行验证。 关键词：模型检测；时间自动机；时态认知逻辑；特征冲突；Web服务组合. – I – Abstract Although Web services techniques have already brought many conveniences for the integration of enterprise applications, the functionalities of some distributed individual Web services is simple and limited. Therefore, some existing (individual) Web services need to be composed into new Web services, to provide more sophisticated functionalities. Within a composite Web service, some of related atom services may exchange a lot of complex information with each other in the unreliable Internet environment. In order to protect the correctness of Web services, it is necessary to formally verify the implementation of Web services. Thanks to the high automation of model checking technology, it has drawn greater attention on Web services verification. The traditional model checking techniques are mainly based on finite state systems. It is hard to apply them to guaranteeing the correctness of Web services composition with timed constraints. To support timed modeling and verification, we aim to model Web services composition as a n