计算机和网络通信技术的迅猛发展，Internet技术的兴起和广泛应用，有力地促进了网络环境下的商业应用发展和科学应用研究。广域高性能的网格技术的研究正是在这样的背景下提出来的。它的目标是将地理和组织上分布、异构的各种高性能计算机、数据服务器、大型检索存储系统和可视化、虚拟现实系统等，通过高速互连网络连接并集成起来，共同完成一些缺乏有效研究办法的重大应用研究问题，并且实现资源的共享。 现在的网格研究集中在网格建设、网格系统软件和应用开发上，学者们还很少涉及网格理论模型的研究。本文结合国家高性能计算环境NHPCE和织女星网格Vega Grid的开发和研究，对网格理论模型进行了深入研究，主要创新点包括：①建立了一个网格理论模型，网格自动机模型GAM，对网格系统进行形式化，②利用GAM，对网格一些基本算法和性质进行了研究，③提出基于GAM和古典Bell-LaPadula模型的网格访问控制模型GACM。 本文首次提出了网格理论模型，网格自动机模型。这个模型基于网格系统的异步特征，以异步I／O自动机理论为基础，利用自动机的组合操作和隐藏操作，很好地形式化了网格的局部功能和全局功能。GAM不仅可以被用来研究和分析现有网格系统，加深开发研究人员对网格的理解，还可以用来设计新的网格系统。 对于网格的三种通信子系统：点对点方式、广播方式和组播方式，本文进行了形式化，并且研究了这三种子系统的性质。虽然本文在进行形式化的时候，假定这些信道都是可靠的；但我们可以利用自动机的方法来模拟容错的信道，如TCP／IP，UDP信道。 在网格系统中经常要进行广播和聚合通信，这两种通信方式都要先构造一棵以特定源结点为根的生成树，然后再利用这棵树进行通信。在本文中提出了三种网格异步式广度优先搜索算法：GridBFS，LayerBFS和MiddleBFS，并证明这些算法将最终生成一棵包含系统中所有节点的广度优先生成树。本文还对异步式最短路径算法进行了形式化，并证明这个算法将最终为网格中每个非源点功能模块找到一条到源点的最短路径。本文还分析了这些算法的时间和通信复杂度。这些算法还能被应用到网格监控和死锁检测。 本文研究了网格稳定性质和网格快照，实现了检测扩散算法终止的异步DijkstraScholten算法，证明了这个算法最终将检测到终止的功能模块；本文还实现了摄取网格一致性快照的ConsistSnapShot算法，并证明了这个算法的正确性。稳定性质和快照的概念，被用来在网格中检验某个网格任务是否违反其所要遵守的性质，维护网格任务的全局状态备份，检测终止执行的网格任务，以及检测网格任务是否陷入死锁。 现在的网格安全研究集中在网格的认证方面，对于网格访问控制模型的研究涉猎很少。本文提出了网格访问控制模型GACM，这个模型以GAM和Bell-LaPadula模型为基础，对于每个网格站点的安全系统，都用一个结点自动机进行模拟；然后用这些结点自动机组合成为一个模拟整个网格安全系统的网格自动机。通过GACM，本文证明了一个有关网格安全的充分必要条件。GACM将传统基于格论的BLP模型扩展到整个网格的访问控制，从而可以在整个网格的基础上保持网格的安全性。 在对国家高性能计算环境进行功能测试时，本文将自动机迹的概念引入到网格功能测试，并且利用自动机迹的性质来指导测试用例的生成，成功地减少了冗余测试用例。本文还对最小测试用例集合和功能完备性的概念进行了定义。