基于Hoare逻辑的软件形式化验证技术研究

发布时间：2022-04-28 21:20

　　随着软件规模越来越大,软件安全性越来越引起开发人员的关注,而现有的编程语言以及软件开发方法所能提供的安全性保证是脆弱和不可靠的,例如,通过标准的软件工程方法和大量的测试能够减少软件漏洞产生,但是即使经过高强度测试的软件,我们也不能保证其没有漏洞,并且这些方法不具有可再现性。已有的软件工程方法对软件安全性的提高已经越来越微弱,而基于Hoare逻辑的程序形式化验证方法能为软件安全性提供可靠保证。本文针对目前程序验证的不可再现性,基于Hoare逻辑中最强后置条件谓词转换,给出了一些可重现的形式化技术和方法求解代码语义,其解决了程序验证的可应用性与可重现性。首先,通过分析推导程序语义的形式化方法,讨论在求解赋值语句最强后置条件中存在的自动化方面的问题。给出赋值语句最强后置条件的一个新定义,使用这个定义即不需求解反函数,也无需引入一个新变量就能自动化地求解赋值语句的最强后置条件。其次,针对求解循环程序语义时需事先知道循环深度这一缺陷,给出了一种求解命令式循环程序语义及其执行和终止条件的方法。该方法包括直接从代码本身进行循环执行和终止条件的算法推导,并可将推出的循环语义信息应用到程序验证和缺陷修正... 

【文章页数】：75 页

【学位级别】：硕士

【文章目录】：
摘要
Abstract
第一章绪论
    1.1 研究背景
    1.2 论文的应用价值
    1.3 论文的组织结构
第二章 相关技术分析
    2.1 Hoare 逻辑
        2.1.1 逻辑正确性概念
        2.1.2 部分正确性证明规则
    2.2 形式化符号表示
        2.2.1 项及公式
        2.2.2 函数
        2.2.3 其他符号约定
    2.3 确认与验证
        2.3.1 形式化验证方法
        2.3.2 软件测试
        2.3.3 软件审查
    2.4 最强后置条件谓词转换
        2.4.1 赋值语句的最强后置条件
        2.4.2 顺序结构的最强后置条件
        2.4.3 分支结构的最强后置条件
        2.4.4 迭代结构的最强后置条件
        2.4.5 过程调用的最强后置条件
        2.4.6 变量声明的最强后置条件
    2.5 本章小节
第三章 基于Hoare 逻辑的循环程序验证技术研究
    3.1 引言
    3.2 迭代不变式
        3.2.1 差分方程
        3.2.2 迭代相关性的表示方法
        3.2.3 求解迭代不变式
    3.3 循环执行条件的研究
        3.3.1 简单循环条件
        3.3.2 复杂循环条件
    3.4 循环终止条件研究
    3.5 本章小节
第四章 基于Hoare 逻辑的过程验证技术研究
    4.1 引言
    4.2 过程和过程调用规则
    4.3 提取过程语义
    4.4 过程调用的语义
        4.4.1 参数代换
        4.4.2 检验过程的前置条件
        4.4.3 过程调用的最强后置条件
    4.5 Hoare 逻辑在函数验证中的应用
    4.6 本章小节
第五章 基于Hoare 逻辑的程序验证技术的应用
    5.1 引言
    5.2 公理证明法
        5.2.1 使用R_(k+1) 证明程序部分正确性
        5.2.2 识别不一致性
        5.2.3 直接证明方法
    5.3 基于功能理论的正确性证明方法
    5.4 本章小节
第六章 总结与展望
    6.1 本文的工作总结
    6.2 下一步工作展望
参考文献
作者简历 攻读硕士学位期间完成的主要工作
致谢



本文编号：3649554