基于Web服务组合的软件服务协同技术已成为构造开放网络的动态协作、按需组合的服务交互环境的关键支撑技术。在实际的复杂应用环境中,如何基于语法和语义的正确性检验剔除服务组合的不良程序行为,以及如何确保贯穿服务组合生命周期的QoS质量成为制约服务组合应用的两个具有挑战性的关键问题。为实现动态的跨企业业务协作与集成,本文围绕服务组合行为的正确性检验以及服务质量保证这二个正交的性质,深入研究了基于进程代数Pi演算及离散时间Ambient演算的服务组合形式化检验,以及基于QoS数学模型进行精确计算的服务组合优化与划分方法。实现了支撑形式化检验与QoS感知的服务组合架构,并将该架构应用于数字卡通的网上协同制作。本文完成的主要工作如下:(1)针对服务组合行为的检验,扩充了Pi演算上的可描述XML数据类型的类型系统,建立了BPEL4WS与Pi演算的双向映射。提出了带有出错程序片段追踪的验证算法,包括基于开互模拟的Pi演算检验、基于模态μ演算的性质检验、基于类型化Pi演算的服务相容性检验,其中独立提出了针对服务组合的相容性定义和检验算法,并且在Web服务组合过程中引入服务相容性检验制导的发现与组合方法。基于以上研究,研制了嵌入了Web组合服务验证工具WebJetChecker,采用组合验证的方法对服务组合程序的性质进行验证,在验证工具中实现了对服务组合程序的出错路径自动标识与出错提示。(2)为描述带时间约束的移动行为的分布式动态服务组合,以及复杂Web服务组合结构,独立提出了离散时间Ambient演算(Discrete Timed Mobile Ambient,DTMA)。给出了DTMA的语法和语义、DTMA的性质、DTMA模态逻辑。通过结合时间同步树与Ambient图两种形式化模型,以Ambient时间同步树的方式将实时和移动特征统一在一个形式框架内。对于DTMA与DTMA模态逻辑的子集给出了一个模型验证的算法,证明了验证算法的可判定性。在基于DTMA的BPEL4WS活动的编码基础上,讨论了多层scope的出错与补偿处理Ambient演算形式化模型,并用DTMA描述和分析了带时间约束的移动分布式服务组合实例。(3)深入研究了基于QoS的服务组合优化算法,在局部优化算法上实现了针对成分服务选择的基于自动修正区间判断矩阵的层次分析法。在全局优化算法研究上,基于启发式0-1整线性规划算法结合了修正单纯形法和启发式枚举法,仿真实验表明该算法与MATLAB 7的0-1整数规划方法比较,在优化程度及优化效率上得到了显著改进,并且对服务组合和候选服务集合的规模变化没有明显的相关性,因而该算法可用于服务组合规模动态变化的场景,但该算法不能应用于存在服务联盟(服务域)的非线性全局优化模型。因而本文进一步研究了基于QoS的Web服务优化选择的树型编码遗传算法,仿真实验表明在同等优化效果下,树型编码遗传算法比一维编码遗传算法获得了更快的速度,并可有效地支持组合服务运行时重计划。由于树型编码遗传算法可求解非线性全局优化模型,解决了服务联盟的服务组合优化问题。(4)针对数据流约束的应用环境,提出了按服务域的基于图聚类的服务组合划分算法。存满足服务域之间数据流量最小化及分布式系统吞吐量最大化的目标约束下,运用图聚类的多级算法划分BPEL服务组合,然后采取分布式方式运行服务组合片段,并对BPEL片段迁移到的分布式节点的负载进行均衡调整。(5)基于以上研究,提出了一种支撑QoS感知的服务组合架构。该架构包括服务组合执行引擎的设计,采取了解耦流程执行和成分Web服务调用的方式,实施了带有双控制反馈控制环的流程执行结构。仿真实验表明引入QoS反馈控制结构,使得引擎在组合服务负荷变化时,可为不同的请求服务等级提供服务响应时间保障;解耦流程执行和成分Web服务调用提高了引擎资源的使用效率及引擎的吞吐量。该架构还支持服务组合运行时容错处理的框架,基于此框架研究了用户SLA估计值与实测值偏差检测的在线容错机制,提出了容错选择因子概念及向容错处理方法的映射函数,对运行时故障处理方式提出了“重试调用—替代失效服务—重构局部流程”处理策略,仿真实验表明该在线容错机制有效地支持了服务组合流程的在线自恢复。综合应用以上研究成果,设计并实现了一个支撑服务组合的形式化检验与QoS感知的服务组合架构原型系统,并将该架构应用于数字卡通企业协作群的网上协同制作,实现了卡通动画的跨企业协同制作工艺流程。
