摘要: 1．本文的创新点
网格技术的快速发展带来了网格应用复杂程度的不断提升。为了确保网格工作流执行期具有足够的可靠性和可信性，排查并验证在应用设计的初始阶段中的时序特性中的错误的问题在这种背景下尤为重要。本文通过提出一种称为状态?演算的状态/事件混合形式化工具，采用与模型验证（Model Checking）相结合的手段，系统研究了以状态?演算为基础的网格服务流形式化建模、验证及验证性能优化技术。
2．实现方法
结合网格中Web服务资源框架对有状态资源的管理特点，本文首先提出了一种状态?演算的新形式化工具并分析了其语义和性质，它实现了对系统状态的灵活抽象与管理，有效简化了网格服务流及其业务逻辑的建模和验证。基于状态?演算，本文实现了网格服务及其选择、BPEL4WS、DAGMan规范和网格服务流中并发与管道模式的形式化语义。这不仅为部分晦涩复杂的网格服务流规范提供了重要的形式化基础，也验证了状态?演算自身的表达能力。
在此形式化语义的基础上，本文从网格服务流的结构验证、规范语义约束验证、业务逻辑验证及其一致性检验的四个方面和静态/动态两个层面对其形式化验证技术进行了研究。通过提出状态?演算的强/弱状态断言和灵活复用模型验证的方法为以上问题提供了系统的解决方法。通过应用实例发现，该方法实现了对状态?演算的状态/事件混合推演和模型验证支持，且有减少重复验证和验证方法独立于特定模型验证技术的优点。
进一步，本文还从服务流验证分解和错误过程模式的两种思路，研究了对网格服务流形式化验证的性能改进。一方面，通过将网格服务流分解为一系列串行域和并发支，提出了基于模块化验证的验证分解策略；另一方面，通过分析网格服务流中可能存在的错误过程模式及其特点，提出了基于错误过程模式搜索向导的快速证伪方法。通过不同复杂度的LIGO引力波数据分析服务流实例和数值比较结果，验证了以上两方法在验证效率和内存占用上均有明显提高。
3．结论及未来待解决的问题
在引力波探测数据分析的真实试验中，首先我们证实了本方法能够快速寻找到逻辑验证程序中具有错误或者不一致的情况，并将违背约束限制的可能性通过逻辑验证体现出来，同时后续的优化方法本方法能够大大降低验证过程的CPU和内存消耗量，提升优化性能和效率。
4．实用价值或应用前景
以上研究成果在本文的系统化原型GridPiAnalyzer得到了具体的结合与实现，从而为网格服务流的正确性保障提供了自动化和可视化的工具支持。本文部分研究成果已在LIGO项目的引力波探测数据分析和银行开系统的反洗钱法验证中得到了实际的应用案例。