论文题目: 程序正确性验证的几个问题
论文类型: 博士论文
论文专业: 应用数学
作者: 范年柏
导师: 周叔子,张大方
关键词: 形式化验证,统一建模语言,模型检验,函数式语言,副作用,抽象数据类型,类别代数,图灵机
文献来源: 湖南大学
发表年度: 2005
论文摘要: 计算机软件的发展受着许多因素的影响,它滞后于硬件,其安全性、可靠性和稳定性一直是人们关注的几个重要问题。 随着大型软件的快速发展,以及安全性要求极高的航天航空技术的需要,人们对软件质量的要求起来越高,尤其是对软件的正确性要求,因而出现了软件的正确性验证与测试两个重要领域。软件的正确性验证讨论的是确保程序是没有错误的,并且满足用户需求,软件测试则是要找出程序中存在的错误,两者有着本质的区别,也有着密切的联系,它们贯穿软件的整个生命周期。人们在不同的领域构造了许多不同的模型,如:可计算函数模型、谓词演算模型、代数模型等。不同的模型适用于不同的范围,它们在一定的范围内解决了许多问题,但都存在一定局限性,当然试图用一种模型解决复杂的软件可靠性问题也是不现实的。程序的实质是有限状态机FSM,本文将对几种不同的状态机模型进行讨论,从传统的FSM到目前流行的UML(Unifled Modeling Language)状态机,并给出一个状态机的矩阵模型,从而可用纯数学的方法讨论计算机领域中的有关问题,在此基础上,可得到相应的代数性质,并借助完善的代数理论对计算机领域所关心的代数问题,例如:可靠性问题、完备性问题及可解性问题等进行讨论;同时,本文也将借助面向对象的程序设计理论,讨论UML语言扩展机制,从设计的源头入手研究程序的正确性问题。 本文将针对以下几个方面,进行程序正确性的讨论: 1.程序正确性的定义:长期以来,人们对程序的正确性的定义一直未给出准确的陈述,本文将对此进行必要的讨论,从而可克服长期以来形成的某些误区。 2.模型的正确性:针对用例、UML的状态机进行一些讨论,用例不仅用于测试,同时也用于建模。用例规模往往很大,使得测试、建模很困难,本文将对栈的用例规模进行讨论,并得到一个递归推导公式;UML的状态机不同于传统的FSM,本文试图将两者结合起来用于建模,这样将更利于编制高效而又可靠的程序。 3.类型与类型系统的正确性:类型系统是算法语言的一个组成部分,它监视程序中变量的类型,包括所有表达式的类型;类型检验是保证程序正确性的重要手段。本文将对类别代数中经典的有限基问题进行讨论,从而可得到具有共轭可置换代数具有有限基的结论;另外利用图灵机的矩阵模型给
论文目录:
摘要
Abstract
第1章 绪论
1．1 研究背景
1．2 程序正确性验证概述
1．3 本文结果与创新点
1．3．1 程序的正确性的定义
1．3．2 正确性的证明方法
1．4 论文的结构
第2章 关于程序的正确性的讨论
2．1 程序的正确性(Correctness)的概念
2．1．1 语法正确性
2．1．2 语义正确性
2．2 程序正确性的验证方法
2．2．1 静态类型检查与测试
2．2．2 利用逻辑推理对程序结构的正确性进行验证
2．2．3 程序正确性验证的其他方法
2．3 小结
第3章 类型系统与类别代数
3．1 类型系统介绍
3．2 类别代数与出错处理
3．3 一个具有有限基的代数
3．4 利用Turing机停机问题的不可判定性解决代数系统的不可解性
3．5 类型系统可靠性的一个条件
3．5．1 不含空类型的可靠性与完备性
3．5．2 含空类型的可靠性
3．6 小结
第4章 算法语言中表达式的副作用问题
4．1 算法语言的指称语义
4．2 强制型语言中表达式的副作用问题
4．3 函数式语言中表达式副作用问题
4．4 小结
第5章 形式化工程的建模及验证
5．1 UML状态图简介
5．1．1 类图
5．1．2 状态图
5．1．3 利用状态图进行程序设计
5．2 基于状态图的正确性验证
5．2．1 设计栈操作的交互式状态机
5．2．2 正确性验证
5．3 基于栈操作用例规模的一个计算公式
5．4 小结
结论
参考文献
附录A：攻读博士学位期间发表的学术论文
附录B：一个抽象数据类型的说明(类C语言描述)
附录C：攻读博士学位期间参与的主要科研项目
致谢
发布时间: 2006-05-10
相关论文
- [1].面向UML的模型检验研究[D]. 董威.中国人民解放军国防科学技术大学2002
- [2].并发系统的模型检测与测试[D]. 吴鹏.中国科学院研究生院（软件研究所）2005
- [3].基于UML的软件统计测试研究[D]. 颜炯.国防科学技术大学2005
- [4].模型检验的反例解释[D]. 沈胜宇.国防科学技术大学2005
- [5].基于接口自动机的组合验证方法研究[D]. 文艳军.国防科学技术大学2005
- [6].依赖性分析及其在软件测试中的应用[D]. 缪力.湖南大学2006
- [7].高可信软件可靠性和防危性测试与评价理论研究[D]. 覃志东.电子科技大学2005
- [8].软件测试与可靠性评估[D]. 张广梅.中国科学院研究生院（计算技术研究所）2006
- [9].基于逻辑的程序验证方法在高可信软件开发上的应用[D]. 项森.中国科学技术大学2006
- [10].面向C程序验证的切片执行方法[D]. 易晓东.国防科学技术大学2006
标签：形式化验证论文; 统一建模语言论文; 模型检验论文; 函数式语言论文; 副作用论文; 抽象数据类型论文; 类别代数论文; 图灵机论文;