检索结果-南通市图书馆

基于谓词抽象的C语言程序安全性验证方法研究

在线全文

学校读者我要写书评

暂无评论

基于谓词抽象的C语言程序安全性验证方法研究

作者：梁皓伟天津理工大学

学位级别：硕士

随着软硬件系统规模的不断扩大和功能的日益强大,软件安全问题日益严重。模型验证从数学定理的角度提供了一种新的验证方式,但会造成状态空间爆炸的问题。一直以来,状态空间爆炸问题严重影响了软件验证的进一步发展和应用,成为该研究方... 详细信息

随着软硬件系统规模的不断扩大和功能的日益强大,软件安全问题日益严重。模型验证从数学定理的角度提供了一种新的验证方式,但会造成状态空间爆炸的问题。一直以来,状态空间爆炸问题严重影响了软件验证的进一步发展和应用,成为该研究方向的瓶颈。Impact算法是懒抽象算法的具体实现。同谓词抽象相比,算法的精炼部分不再将谓词存储为全局存储,而是将其映射到状态节点。这样,在下一次迭代中,算法不需要重新启动,而是基于上次迭代结果,从靠近错误的节点的循环头重新开始。但是,这项技术仍然存在一些不足。首先,在验证过程中,Impact不区分断言表达式。当断言变量绑定的逻辑关系影响到后续的Impact覆盖行为,验证模型的收敛速度就会被减缓。其次,算法在求解谓词时完全依赖克雷格插值求解器,然而插值求解器的求值细节是不可见的,即插值结果是不可预测的,所以经常会得到低效的插值。这会导致算法无法终止并无限期的继续执行。为了弥补Impact的不足,本文从C程序的解析入手,分析了C程序的抽象语法树,构建了程序转移模型。在转移模型中,对断言表达式的逻辑关系进行分类。一旦确定表达式是单变量逻辑关系,立即向精炼部分发送信号,提示需要在精炼过程中对表达式进行逻辑分析,以消除断言表达式对插值的影响。基于插值器对路径中变量敏感的事实,本文提出了一种基于辅助表达式的优化验证算法。该算法使用跟踪变量方法在代码中插入跟踪表达式。从插值计算的角度来看,该方法通过替换输入参数来影响插值结果,从而获取高效的插值。对于程序功能而言,该方法保持了原有的程序表达式。在本文的最后,对所提出的基于辅助表达式优化验证算法进行了实验验证。实验结果表明,该算法在保证正确率的前提下,减少了验证过程中的内存消耗,缩短了验证时间。

关键词：模型验证克雷格插值谓词抽象懒抽象

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

基于谓词抽象的测试用例约简生成方法

通信学报 2012年第3期33卷 35-43,51页

作者：郭曦张焕国武汉大学计算机学院湖北武汉430072 武汉大学空天信息安全与可信计算教育部重点实验室湖北武汉430072

针对大规模软件系统状态迁移数量庞大,容易导致状态空间爆炸的问题,提出一种基于谓词抽象的测试用例约简生成方法,该方法依据给定的谓词集合对软件系统的状态空间进行等价类划分,通过状态集合之间的映射得到约简的抽象状态,并以抽象状... 详细信息

针对大规模软件系统状态迁移数量庞大,容易导致状态空间爆炸的问题,提出一种基于谓词抽象的测试用例约简生成方法,该方法依据给定的谓词集合对软件系统的状态空间进行等价类划分,通过状态集合之间的映射得到约简的抽象状态,并以抽象状态之间的迁移关系作为测试用例约简生成的基础。实验结果表明,该方法可以有效地对系统状态进行约简,并生成规模较小的测试用例集。

关键词：谓词抽象状态约简等价类划分测试用例生成

基于符号模拟和约束逻辑编程的RTL级Verilog谓词抽象方法

在线全文

学校读者我要写书评

暂无评论

计算机学报 2007年第7期30卷 1138-1144页

作者：李暾屈婉霞郭阳刘功杰李思昆国防科学技术大学计算机学院

利用人工智能最新研究成果——约束逻辑编程对Verilog描述进行谓词抽象,并与目前基于SAT的方法进行了比较．首先通过符号模拟建立Verilog的形式化模型,然后结合要抽象的谓词,将谓词抽象问题转化为约束逻辑编程问题并进行求解．该方法的... 详细信息

利用人工智能最新研究成果——约束逻辑编程对Verilog描述进行谓词抽象,并与目前基于SAT的方法进行了比较．首先通过符号模拟建立Verilog的形式化模型,然后结合要抽象的谓词,将谓词抽象问题转化为约束逻辑编程问题并进行求解．该方法的优点是在计算抽象系统时,不需要像基于SAT的方法那样将字级约束打散成位级约束,求解效率显著提高;提供了一个统一的框架用于描述各种约束．实验结果表明,与基于SAT的抽象技术相比,基于约束逻辑编程的抽象方法的求解速度有显著提高．

关键词：谓词抽象 Verilog约束逻辑编程模型检验符号模拟

在线全文

学校读者我要写书评

暂无评论

谓词抽象和“弗雷格之谜”

学术研究 2014年第10期 23-28,159页

作者：邓雄雁秦波胡泽洪华南师范大学政治与行政学院博士后流动站华南师范大学政治与行政学院

弗雷格认为"相等"问题需要考虑涵义和意谓两个因素,这个问题包含相等的必然性、同一保真替换有效性和空词项三方面的问题。这些之所以成为问题,原因在于缺乏一个有效手段对"相等"的从言和从物形式进行区分,并误认为内涵和外延是截然对... 详细信息

弗雷格认为"相等"问题需要考虑涵义和意谓两个因素,这个问题包含相等的必然性、同一保真替换有效性和空词项三方面的问题。这些之所以成为问题,原因在于缺乏一个有效手段对"相等"的从言和从物形式进行区分,并误认为内涵和外延是截然对立的。引入谓词抽象,可以穿透内涵语境,把涵义和意谓衔接起来,对模态从言和从物形式进行区分,并刻画词项的不同指称方式,从而完成对"相等"问题的三方面考察。

关键词：弗雷格相等从言模态从物模态谓词抽象

在线全文

学校读者我要写书评

暂无评论

谓词抽象和模态谓词逻辑的合法性

世界哲学 2014年第2期 139-145页

作者：邓雄雁胡泽洪华南师范大学政治与行政学院

奎因对模态谓词逻辑的合法性持怀疑态度,他从逻辑角度论证了模态语境是指称不明的,同一替换原理和存在概括规则在模态语境中都是无效的,他的批评影响很大。但是,若在模态谓词逻辑中引入谓词抽象,它可以表达所有模态从言和从物命题,还能... 详细信息

奎因对模态谓词逻辑的合法性持怀疑态度,他从逻辑角度论证了模态语境是指称不明的,同一替换原理和存在概括规则在模态语境中都是无效的,他的批评影响很大。但是,若在模态谓词逻辑中引入谓词抽象,它可以表达所有模态从言和从物命题,还能有助于区分严格指示词和非严格指示词的模态意义。同一替换和存在概括都有从言和从物形式,可是奎因没有注意到这些重要区别,所以,奎因的论点是以偏概全的,其论证并不真正构成对模态谓词逻辑发展的威胁。

关键词：模态逻辑谓词抽象从言模态从物模态严格指示词

在线全文

学校读者我要写书评

暂无评论

谓词抽象:一种新型语言辖域装置

科学技术哲学研究 2012年第5期29卷 47-52页

作者：魏燕侠华侨大学哲学与社会发展学院福建厦门361021 厦门大学哲学系福建厦门361005

自然语言歧义所产生的哲学问题在语言哲学史上占据着重要位置。罗素的摹状词理论中包含着一种基于经典逻辑的语言辖域装置,它解决了"排中律失效"问题。作为一种基于量化模态逻辑的新型语言辖域装置,谓词抽象可以解决包括奎因的"指称晦... 详细信息

自然语言歧义所产生的哲学问题在语言哲学史上占据着重要位置。罗素的摹状词理论中包含着一种基于经典逻辑的语言辖域装置,它解决了"排中律失效"问题。作为一种基于量化模态逻辑的新型语言辖域装置,谓词抽象可以解决包括奎因的"指称晦暗语境"以及"信念之谜"在内的模态逻辑语境下的语言歧义问题。在问题的适用域上,谓词抽象优越于罗素的辖域装置。谓词抽象还有着广阔的哲学应用前景和进一步的研究价值。

关键词：谓词抽象语言歧义辖域装置摹状词

在线全文

学校读者我要写书评

暂无评论

谓词抽象技术中循环反例的解决方法研究

计算机工程与设计 2010年第24期31卷 5269-5272,5277页

作者：梁加宾张来顺解放军信息工程大学电子技术学院河南郑州450004

为了解决谓词抽象技术面临的程序中循环体的每次迭代都至少需要一个谓词来实现的难题,提出了一个两阶段的不完全判定过程,用来对一个包含循环的反例进行可行性模拟。通过给出的循环探测算法来从抽象模型中提取出包含循环的反例,并用循... 详细信息

为了解决谓词抽象技术面临的程序中循环体的每次迭代都至少需要一个谓词来实现的难题,提出了一个两阶段的不完全判定过程,用来对一个包含循环的反例进行可行性模拟。通过给出的循环探测算法来从抽象模型中提取出包含循环的反例,并用循环迭代的数量作为参数来确定模拟实例。实验结果表明,该方法在典型的缓冲溢出实例中的表现优于传统的抽象求精方法。

关键词：模型检测谓词抽象求精反例循环

在线全文

学校读者我要写书评

暂无评论

葛梯尔型反例的谓词抽象式解答方案

学术研究 2015年第11期 25-30页

作者：魏燕侠华侨大学哲学与社会发展学院

葛梯尔问题是当代知识论的核心问题,层出不穷的葛梯尔型反例使葛梯尔问题的解答蒙上了阴影。对葛梯尔型反例进行逻辑分析,体现了葛梯尔问题研究的最新动向。包括葛梯尔第一反例在内的一批葛梯尔型反例,是自然语言的辖域歧义导致的语言... 详细信息

葛梯尔问题是当代知识论的核心问题,层出不穷的葛梯尔型反例使葛梯尔问题的解答蒙上了阴影。对葛梯尔型反例进行逻辑分析,体现了葛梯尔问题研究的最新动向。包括葛梯尔第一反例在内的一批葛梯尔型反例,是自然语言的辖域歧义导致的语言问题。谓词抽象从句法和语义两个方面将自然语言表达的歧义命题加以澄清,从而表明这类葛梯尔型反例之所以构成了对传统知识三元定义的挑战,乃是出于对自然语言的歧义命题不全面理解基础之上的。

关键词：葛梯尔型反例谓词抽象语言辖域问题

在线全文

学校读者我要写书评

暂无评论

不可满足子式在谓词抽象中的应用与分析

计算机应用 2014年第A1期34卷 273-276页

作者：张建民黎铁军张峻庞征斌李思昆国防科学技术大学计算机学院长沙410073

随着软硬件设计的规模越来越大,功能越来越复杂,往往导致形式化验证出现"组合爆炸"问题,而谓词抽象方法是解决状态空间"组合爆炸"问题的重要技术之一。面向硬件的谓词抽象方法是不可满足子式的典型应用,通过求解不可满足子式,能够减少... 详细信息

随着软硬件设计的规模越来越大,功能越来越复杂,往往导致形式化验证出现"组合爆炸"问题,而谓词抽象方法是解决状态空间"组合爆炸"问题的重要技术之一。面向硬件的谓词抽象方法是不可满足子式的典型应用,通过求解不可满足子式,能够减少谓词抽象过程中精化迭代的次数,从而提高形式化验证效率。针对微处理器的指令Cache部件,将两种最小不可满足子式的求解算法进行了比较,结果表明贪心遗传算法在运行效率方面优于分支-限界算法。并且深入分析了不可满足子式在硬件谓词抽象中的作用,以及如何加速芯片的形式化验证过程。

关键词：功能验证形式化方法谓词抽象布尔可满足性最小不可满足子式