线性空间理论在定理证明器HOL中的形式化

发布时间：2018-01-14 07:00

  本文关键词：线性空间理论在定理证明器HOL中的形式化　出处：《北京化工大学》2013年硕士论文　论文类型：学位论文

  更多相关文章： 形式化 定理证明方法 定理证明器HOL 线性空间理论 HOL4系统

【摘要】：目前，计算机系统的设计正确性检验问题已成为人们关注的重点，形式化方法就是一种新兴的系统设计验证方法，它有效地弥补了传统的测试、模拟等方法在系统设计验证中的“不完备性”问题。本文以一种典型的形式化方法——定理证明方法为研究方向，主要对定理证明器HOL进行了研究，完成了以下一些工作： 首先对形式化方法进行了简要的介绍，主要包括形式化方法的两个方面——系统规范和形式化验证的基本概念，以及三种形式化验证方法的基本原理和各自的优缺点。 接着对定理证明器HOL的发展历史，以及HOL系统的最新版本HOL4系统的结构进行了详细的分析、研究与归纳小结，并总结出了HOL4系统中一般理论建立的基本步骤。 根据对HOL4系统基本结构的研究发现HOL4系统现有的理论体系并不完善，针对这一点，本文完成了HOL4系统中缺少的一个重要理论——线性空间理论在HOL4系统中的形式化工作。 最后，利用已形式化的线性空间理论，，在HOL4系统中完成了线性空间理论的几个应用实例的实现，从而展现了HOL4系统中已形式化的线性空间理论的应用价值，进一步说明了在HOL4系统中形式化线性空间理论的意义。
[Abstract]:At present, the design verification problem of computer system has become the focus of attention, formal method is a new system design verification method, it effectively makes up for the traditional test, simulation method in system design verification in the "incompleteness" problem. This paper takes a typical formal method theorem proving method is the research direction of the main theorem prover HOL is studied, completed the following work:
First, the formal methods are briefly introduced, including two aspects of formal methods, namely, the basic concepts of system specification and formal verification, as well as the basic principles and advantages and disadvantages of the three formal verification methods.
Then, the development history of theorem prover HOL and the latest version of HOL system, the structure of HOL4 system are analyzed, summarized and summarized, and the basic steps of general theory in HOL4 system are summarized.
According to the research on the basic structure of HOL4 system, it is found that the theoretical system of HOL4 system is not perfect. In view of this, this paper has completed an important theory in HOL4 system -- the formalization of linear space theory in HOL4 system.
Finally, using the linear space theory has been formally implemented, several application examples of the linear space theory in HOL4 system, so as to show the value of the linear space theory has been formalized in the HOL4 system, further illustrates the significance in HOL4 system of linear space theory.

【学位授予单位】：北京化工大学
【学位级别】：硕士
【学位授予年份】：2013
【分类号】：TP306

【参考文献】

相关期刊论文 前10条

1 王青;杨孟飞;;基于断言的形式验证方法应用研究[J];航天控制;2007年03期

2 ;Formal verification of safety protocol in train control system[J];Science China(Technological Sciences);2011年11期

3 王金双;杨华兵;张兴元;王元元;张毓森;;SAODV协议在Isabelle/HOL中的正确性验证[J];解放军理工大学学报(自然科学版);2008年05期

4 周宏斌,黄连生,桑田;基于串空间的安全协议形式化验证模型及算法[J];计算机研究与发展;2003年02期

5 赵辉;李明楚;王智慧;;一种基于虚拟组织的网格安全协议形式化验证方法[J];计算机工程与应用;2007年24期

6 李光辉;曾松伟;;时序电路等价性检验中的存储元素映射方法研究[J];计算机科学;2009年04期

7 曾琼;闫炜;;组合电路等价性检验方法研究[J];计算机工程;2007年04期

8 杨军;翁延龄;葛海通;严晓浪;;利用状态缓存的时序等价性验证算法[J];计算机辅助设计与图形学学报;2008年02期

9 李光辉;冯冬芹;曾松伟;;基于电路拓扑结构分析的等价性验证方法[J];计算机辅助设计与图形学学报;2008年12期

10 李光辉,李晓维;基于增量可满足性的等价性检验方法[J];计算机学报;2004年10期

相关博士学位论文 前3条

1 左天军;Java虚拟机安全性的形式化分析和验证[D];西安电子科技大学;2005年

2 李光辉;逻辑电路的等价性检验方法研究[D];中国科学院研究生院（计算技术研究所）;2005年

3 郭建;在数字系统设计中断言验证的研究[D];西安电子科技大学;2008年

相关硕士学位论文 前3条

1 林立;基于高阶逻辑系统HOL的数字硬件形式化验证[D];西安电子科技大学;2005年

2 陈波;基于定理证明器HOL的硬件验证研究[D];兰州大学;2006年

3 郭文章;ATS系统内部通信协议的设计及形式化验证[D];北京交通大学;2009年

本文编号：1422492