基于谓词抽象的软件安全性验证
本文应用模型检验方法对软件进行验证要解决软件的无穷状态空间问题，提出的谓词抽象方法将软件无穷的状态空间抽象为基于一组谓词表示的有限状态自动机，抽象过程使用最弱前置条件和定理证明工具直接对软件源代码自动进行，并能保证如果待验证的安全性质在抽象模型中满足，则其在程序中也满足。谓词抽象的精度取决于所选用的谓词集合，验证过程使用了基于反例的抽象精化思想，利用验证产生的伪反例路径推断出新的谓词不断精化模型，从而可以全自动地完成对程序安全性质的验证。
谓词抽象 模型检验 抽象精化 软件安全性
易晓东 杨学军
国防科技大学计算机学院，湖南长沙410073
国内会议
武汉
中文
2005-10-13（万方平台首次上网日期，不代表论文的发表时间）