导读:本文包含了符号化模型检验论文开题报告文献综述及选题提纲参考文献，主要关键词:模型检验,SAT求解器,限界模型检验,LTL
符号化模型检验论文文献综述
王瑞[1]（2014）在《基于SAT的符号化模型检验技术研究》一文中研究指出随着计算机技术的不断进步,计算机系统的软硬件设计越来越复杂,过于复杂和庞大的设计必定会带来越来越多的设计缺陷和错误。传统的方法很难检测到系统设计中的所有错误。然而,系统的安全性在航空、航天、国防、医疗等安全攸关的领域却非常重要。因此,用以保证系统正确性的形式化方法亟待出现。模型检验是上世纪80年代提出的一种针对有穷状态系统进行自动化验证的技术。经过30多年的发展,模型检验技术已经是计算机辅助验证领域非常重要的技术之一。然而,状态空间爆炸问题始终是制约模型检验技术发展的最大障碍。为此,研究人员提出了很多技术来对付该问题,比如基于BDD的符号化模型检验技术、偏序归约技术、抽象精化技术等。近年来,随着SAT技术的进展,Biere[1]等人提出了基于SAT的限界模型检验技术。该技术利用SAT求解器的能力进一步提高了模型检验技术处理问题的规模。目前,基于SAT的符号化模型检验技术已经成为计算机辅助验证领域研究的热点问题之一。然而,在实际应用中,基于SAT的符号化验证技术还存在诸多问题,比如验证效率、验证能力、完全性等。本文围绕基于SAT的符号化模型检验技术进行了一系列研究,旨在进一步提高该技术的效率以及扩展该技术处理问题的能力。本文的主要贡献包括:1)优化了LTL的限界模型检验技术针对现有的LTL的限界模型检验技术,本文提出两种优化的方法。第一种优化技术是一种称为反例集合保持的化简技术,该技术的核心思想就是在进行模型检验之前,首先使用一种轻量级的技术对待验证的LTL性质进行化简,使得化简后的性质与原性质关于待验证的模型是等价的。因此,在真正的模型检验中,就可以使用化简后的性质代替原性质进行验证,该技术对于复杂的性质规约具有非常明显的作用。第二种优化技术,是利用SAT求解器的增量式求解能力,优化了基于语义的限界模型检验编码,实验表明,新的编码在验证效率上,相对于其他编码有很大的优势。这两种技术可以很自然地结合起来,从而提高LTL的限界模型检验效率。2)提出ω-正规性质的限界模型检验算法。由于在工业应用中,许多重要的时序性质无法采用LTL表达,因此,针对ω-正规性质的限界模型检验具有十分重要的理论和实际意义。本文针对两种具有ω-正规表达能力的时序逻辑ETLl+f和QTL,分别提出了对应的限界模型检验算法。针对ETLl+f,本文提出了基于语义的限界模型检验算法。该技术的核心是构造ETLl+f的tableau,通过扩展LTL的tableau构造技术,本文提出了ETLl+f的tableau构造算法。针对QTL,本文提出了两种限界模型检验算法,分别为基于语法的限界模型检验和基于语义的限界模型检验。基于语法的限界模型检验的核心思想是将QTL公式的限界语义编码成QBF公式,然后利用QBF求解器来验证该问题。基于语义的限界模型检验同样是通过扩展LTL的tableau构造方法得到QTL的tableau构造方法,然后将限界模型检验问题转化为受限路径上的公平性路径查找问题。然后,将公平性路径查找问题编码成布尔公式,最后利用SAT求解器来验证该问题。3)提出了基于SAT的符号化模型检验的完全性保证的算法。制约限界模型检验技术应用的一个主要瓶颈在于其不是一种完全的技术,即它不能证明给定的模型是否满足给定的性质。然而,线性时序逻辑的模型检验问题最终都可以转化为公平性路径查找问题,而公平性路径查找问题可以转化为若干个可达性问题。因此,开发高效的可达性算法是解决基于SAT符号化模型检验完全性保证技术的核心。本文基于目前最好的可达性算法,即属性指导的可达性分析算法(Property Directed Reachability,简称PDR),提出了两种新的可达性算法。两种算法的核心思想都是试图通过双向逼近可达状态空间,从而加快算法的收敛速度。实验结果表明,本文提出的可达性算法相对于基本的算法有了很大的提高。4)实现了两个实用的工具。模型检验技术的最终目的是应用,将理论上的算法转化为实用的工具是模型检验技术非常重要的一部分。本文实现了两个实用工具,分别支持本文提出的各个算法。工具ENu SMV是基于开源的符号化模型检验工具Nu SMV实现的,它支持本文提出的C?PR?(Counter?xample Preserving R?duction,简称C?PR?)算法、增量式的基于语义的LTL限界模型检验算法、基于语义的ETLl+f的限界模型检验算法。工具Reach是一个全新的基于SAT的符号化模型检验工具,它不仅支持本文提出的交迭的PDR算法以及并行的PDR算法,还支持其他着名的可达性算法,包括限界模型检验算法、k步归纳算法、基于插值的符号化模型检验算法以及基本的PDR算法。(本文来源于《国防科学技术大学》期刊2014-06-09）
刘万伟,王戟,王昭飞[2]（2009）在《ETL的符号化模型检验》一文中研究指出为使符号化模型检验技术适用于全部ω-正规性质,研究了ETL(extended temporal logic)的符号化模型检验方法.首先,扩展了LTL(linear temporal logic)的Tableau方法,给出了ETL的Tableau构造方法,进而给出了该方法基于BDD(binary decision diagram)的符号化实现.同时,在NuSMV的基础上实现了支持ETL符号化验证的模型检验工具ENuSMV.该工具允许用户自定义时序连接子,从而可以检验全部ω-正规性质.实验结果表明,ETL性质能够被高效地采用符号化技术加以检验.(本文来源于《软件学报》期刊2009年08期）
刘万伟[3]（2009）在《扩展时序逻辑的推理及符号化模型检验技术》一文中研究指出随着计算机软、硬件系统复杂性的日益增长,系统设计和实现的正确性越来越难以得到保证。因此,用以检验系统正确性的形式化方法亟待出现。上个世纪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。它允许用户通过描述自动机的方式自定义时序连接子,能够检验全部的ω-正规性质。(本文来源于《国防科学技术大学》期刊2009-04-01）
符号化模型检验论文开题报告
（1）论文研究背景及目的
此处内容要求：
首先简单简介论文所研究问题的基本概念和背景，再而简单明了地指出论文所要研究解决的具体问题，并提出你的论文准备的观点或解决方法。
写法范例：
为使符号化模型检验技术适用于全部ω-正规性质,研究了ETL(extended temporal logic)的符号化模型检验方法.首先,扩展了LTL(linear temporal logic)的Tableau方法,给出了ETL的Tableau构造方法,进而给出了该方法基于BDD(binary decision diagram)的符号化实现.同时,在NuSMV的基础上实现了支持ETL符号化验证的模型检验工具ENuSMV.该工具允许用户自定义时序连接子,从而可以检验全部ω-正规性质.实验结果表明,ETL性质能够被高效地采用符号化技术加以检验.
（2）本文研究方法
调查法：该方法是有目的、有系统的搜集有关研究对象的具体信息。
观察法：用自己的感官和辅助工具直接观察研究对象从而得到有关信息。
实验法：通过主支变革、控制研究对象来发现与确认事物间的因果关系。
文献研究法：通过调查文献来获得资料，从而全面的、正确的了解掌握研究方法。
实证研究法：依据现有的科学理论和实践的需要提出设计。
定性分析法：对研究对象进行“质”的方面的研究，这个方法需要计算的数据较少。
定量分析法：通过具体的数字，使人们对研究对象的认识进一步精确化。
跨学科研究法：运用多学科的理论、方法和成果从整体上对某一课题进行研究。
功能分析法：这是社会科学用来分析社会现象的一种方法，从某一功能出发研究多个方面的影响。
模拟法：通过创设一个与原型相似的模型来间接研究原型某种特性的一种形容方法。
符号化模型检验论文参考文献
[1].王瑞.基于SAT的符号化模型检验技术研究[D].国防科学技术大学.2014
[2].刘万伟,王戟,王昭飞.ETL的符号化模型检验[J].软件学报.2009
[3].刘万伟.扩展时序逻辑的推理及符号化模型检验技术[D].国防科学技术大学.2009