形式验证是一种比测试和模拟更具吸引力的描述和验证软硬件系统的方法.形式验证方法的种类很多,从定理证明到计算机辅助定理证明,最后出现模型检测方法.该文所提出的两个缓解状态爆炸现象的方法都是在现有方法的基础上加以改进或拓宽适用范围.其一,在最近由Glenn提出的部分状态空间模型检测技术的基础上,讨论一类具有公平性约束条件的CTL(计算树逻辑)模型检测问题.部分状态空间模型检测方法只搜索部分状态空间,通过定义一个序关系来表达部分状态空间之间的关系.其二,鉴于目前所提出的分布式模型检测算法破坏了原有顺序算法的嵌套深度优先搜索顺序,因此不能验证LTL公式.我们提出了一种能够保持深度优先搜索序的分布式嵌套深度优先算法(DDDFA)来验证LTL公式所刻画的属性.论文还讨论了网格计算环境下信息服务体系结构,为了实现网格计算环境中大规模资源共享的目标,需要定义一个灵活、安全、协调的资源共享机制,这种共享机制是建立在某个通过动态组合个体、机构及资源而构成的VO上的.而VO范例的实现依赖于分布式目录服务,即目录服务趋于分布.但分布的一个后果就是它很难提供给用户一个准确的信息,因此分布式目录服务的主要任务就集中到如何准确获得一个实体的位置信息.该文工作的最主要的意义是:鉴于现有验证无限状态系统(特指参数化系统)的方法,几乎都是从系统的符号化模型开始进行到达性分析,该文定义了一个可以直观描述参数化系统的语言PSL,并给出直接从PSL脚本自动生成符合化模型的算法.因此,我们的工作是最新的,它使验证参数化系统更自动更完整.另外,该文是第一次尝试用形式化方法描述和验证网格计算环境中的关键部件,并获得一些满意的实验结果.由于形式化方法可以精确验证系统的正确性,所以可以提高设计这些关键部件的准确性.