摘要: 模型检验是一种可以自动验证某个系统模型是否满足一个给定的特性的形式化技术。模型检验的基本方法是利用计算机的强大计算和存储能力，对系统模型的状态空间进行穷尽搜索。但是，随着系统规模的扩展，状态空间的大小呈现爆炸性的增长，往往超出了当前计算机的能力极限。这被称为“状态空间爆炸问题”。这个问题在针对实时系统的模型检验中更加严重，其主要原因是在实时系统中引入了时钟变量。 时间自动机是可以用于对实时系统建模的有效工具。一个时间自动机是一个五元组 ( N , l 0 , C , E , I ) ，其中 N 为一个有穷的位置集合， l 0 ∈ N 是初始状态， C 是一个取实数值的时钟变量的有穷集合， E N × G ( C )×2 C × N 是转换的集合。 I ： N à G ( C ) 赋予每个 N 中的位置一个 G ( C ) 中的位置不变式。这里 G ( C ) 表示形如 x ~ c （ ~ ∈ <,≤,≥,> ）的原子公式 的合取式的集合。在运行时刻，所有时钟变量的值随着时间同步增长。当自动机当前状态为 l 时，转换 ( l , g , r , l' ) 的使能条件是时钟变量的取值满足 g ，而当转换发生之后， r 中时钟的值被重置为 0 。 多个并发的时间自动机可以通过同步通信机制，或者共享变量相互影响，形成一个时间自动机的并发组合。 我们研究的内容是对时间自动机，以及它们的并发组合的可达性分析，即验证系统是否可能到达一个特定的状态。由于时钟变量是取实数值的，因此一个时间自动机的状态空间是无穷的。所以，大多数可达性分析算法通过对符号状态的枚举来完成分析。一个符号状态是一个二元组 ( l , D ) ，其中 l 是一个自动机的位置，而 D 是一个时间约束。时间约束是一组形如 x - y ~ c 的原子约束的合取式，其中 x , y ∈ C ∪ 0 ， c 是常量。一个符号状态代表了一个具体状态的集合。给定一个符号状态 ( l , D ) ，和一个离开 l 的转换 e ，我们可以计算得到 ( l , D ) 相对于 e 的符号后继，记为 sp δ ( e ,( l , D )) 。符号后继是时间自动机的具体状态之间的后继关系的符号表示。对于时间自动机的可达性分析算法可以简单描述如下：从初始符号状态开始，通过计算已有符号状态的符号后继，不断生成新的符号状态。这个迭代过程的结束条件有两个： 1 、不能再生成新的符号状态。此时算法返回 false ，即目标状态不可达； 2 、生成了一个和目标状态相交的符号状态。此时算法返回 true ，即目标状态可达。 论文的基本思想是基于这样一个事实：在算法生成的符号状态中，大部分的原子约束实际上并不影响时间自动机的符号化演进。消除这些原子约束并不会影响到可达性分析的结果。我们把这样的原子约束称为“无关原子约束”。由可达性算法得到的符号状态中，通常有着 n(n+1)/2 个约束（ n 为时钟个数）。而从认知学原理来讲，一个设计师在考虑系统的正确性的时候，往往只会考虑其中的几个关键原子约束。因此，无关的原子约束是广泛存在的。删除这些无关的原子约束可以使得可达性分析算法的效率得到显著提高。 本文首先证明了两个有关时间约束的合取运算的性质。并以此为基础，证明了两个可以用于寻找无关原子约束的定理： ? 如果从某一个位置 l 出发，一个时间变量 x 在被重置之前，不会被任何转换用形如 x > c 或者 x ≥ c 的条件测试，那么符号状态 ( l , D ) 中的所有形如 x - y < c 和 x - y ≤ c 的原子约束都是无关的。 ? 如果从某一个位置 l 出发，一个时间变量 x 在被重置之前，不会被任何转换用形如 x < c 或者 x ≤ c 的条件测试，那么符号状态 ( l , D ) 中的所有形如 y - x < c 和 y - x ≤ c 的原子约束都是无关的。 随后，我们提出了两个寻找无关原子约束的方法：静态方法和动态方法。在静态方法中，我们通过对单个自动机的分析，获取有关对时间变量的测试和重置的信息，并使用这些信息在进行可达性分析的时候寻找并删除无关原子约束。在动态方法中，我们的算法根据可达性分析算法在检验过程中已经生成的符号状态及相关信息来寻找并删除无关原子约束。第二种方法可以找到更多的无关原子约束 ,但是要付出运行时间的代价。 我们将以上的技术结合进可达性模型检验算法。在实例研究中表明这种技术可以得到很好的优化效果。