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

Isabelle定理证明器的剖析及其在PAR方法/PAR平台中的应用

作　者: 游珍
导　师: 薛锦云
学　校: 江西师范大学
专　业: 计算机软件与理论
关键词: 形式化方法 高可信软件 形式化验证 定理证明 高阶逻辑 交互式定理证明器 算法程序 PAR方法 PAR平台
分类号: TP311.11
类　型: 硕士论文
年　份: 2009年
下　载: 30次
引　用: 0次
阅　读: 论文下载
 

内容摘要


形式化方法可以对系统进行严格的规约,并可以从不同的角度验证开发的系统是否具有所期望的性质,在高可信软件的开发中越来越受重视。定理证明是计算机领域中形式化验证的重要研究课题,对保证软件的正确性和可靠性具有十分重要的意义。Isabelle是基于高阶逻辑的交互式定理证明工具,它具有丰富的类型系统,强大的规则库和灵活高效的命令集;它不仅支持多种对象逻辑,而且允许用户自定义新的逻辑。开发正确且高效的算法程序仍然是计算机科学中最具有挑战性的核心工作。PAR方法是薛锦云教授提出的基于分划和递推的算法程序设计方法;它是一种简单实用的支持算法程序开发全过程的形式化方法,并对于理解和证明算法程序十分有效,是算法程序设计和证明方法研究方面的重要突破。PAR平台是支撑PAR方法的CASE工具。使用定理证明工具对算法程序进行机械证明是一种发展趋势。本文分析了Isabelle定理证明器的系统结构、验证原理和核心技术;根据PAR方法/PAR平台开发算法程序的特点,探讨了如何运用Isabelle定理证明器形式化验证算法程序的工作流程,并对一些算法程序进行正确性验证;最后,阐述了如何使用Isabelle证明PAR平台中部分转换代码的正确性。本文的创新点体现在以下两个方面:1、提出了一种使用Isabelle定理证明器对算法程序进行机械验证的方法。该方法既克服了传统手工验证过程的繁琐性和易错性等缺点;又达到“提高验证效率和保证算法程序高可信”的目标,具有很好的实用价值。2、实现了Isabelle定理证明器和PAR方法/PAR平台的有机结合。一方面,算法程序的验证依赖于使用PAR方法开发的循环不变式;另一方面,使用Isabelle定理证明器验证了PAR平台中部分转换代码的正确性,从而保证了Apla程序到可执行程序转换的一致性。

全文目录


摘要  3-4
Abstract  4-8
第一章 绪论  8-15
  1.1 研究背景和意义  8-10
  1.2 相关研究情况  10-14
  1.3 主要研究工作  14-15
第二章 形式化方法和PAR 方法  15-25
  2.1 形式化方法  15-19
    2.1.1 形式化方法的研究内容  16-17
    2.1.2 形式化方法的分类  17-18
    2.1.3 形式化方法的能力和局限  18
    2.1.4 形式化方法在高可信软件开发中的重要性  18-19
  2.2 PAR 方法  19-25
    2.2.1 PAR 方法/PAR 平台简介  20
    2.2.2 算法设计语言Radl  20-22
    2.2.3 抽象程序设计语言Apla  22-25
第三章 Isabelle 定理证明器的剖析  25-37
  3.1 定理证明器的分类  25-26
  3.2 Isabelle 定理证明器的剖析  26-32
    3.2.1 Isabelle 定理证明器的特点  26-28
    3.2.2 Isabelle 定理证明器的系统结构  28-30
    3.2.3 Isabelle 定理证明器的理论  30-31
    3.2.4 Isabelle 定理证明器的证明方法  31-32
  3.3 Isabelle 定理证明器的规则/策略  32-37
    3.3.1 规则  32-35
    3.3.2 策略  35-37
第四章 Isabelle 在PAR 方法/PAR 平台中的应用  37-70
  4.1 PAR 方法开发算法程序  37-39
  4.2 算法程序正确性的证明方法  39-44
    4.2.1 Floyd 的归纳断言法  40
    4.2.2 Hoare 公理方法  40-42
    4.2.3 Dijkstra 最弱前置谓词方法  42-44
  4.3 Isabelle 验证使用PAR 方法/PAR 平台开发的算法程序  44-67
    4.3.1 Isabelle 验证算法程序的工作流程  44-46
    4.3.2 数组和算法程序的验证  46-48
    4.3.3 数组段最小和算法程序的验证  48-52
    4.3.4 Hanoi 塔非递归算法程序的验证  52-58
    4.3.5 二叉树遍历非递规算法程序的验证  58-67
  4.4 Isabelle 验证 PAR 平台中部分的转换代码  67-70
    4.4.1 选择语句转换规则的验证  67-68
    4.4.2 循环语句转换规则的验证  68-70
第五章 总结与展望  70-71
  5.1 工作总结  70
  5.2 下一步工作目标  70-71
参考文献  71-76
致谢  76-77
攻读学位期间参与的科研项目  77
攻读学位期间发表(完成)的学术论文目录  77

相似论文

  1. 基于SystemVerilog的URAT模块功能验证,TN402
  2. Web服务事务协调协议WS-TX的形式化分析与验证,TP393.09
  3. 基于PAR平台的最弱前置谓词生成器的设计与实现,TP311.11
  4. 卡箱式高速公路联网收费通行IC卡管理系统的设计与实现,TP311.52
  5. 基于Z规格的软件缺陷形式化方法,TP311.53
  6. 基于Hoare逻辑的软件形式化验证技术研究,TP311.52
  7. 基于形式化方法的统一软件模型及其应用,TP311.52
  8. 面向软件复用的组件形式化开发,TP311.52
  9. ARINC 659通信总线的设计与实现,TP336
  10. 勾股定理研究,O124.1
  11. 基于密钥链的认证邮件协议的扩展及形式化验证,TP393.08
  12. 基于串空间模型的形式化方法的扩展与应用,TP393.08
  13. 基于改进型遗传算法的面向路径测试数据生成,TP311.53
  14. UML建模的形式化方法研究和应用,TP311.52
  15. 电子商务安全协议的一种形式化分析方法,TP393.08
  16. 出具证明编译器中证明生成的研究,TP314
  17. 形式化方法的理论及其影响,B812
  18. 基于行为时序逻辑模型检测的研究与应用,TP311.52
  19. 基于SPIN/Promela的UML模型验证工具设计与实现,TP311.52
  20. EFSOS模型验证技术和反向建模方法的研究与应用,TP311.53
  21. PDA设备安全管理系统生成器的分析、设计和实现,TP311.52

中图分类: > 工业技术 > 自动化技术、计算机技术 > 计算技术、计算机技术 > 计算机软件 > 程序设计、软件工程 > 程序设计 > 程序设计方法
© 2012 www.xueweilunwen.com