中文摘要：

利用形式化方法进行Web服务组合建模及验证是保证Web服务组合正确性与可靠性的重要手段。但是，当前用于Web服务组合建模的形式化方法均侧重于对模型进行描述、分析和验证，缺乏对底层实现的有效支持。本课题引入基于Kahn进程网络的Web服务组合建模方法，不仅支持组合系统的高层建模，而且支持系统的底层实现。针对当前主流的基于WSDL标准的Web服务组合语言缺乏形式化基础且对Web服务行为缺乏有效约束的不足，设计了一种新的基于Kahn进程网络的Web服务组合建模语言（CCML）。采用CCS进程代数对CCML语言描述的应用系统模型进行形式化验证，以保证服务组合的正确性。通过实现支持Web服务标准协议的分布式Kahn进程网络和CCML语言解释器，达到应用系统模型实现的目的。本课题研究成果将推动Web服务组合技术向更高层次发展，进一步加速Web服务组合技术的实际应用。

结论摘要：

该项目研究基于进程网络的Web服务组合建模和验证方法，项目研究内容已按计划全部完成，主要成果如下 1、提出了基于Kahn进程网络的Web服务组合建模方法，该方法不仅支持组合系统的高层建模，而且支持系统的底层实现。重点研究了Web服务的行为和行为组合，相应的组合模型称为CCM（Cooperative Composition Model，协同组合模型）。为了解决Web服务组合的个性化问题，将上下文感知计算技术应用到CCM中，并重点研究了上下文感知Web服务的行为自适应技术，即上下文感知Web 服务如何根据上下文的变化动态调整自身的行为，以使组合系统具有更高的灵活性和用户满意度。为了解决CCM中交互服务之间的行为不匹配问题，研究了Web服务的行为适配和验证技术，给出了行为不匹配的形式化检测方法和相应的适配方法。 2、设计了一种新的Web服务组合建模语言。为了描述基于进程网络的Web服务组合，设计了Web服务组合建模语言CCML（Cooperative Composition Modeling Language，协同组合建模语言）。与传统的Web服务组合语言相比，该语言具有严密的数学基础并侧重于描述Web服务的功能行为及服务之间的行为交互。因此，采用CCML描述Web服务组合，有利于提高组合的成功率。为了描述上下文感知的Web服务组合，将上下文感知计算技术应用于CCML中，并描述了其操作语义。 3、给出了CCM应用系统模型的形式化验证方法。首先将Web服务组合的CCML语言描述转换为CCS进程代数描述，并使用模态μ-演算表达该模型的时序逻辑属性，然后利用CWB-NC(Concurrency Workbench of the New Century)提供的基于时序逻辑的检测机制和验证工具对模型的属性进行验证。同时，给出了服务行为兼容性的定义和验证方法，通过CCS进程代数中观察等价性的概念来验证两个服务的行为是否兼容。实例表明上述验证方法是有效的。 4、给出了CCM应用系统模型的实现方法。采用Java RMI和Java多线程技术实现了能够支持Web服务标准协议的分布式Kahn进程网络，实现了CCML语言解释器。 5、选取电子商务等领域的典型应用案例，对CCM模型进行了应用研究。该项目在Web服务组合和验证技术、人才培养以及成果应用等方面均达到了项目预期目标。