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