發(fā)布時(shí)間：2018-01-14 07:00

  本文關(guān)鍵詞：線性空間理論在定理證明器HOL中的形式化　出處：《北京化工大學(xué)》2013年碩士論文　論文類型：學(xué)位論文

  更多相關(guān)文章： 形式化 定理證明方法 定理證明器HOL 線性空間理論 HOL4系統(tǒng)

【摘要】：目前，計(jì)算機(jī)系統(tǒng)的設(shè)計(jì)正確性檢驗(yàn)問題已成為人們關(guān)注的重點(diǎn)，形式化方法就是一種新興的系統(tǒng)設(shè)計(jì)驗(yàn)證方法，它有效地彌補(bǔ)了傳統(tǒng)的測(cè)試、模擬等方法在系統(tǒng)設(shè)計(jì)驗(yàn)證中的“不完備性”問題。本文以一種典型的形式化方法——定理證明方法為研究方向，主要對(duì)定理證明器HOL進(jìn)行了研究，完成了以下一些工作： 首先對(duì)形式化方法進(jìn)行了簡(jiǎn)要的介紹，主要包括形式化方法的兩個(gè)方面——系統(tǒng)規(guī)范和形式化驗(yàn)證的基本概念，以及三種形式化驗(yàn)證方法的基本原理和各自的優(yōu)缺點(diǎn)。 接著對(duì)定理證明器HOL的發(fā)展歷史，以及HOL系統(tǒng)的最新版本HOL4系統(tǒng)的結(jié)構(gòu)進(jìn)行了詳細(xì)的分析、研究與歸納小結(jié)，并總結(jié)出了HOL4系統(tǒng)中一般理論建立的基本步驟。 根據(jù)對(duì)HOL4系統(tǒng)基本結(jié)構(gòu)的研究發(fā)現(xiàn)HOL4系統(tǒng)現(xiàn)有的理論體系并不完善，針對(duì)這一點(diǎn)，本文完成了HOL4系統(tǒng)中缺少的一個(gè)重要理論——線性空間理論在HOL4系統(tǒng)中的形式化工作。 最后，利用已形式化的線性空間理論，，在HOL4系統(tǒng)中完成了線性空間理論的幾個(gè)應(yīng)用實(shí)例的實(shí)現(xiàn)，從而展現(xiàn)了HOL4系統(tǒng)中已形式化的線性空間理論的應(yīng)用價(jià)值，進(jìn)一步說明了在HOL4系統(tǒng)中形式化線性空間理論的意義。
[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.

【學(xué)位授予單位】：北京化工大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2013
【分類號(hào)】：TP306

【參考文獻(xiàn)】

相關(guān)期刊論文 前10條

1 王青;楊孟飛;;基于斷言的形式驗(yàn)證方法應(yīng)用研究[J];航天控制;2007年03期

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

3 王金雙;楊華兵;張興元;王元元;張毓森;;SAODV協(xié)議在Isabelle/HOL中的正確性驗(yàn)證[J];解放軍理工大學(xué)學(xué)報(bào)(自然科學(xué)版);2008年05期

4 周宏斌,黃連生,桑田;基于串空間的安全協(xié)議形式化驗(yàn)證模型及算法[J];計(jì)算機(jī)研究與發(fā)展;2003年02期

5 趙輝;李明楚;王智慧;;一種基于虛擬組織的網(wǎng)格安全協(xié)議形式化驗(yàn)證方法[J];計(jì)算機(jī)工程與應(yīng)用;2007年24期

6 李光輝;曾松偉;;時(shí)序電路等價(jià)性檢驗(yàn)中的存儲(chǔ)元素映射方法研究[J];計(jì)算機(jī)科學(xué);2009年04期

7 曾瓊;閆煒;;組合電路等價(jià)性檢驗(yàn)方法研究[J];計(jì)算機(jī)工程;2007年04期

8 楊軍;翁延齡;葛海通;嚴(yán)曉浪;;利用狀態(tài)緩存的時(shí)序等價(jià)性驗(yàn)證算法[J];計(jì)算機(jī)輔助設(shè)計(jì)與圖形學(xué)學(xué)報(bào);2008年02期

9 李光輝;馮冬芹;曾松偉;;基于電路拓?fù)浣Y(jié)構(gòu)分析的等價(jià)性驗(yàn)證方法[J];計(jì)算機(jī)輔助設(shè)計(jì)與圖形學(xué)學(xué)報(bào);2008年12期

10 李光輝,李曉維;基于增量可滿足性的等價(jià)性檢驗(yàn)方法[J];計(jì)算機(jī)學(xué)報(bào);2004年10期

相關(guān)博士學(xué)位論文 前3條

1 左天軍;Java虛擬機(jī)安全性的形式化分析和驗(yàn)證[D];西安電子科技大學(xué);2005年

2 李光輝;邏輯電路的等價(jià)性檢驗(yàn)方法研究[D];中國(guó)科學(xué)院研究生院（計(jì)算技術(shù)研究所）;2005年

3 郭建;在數(shù)字系統(tǒng)設(shè)計(jì)中斷言驗(yàn)證的研究[D];西安電子科技大學(xué);2008年

相關(guān)碩士學(xué)位論文 前3條

1 林立;基于高階邏輯系統(tǒng)HOL的數(shù)字硬件形式化驗(yàn)證[D];西安電子科技大學(xué);2005年

2 陳波;基于定理證明器HOL的硬件驗(yàn)證研究[D];蘭州大學(xué);2006年

3 郭文章;ATS系統(tǒng)內(nèi)部通信協(xié)議的設(shè)計(jì)及形式化驗(yàn)證[D];北京交通大學(xué);2009年

本文編號(hào)：1422492