论文部分内容阅读
随着计算机软、硬件系统复杂性的日益增长,系统设计和实现的正确性越来越难以得到保证。因此,用以检验系统正确性的形式化方法亟待出现。上个世纪80年代提出的模型检验方法被证明是行之有效的系统正确性验证手段。执行模型检验的算法,对所采用规约语言的类型十分敏感。由于线性框架下的时序逻辑(如LTL),具有表达能力(相对)较强、直观、兼容性好等特点,使得这类时序逻辑在实际应用中被使用的相对广泛。但是,在工业界应用中,许多重要的时序性质无法采用LTL表达。因此,若干LTL的扩展被陆续提出,它们大致分为两类。1.一种方法是向时序逻辑中添加无穷多个时序连接子或者正规表达式,以期获得等价于ω-正规语言的表达能力。这类逻辑如ETL、FTL、PSL等。2.另一种方法是向时序逻辑中添加二阶量词或者不动点算子。这类时序逻辑诸如MSOL、QTL、线性μ-演算等。这些LTL的扩展,都与ω-正规语言等价。对于这些逻辑本身,人们比较关心下列问题:1.判定问题。即:逻辑的(可满足)判定性及其复杂度。这是在这些逻辑被提出时首先要解决的问题。2.公理化问题。即:能否给出一套针对该种逻辑的可靠完备的公理系统。公理系统往往由若干公理和推理规则构成。这些公理/规则刻画了该种逻辑的实质。3.模型检验问题。对于某种特定的时序逻辑,开发其高效的模型检验算法是人们追求的核心目标之一。同时,有无高效的检验算法也直接影响该种逻辑能否得到广泛应用。对于时序逻辑的各类ω-扩展,其公理化以及符号化模型检验算法的研究还具有另外的特殊意义。在线性结构上,等价于ω-正规语言的时序逻辑具有足够强的能力表达工业界实际应用中用到的各种性质。各种线性时间的时序逻辑,可以看作它们的逻辑片断或者子逻辑。因此,这些逻辑的公理化以及符号化模型检验算法可以派生出它的子逻辑或者实例的的公理系统和符号化模型检验算法。本文主要工作如下:1.给出了三类ETL(ETLl、ETLf、ETLr)的可靠完备的公理系统,同时给出了基于时序算子编码的ETL逻辑片段可靠完备公理化方法。2.基于博弈方法,给出了μ-演算的公理系统的新的完备性证明。同已有的方法相比,该证明相对直观、简洁。3.基于tableau方法,给出了三类采用交错自动机作为连接子的ETL(ATLf、ATLl、ATLr)以及PSL的某个变种(APSL)的基于BDD的符号化模型检验算法。4.分别给出了具有一般形式和特定形式(ν-范式)的线性μ-演算的基于BDD的符号化模型检验算法。5.基于上述算法,在模型检验工具NuSMV的基础上,实现了支持扩展时序逻辑的符号化模型检验工具ENuSMV。它允许用户通过描述自动机的方式自定义时序连接子,能够检验全部的ω-正规性质。