学位论文 > 优秀研究生学位论文题录展示

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

作　者: 雷富兴
导　师: 张来顺
学　校: 解放军信息工程大学
专　业: 计算机应用技术
关键词: Hoare逻辑形式化方法程序语义程序验证最强后置条件谓词转换
分类号: TP311.52
类　型: 硕士论文
年　份: 2010年
下　载: 78次
引　用: 0次
阅　读: 论文下载

内容摘要

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

全文目录

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

相似论文

有限元法在略阳电厂边坡稳定性分析中的应用与研究,TU43
Web服务事务协调协议WS-TX的形式化分析与验证,TP393.09
卡箱式高速公路联网收费通行IC卡管理系统的设计与实现,TP311.52
基于Z规格的软件缺陷形式化方法,TP311.53
基于形式化方法的统一软件模型及其应用,TP311.52
基于程序语义的静态恶意代码检测系统的研究与实现,TP393.08
面向软件复用的组件形式化开发,TP311.52
基于串空间模型的形式化方法的扩展与应用,TP393.08
UML建模的形式化方法研究和应用,TP311.52
电子商务安全协议的一种形式化分析方法,TP393.08
出具证明编译器中证明生成的研究,TP314
一种出具证明编译器中汇编级断言和证明的生成方法,TP314
形式化方法的理论及其影响,B812
基于行为时序逻辑模型检测的研究与应用,TP311.52
基于SPIN/Promela的UML模型验证工具设计与实现,TP311.52
Isabelle定理证明器的剖析及其在PAR方法/PAR平台中的应用,TP311.11
验证带有线程动态创建和退出多线程程序,TP311.53
THP事务协调协议的形式化分析与验证,TP311.52
基于PVS的自稳定算法形式化分析,TP338.8
关于密码协议的形式化分析方法的研究,TP393.08