【作者】 许可；

【导师】 吴澄；

【作者基本信息】 清华大学 ， 控制科学与工程， 2007， 博士

【摘要】 网格服务流是实现复杂网格应用中大规模异构资源协作与共享的重要手段。如何确保其设计和实现上的正确性是系统科学和计算机科学领域的前沿性研究方向,具有重要的理论意义和实用价值。本文通过提出一种称为状态π演算的状态/事件混合形式化工具,采用与模型验证(Model Checking)相结合的手段,系统研究了以状态π演算为基础的网格服务流形式化建模、验证及验证性能优化技术。部分研究成果已在LIGO数据网格项目和银行法律法规验证中得到应用。结合网格中Web服务资源框架对有状态资源的管理特点,本文首先提出了一种状态π演算的新形式化工具并分析了其语义和性质,它实现了对系统状态的灵活抽象与管理,有效简化了网格服务流及其业务逻辑的建模和验证。基于状态π演算,本文实现了网格服务及其选择、BPEL4WS、DAGMan规范和网格服务流中并发与管道模式的形式化语义。这不仅为部分晦涩复杂的网格服务流规范提供了重要的形式化基础,也验证了状态π演算自身的表达能力。在此形式化语义的基础上,本文从网格服务流的结构验证、规范语义约束验证、业务逻辑验证及其一致性检验的四个方面和静态/动态两个层面对其形式化验证技术进行了研究。通过提出状态π演算的强/弱状态断言和灵活复用模型验证的方法为以上问题提供了系统的解决方法。通过应用实例发现,该方法实现了对状态π演算的状态/事件混合推演和模型验证支持,且有减少重复验证和验证方法独立于特定模型验证技术的优点。进一步,本文还从服务流验证分解和错误过程模式的两种思路,研究了对网格服务流形式化验证的性能改进。一方面,通过将网格服务流分解为一系列串行域和并发支,提出了基于模块化验证的验证分解策略;另一方面,通过分析网格服务流中可能存在的错误过程模式及其特点,提出了基于错误过程模式搜索向导的快速证伪方法。通过不同复杂度的LIGO引力波数据分析服务流实例和数值比较结果,验证了以上两方法在验证效率和内存占用上均有明显提高。最后介绍了本文工作的系统化集成,即GridPiAnalyzer原型系统的模块和应用。它目前已提供了对Condor DAGMan、BPEL 1.1规范和IBM WBITM的支持。更多还原

【Abstract】 Grid service flow is an important paradigm for realizing complex heterogeneous resource collaboration and sharing in various grid applications. Correctness verification in the design and implementation of grid service flows is an active research topic in the domain of system science and computer science which enjoys both great theoretical and practical values. Based on realistic applications like LIGO data grid, this dissertation has systematically investigated the formal modeling, verification and its performance issues for grid service flows by proposing a calculus called the stateπcalculus and the study of its formal verification support.Following the new feature of stateful resource management introduced in the Web Service Resource Framework, first a new stateπcalculus is proposed to further strengthen its capability in managing the life-cycle of system states. The proposed calculus not only enables the flexible abstraction and management of historical system events, but also facilitates the modeling and verification of grid service flows. Moreover, based on the stateπcalculus, the formal semantics of grid service execution and selection, the specification of BPEL4WS, DAGMan and the parallel / pipeline patterns in grid service flows are also rigidly captured, which at the same time has verified the full expressiveness of our stateπcalculus.Based on the formal semantics of grid service flows with stateπcalculus, the dissertation fully studies from both the static and dynamic aspects of its formal verification issues including its structural correctness, specification satisfiability, business logic satisfiability and consistency. Systematic solution is provided for the above issues by the proposal of strong/weak state assertion for our stateπcalculus with its model checking support. By the gravitational wave data analysis application from LIGO data grid, it is shown the proposed solution enjoys the advantages of: (1) supports the state / event hybrid analysis and model checking of stateπcalculus models; (2) reduce unnecessary verifications to save the verification cost; (3) be independent of specific model checking engine and thus enjoys a wider choice of new formal verification techniques.Furthermore, the improvement of verification performance is also investigated by following the two ideas of grid service flow decomposition and process bug patterns respectively. On the one hand, by decomposing a grid service flow into a set of sequential standard regions with parallel branches, the corresponding verification strategy is also decomposed following the idea of modular verification. On the other hand, by identifying the potential process bug patterns in the structure of grid service flows, the idea of guided search is combined into the formal verification of grid service flow to efficiently falsify its correctness. With the performance evaluation on verifying multiple gravitational wave data analysis applications with different complexity from LIGO, it is illustrated that the proposed approaches can effectively reduce both the required CPU time and memory cost compared to using various traditional verification approaches alone.Finally, the framework and application background of GridPiAnalyzer, an automatic tool support for the formal verification of grid service flows based on this dissertation, is introduced. It currently provides the support for Condor DAGMan, BPEL4WS 1.1 specification and IBM’s Websphere Business Integrator TM model.更多还原