异步Web服务组合分析与验证方法研究

摘要

随着网络技术的迅速发展，面向服务的体系架构(SOA)以其良好的可重用性、松耦合性和互操作性，已成为一种工业界和学术界广泛接受的网络化软件应用模式。Web服务作为SOA的主流实现方式，正逐步成为网络环境中资源封装的标准方式。目前，Web服务正逐步由单一的面向功能向面向业务流程转变，服务周期随之延长，使得同步通信模式的Web服务已无法满足用户需求，而无阻塞的异步Web服务成为研究热点。
　　 由于单个的Web服务提供的功能有限，为了更加充分地利用共享的Web服务构建企业级应用系统，Web服务组合技术变得愈加重要。Web服务组合研究领域的一个重要的问题是如何形式化描述Web服务组合以及如何验证服务组合的正确性。在对Web服务组合的模型进行验证时，不仅要考虑组合服务是否满足功能需求，还需要检查是否存在时间冲突或数据不一致等问题，确保构建高效正确的服务组合。
　　 本文以异步Web服务为研究对象，分析相关时间和数据约束对服务交互的影响，对异步Web服务组合验证进行了深入研究。主要内容包括：(1)从软件体系结构的角度研究Web服务组合，分析基于时序逻辑的软件体系结构描述语言XYZ/ADL在描述Web服务组合方面的优势，采用XYZ/ADL来描述服务组合的交互行为，相关的时间和数据约束用XYZ/RE表示。(2)基于有限状态自动机理论，建立异步Web服务的形式化模型。针对仅涉及时间约束的Web服务建立时间异步通信模型(TACM)，该模型符合UPPAAL规约，用消息队列模拟异步通信，用时间自动机中的标准时钟来表示时间约束；对于同时涉及时间和数据约束的情况，则建立异步Web服务模型(AWSM)。(3)分别提出基于TACM和基于AWSM的异步Web服务组合验证方法，并通过贯穿整个分析和验证过程的实例加以说明。