王 焱，吴 涛，杨 斐

(1.成都信息工程大学 计算机学院， 成都 610225；2.中国核动力研究设计院 核反应堆系统设计技术重点实验室， 成都 610041)

0 引言

系统和软件设计的可靠性非常重要，因此如何构建可靠的软件和系统的相关技术就极为关键。特别是在一些关键领域，如航天航空领域、核领域等等，系统一旦出现故障，其带来的损失往往是不可接受的。由于传统的测试仿真只能寻找系统的错误，而不能证明系统不存在错误，形式化验证就能够解决这个问题。

模型检测是一种自动验证有限状态并发系统的形式化验证技术[1]，它能够通过对所给模型的所有可能状态进行分析，验证其是否满足所给定的规范。如果不满足，则生成相应的反例。系统规范一般是通过线性时序逻辑(LTL)或者分支时序逻辑(CTL)刻画的[2]。

在显式模型检测中，系统的设计模型通常用有向图表示。它表示了并发系统的所有可能的行为，同时还包含了各个状态之间的变迁关系。一般的，模型检测器采用确定性算法和穷尽搜索状态空间来验证是否满足某些性质。当状态空间过大时，就会导致检测效率较低，甚至不能完成检测目标。在核领域的DCS系统中，由于系统较为复杂，这种问题尤为明显。

为了提高模型检测的效率，业界提出了几种通过减少状态空间大小的方法来缓解这个问题，比如符号模型检测、抽象方法、偏序规约等等[3-5]。同时，除了上述的方法，提高在状态空间中搜索算法的效率也是可行的。……