谓词抽象技术研究?

随着软、硬件系统规模和功能的不断扩充,状态空间爆炸问题严重影响了模型检验的进一步发展与应用,成为验证大规模系统的瓶颈.谓词抽象是解决状态空间爆炸的最有效方法之一,近年来得到迅速发展.介绍了谓词抽象的基本算法并比较了不同的求解支持工具;重点分析了反例指导的抽象求精和基于插值的抽象求精原理;分析了产生新谓词的各种方法的优、缺点;最后指出了谓词抽象技术进一步发展所面临的挑战和发展方向.

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

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

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

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

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

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

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

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

针对Java语言中间形式的谓词抽象算法

谓词抽象是解决软件模型检查中状态空间爆炸的最有效方法之一,针对Java语言面向对象的特性,描述了一种对Java程序语言中间形式的谓词抽象算法,该算法将Java程序抽象成为布尔程序,抽象过程中处理的Java数据结构包括:赋值语句、条件语句、类对象引用、成员方法和方法调用等。用一个Java程序实例说明了该算法的抽象过程和结果。

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

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

基于SAT的程序谓词抽象技术研究

软件模型检验面临的难题是状态空间爆炸问题。解决此问题的重要方法是谓词抽象。在传统的反例导向精化方法中,谓词抽象是通过调用定理证明器计算抽象程序,然而计算效率不高,因此引入了SAT求解器计算抽象程序。通过具体迁移关系的布尔公式构造,用SAT计算抽象程序的方法,包括基本块和控制流语句抽象迁移关系的构造,完成基于SAT抽象程序构造方法的优势。实例分析表明,基于SAT的谓词抽象技术是一种构造程序抽象模型更高效的方法。

一种面向Web服务源程序的谓词抽象验证方法

Web服务作为一种典型的分布式计算技术,常用于跨平台跨组织的分布式环境,因此保证其安全性就显得十分重要。作为一种形式化验证方法,模型检测可以验证并发与分布式系统的安全性。现有形式化方法的验证对象多为Web服务高层描述语言,而针对Web服务底层执行程序的验证工作则较少。提出一种面向Web服务源程序的验证方法,采用谓词抽象技术,将源程序转化为抽象模型,最后通过实验说明此方法的可行性。

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

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

模型检验中抽象技术研究综述

在模型检验中,抽象技术是解决状态空间爆炸问题的有效方法之一。论文描述了模型检验对抽象模型的基本要求,给出了抽象模型的定义及其评价指标,对抽象技术和自动化的抽象精化技术的主要方法及其研究进展作了比较深入、全面的综述,并讨论了抽象技术今后的发展方向。

基于抽象和搜索空间划分的安全性判定方法

为满足访问控制策略安全性快速判定的要求,提出一种基于谓词抽象和验证空间划分的访问控制策略状态空间约减方法,将在访问控制策略原始状态机模型上的安全性分析工作转移到包含较少状态的抽象模型上,并进一步划分抽象模型的验证空间,以提高效率。理论分析和实验数据均表明,其安全性分析所需的时间和空间都得到有效约减。与传统方法相比,它具有速度更快、自动化程度更高等优点。

一种基于抽象与精化技术的Web服务组合验证方法

模型检测因其自动化程度高、能够提供反例路径等优势,被广泛应用于Web服务组合的兼容性验证。本文针对模型检测过程中存在的状态爆炸问题,在传统的模型检测方法中引入谓词抽象和精化技术,提出了一种针对Web服务组合的抽象精化验证框架。使用谓词抽象技术对原子Web服务抽象建模,将各Web服务抽象模型组合成组合抽象模型;将模型检测后得到的反例在各原子Web服务上做投影操作,对投影反例进行确认;对产生伪反例的Web服务抽象模型进行精化,生成新的组合抽象模型,再次对性质进行验证。最后通过实例分析说明基于抽象精化技术的Web服务组合验证框架在缓解状态爆炸问题上的可行性。

关于C语言程序安全验证中K-归纳法的改进

过去几年中,程序验证技术在学术界和工业界获得了越来越多的青睐。K-归纳法是一种著名的软件模型检查技术,其结合了有界模型检查和归纳法来验证程序安全。许多软件验证工具已经将其实现。该方法在有限的时间内展开循环,通过归纳的方式验证整个状态空间。然而,当安全属性在循环结构之外被断言时,K-归纳法只需要检查最后一个循环状态的可满足性,而不是整个状态空间。在这种情况下,K-归纳法必须完全展开循环以获得最后的状态。如果循环很大或者不是确定性的,这个方法就不能及时完成验证。为了扩大K-归纳法的应用范围,文中在K-归纳法中引入谓词抽象和反例引导的抽象精炼(counter-example guided abstraction refinement,CEGAR)。改进后的方法将验证域从一个特定的状态过渡到一个抽象集,并在出现反例时使用CEGAR精炼验证域。实验结果表明,对于具有环外安全特性的程序,该组合方法提高了K-归纳法的有效性和效率。

基于抽象-验证-细化范例的软件模型检测

如何保证软件系统的正确性和可靠性是当前软件开发面临的主要问题之一。模型检测作为一种重要的自动化验证技术在软件的分析与验证中正取得越来越多的成功。本文以微软的SLAM和加州大学伯克利分校的BLAST为例综述性地介绍了基于抽象-验证-细化范例的软件模型检测。

三值自由模态逻辑FML

FML是以自由逻辑为基础构建起来的一个三值模态谓词逻辑表列系统。若一个词项无所指(空词项)则包含该词项的简单句子无所指(即无真值),FML的偏函数语义模型体现了这一思想。通过借鉴普利斯特的一度衍推系统和菲汀的抽象谓词思想,FML系统刻画了在内涵语境下关于空词项的推理规律。最后,用数模的方法证明了FML的强完全性。

循环不变式开发技术研究

高可靠性软件是当今软件开发的热点问题。确保算法程序逻辑结构正确最理想的途径是算法程序的形式化推导和证明,而循环不变式是算法程序形式推导和证明的关键。循环不变式的开发一直是算法程序设计领域中最具挑战性、最富有创造性、也是最困难的问题之一。本文研究了众多现有循环不变式开发方法中较为典型的几种方法,指出了它们的基本原理、技术难点、特点及效果,旨在探寻循环不变式本质特征,从而为研究更简单、有效的生成方法提出指导。

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

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

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

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

奎因与量化模态逻辑的发展

奎因在20世纪40年代提出解释量化模态逻辑的问题,认为不能把标准量化与模态结合起来。逻辑学家尝试了各种解决方案。由于克里普克语义的广泛应用,逻辑学家找出了一些量化模态逻辑系统,并给出相应语义解释和完全性,使特定的模态系统具有正确的句法和语义,因此部分回答了奎因提出的挑战。另一方面,人们从哲学上提出各种不同的对"模态个体"的说明。我们详细讨论奎因提出的问题,简要说明量化模态逻辑的发展。最后的结论是,虽然关于量化和模态的关系的技术处理取得了大量有意思的结果,但从哲学上看,我们仍然需要一种对模态个体、内涵、同一等概念的恰当解释。