作为一种自动化的程序验证方法,近几十年来模型检测技术在软硬件程序、通信协议以及安全协议等领域的正确性分析和验证中得到了广泛的应用。在模型检测中,使用一个有限的系统状态迁移结构模型来描述待验证的系统,并借助某种时序逻辑公式来描述待验证系统的期望性质,然后在这个基础上通过模型检验算法自动化地判断待验证的系统是否满足其期望的性质。经过成熟研究的经典时序逻辑,如线性时序逻辑(LTL)、分支时序逻辑(CTL)等,很难甚至无法描述并行系统的区间相关性质和循环性质。命题投影时序逻辑(PPTL)通过引入chop和projection等时序操作符,可以较方便地描述上述性质,且被证明具有描述完备正则性质的优越表达能力。然而,随着软件行业的不断发展,程序规模不断增大以及复杂程度的不断提高,模型检测技术面临着严重的状态空间爆炸问题。符号模型检测(SMC)是一种基于ROBDD(冗余有序二叉决策图)的针对状态空间爆炸问题而产生的有用的机制。在SMC技术中,使用布尔公式对待验证的系统状态集合以及状态之间的迁移关系进行符号化的编码,而布尔公式本身则使用ROBDD来实现,从而使用ROBDD隐式的实现状态空间及状态空间上的操作,缩减了状态空间的存储。因此,符号模型检测可以处理相对更大规模、更加复杂的系统,在一定程度上有效的缓和了当前面临的状态空间爆炸问题。NuSMV是一个在学术界和工业界应用广泛且日益成熟的限界和符号模型检测工具,使用Nu SMV特定的输入语言描述系统模型,LTL或者CTL来表征期望性质,实现了LTL和CTL的符号和限界模型检测。本文提出了一种基于Nu SMV的PPTL符号模型检测方法。在此方法中,系统设计模型是一个Kripke结构模型M,而系统的期望性质由PPTL公式?来描述。首先将公式的非??转换为对应的LNFG,在此基础上继续进行转换得到??对应的Büchi自动机模型。然后将系统模型M的初始状态集合I沿Büchi自动机向后扩展,若无限经常次的扩展至Büchi自动机的某个可接收节点时,保持可接受节点对应系统状态集不为空,则说明系统模型M中至少存在一条路径满足??,即M|??,此时可给出相应的反例,帮助系统分析与设计人员修正和定位设计中存在的错误;否则得出M|??的结论,即期望的性质有效。此方法基于Nu SMV中使用的Kripke结构模型,并且借助于PPTL来描述待验证系统的期望性质,增强了模型检测的性质刻画能力。另外,采用系统初始状态集合沿着Büchi自动机模型向后递归扩展的方法,在遇到反例的时候可以立即终止Büchi自动机的状态搜索过程,系统模型扩展至空集时也可以立即停止搜索,实现递归过程的剪枝。