【作者】 高春鸣；

【导师】 陈火旺；

【作者基本信息】 国防科学技术大学 ， 计算机科学与技术， 2007， 博士

【摘要】 基于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感知的服务组合架构原型系统,并将该架构应用于数字卡通企业协作群的网上协同制作,实现了卡通动画的跨企业协同制作工艺流程。更多还原

【Abstract】 The software service cooperation technology based on Web Services composition has become the critical technique to construct the circumstance of the dynamic cooperation and on-demand composition service interactions. Under the complicated application circumstance of Web Service composition, there exist two challenging and critical problems: one is how to eliminate the ill behaviors of the orchestration based on verifying the correctness of grammar and semantic, the other is how to guarantee QoS throughout the lifecycle of service composition.In order to achieve dynamic business cooperation and integration across different enterprises, this thesis mainly focuses on the two orthometric properties that are correctness verification and Qos guarantees of Web Service composition. Formalization verification of service composition based on Process Algebra and Discrete Time Ambient-Calculus, as well as combinatorial optimization and the partition method based on QoS mathematic model are deeply studied. The service composition architecture supporting formalization verification and QoS-aware composition has been also implemented. Furthermore, the architecture is applied to digital cartoon cooperation manufacturing in the Internet. The main work of this thesis is displayed as follows:(1) Aimed at the verification of Web Services composition, Pi-Calculus with type system for describing XML data structure is extended, then the dual mapping between BPEL4WS and Pi-Calculus is constructed. A verification algorithm with the function of tracking the error fractions for Web services composition is proposed, which includes Pi-Calculus verification based on open bisimulation, properties verification based on modalμ-Calculus and service compatibility verification based on Pi-Calculus with type. Moreover, we independently give the definition of compatibility and propose compatibility verification algorithm for Web services composition, and also introduce a novel method for discovering and composing services in the process of Web Services composition under the guidance of verifying compatibility of composite Web Services. Based on the above studies, a framework supporting formal verification of service composition, in which the verification tool called WebJetChecker is embedded, is proposed. WebJetChecker with the combination of three types of the verification techniques for verifying orchestration properties is implemented, by which the error fractions of the orchestration are automatically marked and the hints are given.(2) In order to describe distributed dynamic services composition with time-constrained mobile properties and complex structures of services composition, Discrete Timed Mobile Ambient (DTMA) is independently proposed. In the thesis, the semantics and syntax, properties and model logic of DTMA are given. Through combining two formalization models—time synchronous tree and Ambient graph, the time and mobile property are unified into a formal frame by Ambient synchronous tree. A model verification algorithm based on DTMA and the subset of DTMA modal logic is devised, and the decidability of the model verification is proved. According to the encoding of BPEL4WS activities on DTMA, the fault and compensation processing with multi-layer scope are modeled, and an instance of distributed service composition with time constraint and mobility is also described by DTMA and analyzed by the model verification method.(3) It is made our every effort to study optimal algorithms of QoS-aware Web service composition. On local optimal algorithms, an AHP approach is realized, which can automatically modify judgment matrix for selection of the component services. On global optimal algorithms, a heuristic 0-1 Integer Liner Programming algorithm is achieved, which combines heuristic enumeration method and revised simplex method. Simulation experiments show that the degree and optimization efficiency in our algorithm is obviously improved compared with the MATLAB 7 bintprog function that is a 0-1 integer programming algorithm. Moreover our algorithm isn’t relevant to the scale changes of Web services composition and candidate service sets, thus it is applicable for the scenes that the scales of Web services composition changed dynamically. But for Web services composition with service alliance (service domain), the algorithm is unable because the non-linear global optimal model of the fitness function and QoS constraints can’t be expressed in linear mode. Therefore, Tree-Coding Genetic Algorithm (TGA) is used to solve the QoS-aware global optimization with non-linear model. The results of simulation experiments show that TGA is capable of running faster than the one-dimension coding GA under the same conditions, and Tree-Coding has efficient capability for supporting re-planning. In conclusion, TGA has solved non-linear global optimization problems with service alliance.(4) Aimed at the application of data stream constraint, a Web services composition partition algorithm based on graphic clustering and service domain is put forward. Under the constraints of satisfying the data stream minimization between the clusters and the throughput maximization of the distributed system, multi-level algorithms based on graph clustering is used to partition BPEL service composition. Afterward, a way of distributed execution is employed to execute service composition. Furthermore the load of the distributed nodes transferring the BPEL fractions is adjusted to a balance.(5) According to the above studies, an infrastructure supporting QoS-aware service composition is proposed. The infrastructure includes the design and implement of Web services Composition Execution Engine with double feedback controlling loops, which can decouple flow execution and Web service invocation. From the simulation results, it can be concluded that QoS feedback controlling structure can make the engine supply the guarantee of service response time for different service classes when the workload of Web services composition varies significantly. Additionally, the method of decoupling flow execution and service invocation improves resource utilization and increases concurrence ability of flow execution and throughputs of the engine. This paper also presents run-time fault-tolerance processing framework supported by the infrastructure. Based on the framework, online fault-tolerance mechanism on the deviation detection between QoS measuring values and SLA estimated values is studied. A new concept—"fault-tolerance selection factor" and a mapping function which makes this factor map to the fault-tolerance processing are proposed. The simulation experiments also show that the "retry-substitute-reconfigure" processing strategy adopted at run-time fault processing can effectively support online self-resumption of service composition processes.On the basis of all of the above research results, a Web service composition prototype system supporting formal verification and QoS-aware service composition is designed and implemented. This architecture is applied to cooperation manufacturing across different digital cartoon enterprises in the Internet, through which the technologic process of cooperation manufacturing in digital cartoon is realized.更多还原