基于程序骨架的软件模型验证加速方法

摘要：

模型验证作为一种形式化技术,已逐渐应用于软件系统可靠性验证.但对结构复杂的大规模软件的验证,由于状态空间爆炸往往会导致验证过程效率低甚至失败.本文针对ANSI-C软件程序的性质(正确性)验证问题,提出一种基于程序骨架的模型验证加速方法.该方法首先根据性质对源程序进行剪枝,并按照最大强连通分支压缩循环路径以抽取程序骨架,采用Hoare逻辑获取循环压缩节点的不变式,显著减小路径编码长度,将待验证性质转化为SMT一阶谓词逻辑公式,并采用SMT求解器Z3进行验证.实验结果表明抽取程序骨架后的验证效率有较大提升.

关键词： 软件工程 模型验证加速 程序骨架 路径压缩

作者: 王小龙 周宽久 勇嘉伟 任龙涛 侯刚

作者单位: 大连理工大学 软件学院,辽宁省大连市 116620 大连理工大学 软件学院,辽宁省大连市 116620;大连理工大学 软件评测中心,辽宁省大连市 116620

会议类型: 国内会议

会议名称: 2013全国高性能计算学术年会

会议地点: 桂林

会议语种:中文

页码: 736-740

在线出版日期: 2013-10-29（万方平台首次上网日期，不代表论文的发表时间）