本文簡(jiǎn)單介紹了形式化方法的起源、發(fā)展、關(guān)鍵技術(shù)，并與傳統(tǒng)的基于模擬的驗(yàn)證方法進(jìn)行對(duì)比，分析它的優(yōu)點(diǎn)和不足。對(duì)數(shù)字硬件形式化驗(yàn)證技術(shù)進(jìn)行了分類，模型檢測(cè)，定理證明和等價(jià)性檢驗(yàn)。本文重點(diǎn)是基于HOL定理證明器的驗(yàn)證。為使用HOL系統(tǒng)，簡(jiǎn)單介紹函數(shù)式編程語(yǔ)言MOSCOW ML，該語(yǔ)言是HOL系統(tǒng)的元語(yǔ)言。我們?cè)敿?xì)介紹了該定理證明器所支持高階邏輯。分析了HOL系統(tǒng)的邏輯建立過(guò)程，常用的理論庫(kù)和重寫(xiě)策略。特別分析了HOL系統(tǒng)的證明方法及前向證明和目標(biāo)制導(dǎo)這兩種方法。作為上述理論的實(shí)際應(yīng)用，重點(diǎn)給出了RSA數(shù)字硬件的一個(gè)形式化驗(yàn)證實(shí)例。首先介紹如何利用HOL驗(yàn)證RSA算法的正確性。然后詳細(xì)介紹如何用HOL系統(tǒng)驗(yàn)證硬件設(shè)計(jì)的正確性。通過(guò)嚴(yán)密的思維和機(jī)器的輔助在嚴(yán)格的邏輯系統(tǒng)的基礎(chǔ)上進(jìn)行的證明可以提高設(shè)計(jì)的可靠性，進(jìn)一步加強(qiáng)了RSA算法和硬件實(shí)現(xiàn)的正確性的信心。同時(shí)培養(yǎng)我們的科學(xué)態(tài)度和利用數(shù)學(xué)工具分析和解決問(wèn)題的能力。 

【文章來(lái)源】：西安電子科技大學(xué)陜西省 211工程院校 教育部直屬院校

【文章頁(yè)數(shù)】：69 頁(yè)

【學(xué)位級(jí)別】：碩士

【文章目錄】：
緒論
第一章 數(shù)字硬件形式化驗(yàn)證概述
    1.1 形式化
    1.2 形式化的方法
    1.3 形式化的發(fā)展
    1.4 硬件形式化描述
    1.5 硬件形式化驗(yàn)證的過(guò)程
    1.6 定理證明器
第二章 HOL系統(tǒng)
    2.1 ML語(yǔ)言的介紹
    2.2 HOL系統(tǒng)
第三章 RSA加密算法的形式化證明
    3.1 RSA算法
    3.2 RSA的安全性
    3.3 RSA的現(xiàn)狀和前景
    3.4 RSA算法正確性的形式化驗(yàn)證
第四章 RSA數(shù)字硬件的形式化驗(yàn)證
    4.1 VHDL語(yǔ)言簡(jiǎn)介
    4.2 RSA數(shù)字硬件的實(shí)現(xiàn)
    4.3 模和同余的轉(zhuǎn)換的形式化證明
    4.4 模乘運(yùn)算模塊的形式化驗(yàn)證
    4.5 加密模塊的形式化驗(yàn)證
    4.6 證明思路的總結(jié)
    4.7 驗(yàn)證的結(jié)果
結(jié)論
致謝
參考文獻(xiàn)
作者在讀期間的研究成果
附錄A 重要定理證明對(duì)策清單
附錄B RSA數(shù)字硬件VHDL程序清單


【參考文獻(xiàn)】：
期刊論文
[1]基于高階邏輯的硬件驗(yàn)證方法[J]. 霍紅衛(wèi),韓俊剛.  計(jì)算機(jī)學(xué)報(bào). 1993(10)



本文編號(hào)：3150895