基于网格应用的高层形式化描述

论文摘要

开放式网格服务体系结构(OGSA, Open Grid Services Architecture)的思想是把Globus和Web Service结合起来,提出了网格服务的概念,它将一切计算资源、存储资源、网络、数据库等以服务的形式呈现,通过定义标准的服务接口,把服务实现、资源所在地和物理资源屏蔽,这样使得各种应用能够进行共享和交互操作。然而,由于网格系统中存在分布、动态、数量众多的网格服务,网格服务信息分布于网格系统的不同位置,同时很多网格服务之间存在一定的关联和依赖,一种服务的失效影响与之关联的所有服务的可用性。因此,如何管理和维护这些分布、动态的网格服务信息,保证这些网格服务的可用性和一致性,同时支持高效率的基于信息的服务检索,是网格服务研究的一个重要问题。然而目前大部分的网格服务信息采用XML语言描述,虽然具有一定的语义支持,但概念还缺乏严格的形式化定义,选择合适的形式化方法来描述和规范网格应用系统是一个很关键的问题。针对这个问题,本文提出了网格自动机的理论模型,以及基于抽象状态机ASM(Abstract State Machine)的传感器网格应用的形式化描述模型,形式化地给出传感器网格服务的表示模型。基于抽象状态机定义了传感器网格具体的规则,例如传感器节点发现目标,连接服务器,资源匹配,资源请求,服务信息的发送接收,服务注册等,阐述了传感器网格服务信息之间的关联及其约束。另外基于规则的描述,利用微软亚洲工程研究院开发的. NET的AsmL工具对其进行验证,生成有限自动机,精确地定义了传感器网格的功能模块之间的交互以及状态的演化,形式化的描述保证了模型的一致性和正确性。同时通过该工具生成的所有的状态变化的测试用例来进一步分析模型的语义及其验证。

论文目录

• 摘要
• Abstract
• 第一章 绪论
• 1.1 论文的研究背景
• 1.2 国内外研究现状
• 1.3 论文的主要工作
• 1.4 论文的主要框架
• 第二章 网格及网络中心战
• 2.1 网格的概念
• 2.2 网格的标准化趋势
• 2.3 OGSA 的体系结构
• 2.4 OGSI 规范
• 2.5 GLOBUS TOOLKIT
• 2.6 网络中心战
• 2.6.1 网络中心战的概念
• 2.6.2 网络中心战的网格体系结构
• 2.7 本章小节
• 第三章 形式化方法
• 3.1 形式化方法
• 3.1.1 形式化方法的概念
• 3.1.2 形式化方法的特点
• 3.2 常见的几种规范语言及其特点
• 3.2.1 SDL 语言
• 3.2.2 Z 语言
• 3.2.3 SPIN 和Promela
• 3.2.4 Unified Modelling Language （UML）
• 3.3 本章小节
• 第四章 传统网格的形式化方法的研究
• 4.1 网格自动机
• 4.1.1 有限自动机理论
• 4.1.2 网格自动机
• 4.1.3 网格服务的自动机
• 4.2 抽象状态机
• 4.2.1 ASM 的发展
• 4.2.2 ASM 的应用
• 4.2.3 ASM 的基本定义
• 4.2.4 ASM 的基本规则
• 4.2.5 ASM 的扩展规则
• 4.2.6 基于抽象状态机的网格与传统分布式网络的区别
• 4.3 本章小节
• 第五章 网格应用的形式化描述模型
• 5.1 传感器网格的框架
• 5.2 传感器网格的仿真图
• 5.3 传感器网格的功能分析
• 5.4 传感器网格模型的工作时序
• 5.5 传感器网格管理服务器的有限自动机模型
• 5.6 基于ASM 传感器网格的形式化描述
• 5.6.1 模型的语义分析
• 5.6.2 传感器网格的语义模型
• 5.7 本章小节
• 第六章 工具实现及实验研究
• 6.1 抽象状态机语言ASML 工具
• 6.1.1 ASML 的发展及其应用
• 6.1.2 ASML 基本用法实例
• 6.2 语义测试与模型检测
• 6.2.1 资源匹配和资源请求的模型
• 6.2.2 管理服务器获取所有节点信息的模型
• 6.3 本章小节
• 第七章 总结和展望
• 7.1 本文工作总结
• 7.2 进一步研究方向
• 致谢
• 参考文献
• 作者在读期间的研究成果