学位论文 > 优秀研究生学位论文题录展示
基于时间逻辑的程序正确性验证
作 者: 王知远
导 师: 王树义
学 校: 大连理工大学
专 业: 计算机应用技术
关键词: 时间逻辑 编译原理 程序正确性
分类号: TP311.53
类 型: 硕士论文
年 份: 2009年
下 载: 80次
引 用: 0次
阅 读: 论文下载
内容摘要
目前计算机软件的发展受着多种因素的影响,它滞后于硬件,其安全性、可靠性和稳定性一直是人们关注的几个重要问题。随着软件的大型化、模式化,以及安全性需求的日益提高,人们对软件质量的要求起来越高,尤其是对软件的正确性要求。软件质量问题由来已久,由于在许多关键领域运行的软件质量问题而引发重大损失甚至灾难并不少见。基于调试的方法有很大的局限性。在一些经过调试并投入运行的系统程序或应用程序中还存在着隐患。因此,为了保证程序的正确性,必须从理论上研究有关程序的正确性证明的方法。计算机科学家用完全形式化的方法来证明程序同功能归约的一致性,保证程序的正确性。形式化证明把程序完全正确性问题归结为部分正确性和终止性的证明。本文提出了一种新的基于形式化理论的程序自动验证方向:即在程序抽象证明中引入时间逻辑。时间逻辑是在一阶逻辑的基础上通过显式地引进时间变量而得到的一种逻辑。本文用这种逻辑描述程序设计语言各个语言成分的语义,验证程序的性质,以及软件规范。结合利用编译技术实现的编译器,针对C语言类型定义、变量定义、运算符、表达式、语句、函数定义及函数调用的语义,将源程序翻译为时间逻辑公式。最后利用数学原理证明程序性质和规范是否符合需求分析和设计阶段所要达到的目标。本文以ANSI C程序为输入对象,详细描述了该编译器的词法分析、BISON生成的语法分析、语义分析、语法树生成等模块的构造与实现,并给出时间逻辑公式验证的几种证明模式。
|
全文目录
摘要 4-5 Abstract 5-8 1 绪论 8-15 1.1 研究背景 8-12 1.1.1 程序验证概述 8-11 1.1.2 运用编译技术的优点 11-12 1.2 国内外研究发展与现状 12-13 1.3 本文研究目的及主要工作 13-14 1.4 论文章节安排 14-15 2 时间逻辑 15-21 2.1 时间逻辑语言 15-16 2.2 归结原理 16-21 2.2.1 子句集 17 2.2.2 命题逻辑中的归结原理 17-18 2.2.3 替换与合一 18 2.2.4 谓词逻辑中的归结原理 18-21 3 程序设计语言的公理语义 21-41 3.1 类型定义的语义 21-23 3.2 变量定义的语义 23-24 3.3 运算符和表达式的语义 24-28 3.4 语句的公理语义 28-36 3.5 函数定义的公理语义及函数规范 36-37 3.6 函数调用的公理语义 37-39 3.7 有关公理 39-41 4 翻译 C程序成时间逻辑公式的过程 41-59 4.1 词法分析 42-46 4.2 语法分析 46-53 4.2.1 语法分析技术 47-49 4.2.2 语法分析的实现 49-52 4.2.3 BISON输出程序的分析 52-53 4.3 语义分析 53-56 4.3.1 语义分析概述 53-56 4.3.2 语义分析实现 56 4.4 符号表 56-59 5 基于时间逻辑的程序验证 59-68 5.1 一般原理 59-61 5.2 验证实例 61-64 5.3 证明模式 64-68 结论 68-69 参考文献 69-71 攻读硕士学位期间发表学术论文情况 71-72 致谢 72-73
|
相似论文
- 基于PAR平台的最弱前置谓词生成器的设计与实现,TP311.11
- B/S模式C语言考试及自动评分系统的研究与实现,TP311.52
- 基于特征自生成的畸形SIP信令检测技术的研究与实现,TN916.2
- 基于多轴数控加工运动仿真的编译技术研究,TG659
- 基于GCC的C++静态分析器的开发,TP311.52
- 基于电路的虚拟实验研究,TP311.52
- 基于正规表达式的程序阅卷系统设计与实现,TP311.52
- 基于XML的程序设计自动批改的研究,TP311.11
- 基于树结构的代码改进工具设计与实现,TP311.52
- C语言上机考试及自动评分系统的研究与实现,TP311.52
- 面向应用的编译原理实验系统的设计与实现,TP314
- 实时绘制语言的研究,TP391.41
- 基于符号计算方法的程序验证技术研究,TP311.1
- C++代码缺陷检测系统的研究与设计,TP311.53
- 一种于经验数据的软件缺陷修复工作量预测模型研究,TP311.53
- 探索式测试方法在网络游戏软件测试中的应用,TP311.53
- 基于系统调用依赖图的程序相似性研究,TP311.53
- 基于GA的软件测试用例自动生成技术研究,TP311.53
- 基于WATIR和STAF的自动化测试的设计与实现,TP311.53
- 多媒体教学系统的功能测试与执行,TP311.53
- 面向对象分层测试的方法研究,TP311.53
中图分类: > 工业技术 > 自动化技术、计算机技术 > 计算技术、计算机技术 > 计算机软件 > 程序设计、软件工程 > 软件工程 > 软件维护
© 2012 www.xueweilunwen.com
|