作为一种很重要的自动验证技术,模型检测已得到广泛研究,取得了丰硕的成果并应用到众多领域,引起学术界、工业界的密切关注。模型检测的一般原理是用状态迁移系统( M )表示系统的行为,用模态逻辑公式(ψ)描述系统的属性。这样“系统是否具有所期望的性质?”就转化为数学问题“状态迁移系统M是否是公式ψ的一个模型?”。因此,模型检测的研究主要围绕在为待测系统建模和采用某种方法正确有效地刻画待测系统的属性这两个方面进行。本文研究的系统主要是用于对广域网和因特网上的计算模型建模的环境演算系统,刻画该系统的属性采用的是模态逻辑中的空间逻辑并结合时态逻辑,分别从进程的结构性质与归约动作两方面进行描述。本文所做的主要工作如下:(1)首先研究了环境演算系统中的移动环境演算、安全环境演算和盒子环境演算,在已有的相关研究的基础上对这三个系统进行纵向的分析与比较,并分别给出了系统模拟与示例。(2)基于对上述三个环境演算的分析,给出了它们对应的面向归约语义的空间逻辑。一方面,该逻辑的静态部分刻画进程的结构,这部分不仅包含了传统的结构算子,而且还引入了新的描述进程前缀动作的逻辑算子。另一方面,该逻辑的动态部分刻画进程的归约动作,即做一步τ-动作后进程满足某些性质,本文不采用进程的行为动作语义,因此逻辑中不必考虑in、out等动作执行的情况。(3)分别为本文研究的模型系统和逻辑系统给出了相应的数据结构表示,并基于模型检测技术的原理来判断模型系统是否具有对应逻辑所描述的相关属性。本文给出了上述三个系统的模型检测算法并对算法的正确性进行了验证。