循环不变式生成方法研究与改进

论文摘要

软件作为信息系统的实现载体,广泛应用在各个领域,软件中的任何安全漏洞或错误的实现都可能导致非常严重的后果。通过大量的测试可以提高软件的可靠性,但成本较高,也不能完全保证软件的可靠。形式化证明方法基于严密的数学和逻辑基础,经过正确性证明的程序可以保证软件符合指定的程序规范,从而大大提高软件可靠性。程序正确性证明的一个关键问题是发现充分的循环不变式信息来辅助、支撑证明过程的完成。由人工寻找循环不变式工作繁琐,容易出错。因此,研究如何自动地有效分析和生成循环不变式,使得软件证明过程顺利完成,成为形式化方法研究领域的一个重要研究课题。本文主要针对软件验证技术中的循环不变式生成技术进行研究和实现：（1）对形式化程序分析方法主要理论进行总结。本文根据形式化分析中用到的主要理论的不同对形式化分析技术进行总结。对各自的理论核心、主要解决的问题、典型工具进行了阐述。在此基础上,指出形式化证明过程的难点,并总结了当前克服这些难点所采用的方法。（2）介绍和总结了目前求解循环不变式的主要研究状况和现有方法。根据他们主要理论和适用范围的不同进行阐述,指出了目前工作存在的不足。（3）本文提出了一种基于条件赋值转换和自适应模板技术的循环不变式生成方法。根据程序控制流结构、依赖分析结果和值分析结果,生成可能的循环不变式,然后由定理证明器求解。该方法可以自动地运行,并将结果以ACSL注释的形式添加到程序中,辅助完成程序属性的证明过程。（4）基于上述方法,在Frama-C平台和APRON库的基础上,实现了一个分析插件loopInv。选取了一些程序作为分析对象,与其他方法作了比较,结果表明可以发现更多的不变式,使一些程序规范顺利得到证明。

论文目录

• 摘要
• Abstract
• 目录
• 图片目录
• 表格目录
• 第一章 引言
• 1.1 研究背景
• 1.2 研究内容
• 1.3 本文组织
• 第二章 程序分析的基本概念和方法
• 2.1 基本理论
• 2.1.1 研究对象
• 2.1.2 常用概念
• 2.2 主要方法
• 2.2.1 模型检测
• 2.2.2 定理证明
• 2.2.3 符号执行
• 2.2.4 谓词抽象
• 2.3 难点
• 2.3.1 循环的处理方法
• 2.3.2 分支的处理方法
• 2.3.3 数组的处理方法
• 2.4 本章小结
• 第三章 循环不变式生成技术研究
• 3.1 基于迭代不动点计算
• 3.2 基于参数化模板
• 3.2.1 示例演示
• 3.3 基于机器学习的方法
• 3.4 基于实际执行的方法
• 3.5 本章小结
• 第四章 循环不变式生成技术改进
• 4.1 改进动机
• 4.2 处理过程
• 4.2.1 预处理
• 4.2.2 收集信息
• 4.2.3 分析计算
• 4.3 转换系统
• 4.4 条件赋值转换
• 4.5 自适应模板生成
• 4.6 本章小结
• 第五章 Iooplnv插件的设计与实现
• 5.1 平台介绍
• 5.1.1 ACSL
• 5.1.2 CIL
• 5.1.3 Frama-C
• 5.1.4 APRON
• 5.2 系统框架
• 5.3 技术细节
• 5.3.1 主要算法
• 5.3.2 验证与输出
• 5.4 优化措施
• 5.5 开发环境
• 5.6 本章小结
• 第六章 实验过程与结果
• 6.1 实验对象
• 6.2 实验结果与分析
• 6.3 本章小结
• 第七章 结论与展望
• 7.1 本文工作的创新点和主要成果
• 7.2 未来工作和展望
• 参考文献
• 攻读硕士学位期间参与的科研项目
• 攻读硕士学位期间完成的论文
• 致谢