發(fā)布時(shí)間：2017-04-08 22:15

  本文關(guān)鍵詞：一種對NAND閃存硬件和閃存轉(zhuǎn)換層軟件的形式化建模，，由筆耕文化傳播整理發(fā)布。

【摘要】：NAND閃存已經(jīng)成為主流的存儲介質(zhì),并被廣泛地應(yīng)用到嵌入式、桌面、服務(wù)器以及數(shù)據(jù)中心等各種計(jì)算機(jī)系統(tǒng)中,并仍迅速地?cái)D占傳統(tǒng)純磁性材料存儲介質(zhì)的市場。與此同時(shí),在航空航天、國防軍工,核電,醫(yī)療設(shè)備等一些安全攸關(guān)領(lǐng)域,NAND閃存也因其存儲密度高、抗震性好、低功耗等特點(diǎn)得到了越來越多的應(yīng)用。然而NAND閃存的一些獨(dú)有的物理特性導(dǎo)致了其與傳統(tǒng)機(jī)械硬盤相比,具有天然的存儲不穩(wěn)定性。例如NAND閃存存在著磨損的問題,即經(jīng)過多次讀寫之后的閃存單元會變得越來越不穩(wěn)定,而且超過一定的擦除次數(shù)之后,存儲單元就會徹底報(bào)廢。又例如閃存單元讀寫會引入電流干擾,即在寫一個(gè)存儲單元時(shí),電流引起相鄰的存儲單元的位翻轉(zhuǎn)。NAND閃存的這些物理特性就對管理NAND的軟件提出了更高的要求。一種較為常見的解決方案引入一個(gè)被稱為閃存轉(zhuǎn)換層(Flash Translation Layer, FTL)的軟件層,用以隱藏這些物理特性,使得NAND閃存可以像傳統(tǒng)的機(jī)械硬盤一樣進(jìn)行任意讀寫。在過去的十多年里,有大量FTL軟件相關(guān)的算法被提出。為了兼顧穩(wěn)定性、性能,可靠性,這類算法通常比其他存儲介質(zhì)的管理軟件更為復(fù)雜,也更容易出現(xiàn)問題。為了構(gòu)建高可信的基于NAND閃存存儲的系統(tǒng)軟件,通過嚴(yán)格的形式化方法對NAND閃存硬件進(jìn)行建模,對管理NAND閃存的FTL軟件層的行為進(jìn)行正確性驗(yàn)證具有一定的理論和實(shí)際意義。 首先,本文根據(jù)一個(gè)被眾多閃存生產(chǎn)廠商廣泛接受認(rèn)可的NAND閃存接口標(biāo)準(zhǔn)ONFI3.0,采用形式化語言對NAND閃存硬件的真實(shí)語義進(jìn)行形式化建模。本文提出的形式化模型包括ONFI所定義的NAND閃存硬件的存儲層次結(jié)構(gòu)、閃存硬件芯片處理命令的內(nèi)部工作流程、閃存硬件的命令集,以及在此基礎(chǔ)之上定義的閃存的基本操作。本文的NAND閃存形式化模型在定理證明工具Coq中定義實(shí)現(xiàn)。在Coq工具中,該模型的一些性質(zhì)也得到了完整地證明。該模型可以直接被用來作為驗(yàn)證基于NAND閃存硬件的存儲系統(tǒng)軟件的基礎(chǔ)。 其次,本文使用基于不變式的證明方法建立了一個(gè)通用的、可以驗(yàn)證各種閃存轉(zhuǎn)換層正確性的形式化框架。所謂的正確性是指：在正確的初始條件下,,一個(gè)運(yùn)行著正確的閃存轉(zhuǎn)換層算法的NAND閃存與一塊傳統(tǒng)機(jī)械硬盤在相同的讀寫命令序列之后將輸出同樣的數(shù)據(jù)。在該形式化框架中,本文首次定義了一個(gè)經(jīng)典的閃存轉(zhuǎn)換層算法(BAST),并證明了算法的正確性。本文所建立的形式化NAND閃存模型和閃存轉(zhuǎn)換層算法證明框架為驗(yàn)證其上運(yùn)行的嵌入式操作系統(tǒng)及其它嵌入式軟件提供了嚴(yán)格的形式化模型,并將為基于NAND閃存的高可信嵌入式軟件的開發(fā)提供一個(gè)堅(jiān)實(shí)的基礎(chǔ)
【關(guān)鍵詞】：形式化驗(yàn)證 閃存轉(zhuǎn)換層 閃存設(shè)備 形式化建模 高可信軟件 存儲系統(tǒng)
【學(xué)位授予單位】：中國科學(xué)技術(shù)大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2015
【分類號】：TP333
【目錄】：

• 摘要5-7
• ABSTRACT7-9
• 目錄9-12
• 第1章 緒論12-20
• 1.1 研究背景12-16
• 1.1.1 NAND閃存12-14
• 1.1.2 閃存轉(zhuǎn)換層14
• 1.1.3 基于定理證明的程序驗(yàn)證14-16
• 1.2 研究內(nèi)容與研究方法16-18
• 1.3 研究難點(diǎn)與本文貢獻(xiàn)18-19
• 1.4 符號規(guī)范19
• 1.5 組織結(jié)構(gòu)19-20
• 第2章 NAND閃存模型的形式化20-30
• 2.1 形式化驗(yàn)證工具COQ20-21
• 2.2 NAND閃存存儲結(jié)構(gòu)21-22
• 2.3 NAND閃存工作結(jié)構(gòu)22-23
• 2.4 NAND閃存模型23-28
• 2.4.1 數(shù)據(jù)單元23-24
• 2.4.2 頁24-25
• 2.4.3 塊25-26
• 2.4.4 Plane26
• 2.4.5 邏輯單元26-27
• 2.4.6 Target27
• 2.4.7 設(shè)備27-28
• 2.5 本章小結(jié)28-30
• 第3章 NAND閃存操作的形式化30-50
• 3.1 NAND閃存的操作30-31
• 3.2 NAND閃存命令的形式化語義31-44
• 3.2.1 發(fā)送指令的操作語義32-36
• 3.2.2 發(fā)送地址的操作語義36-37
• 3.2.3 等待設(shè)備的操作語義37-41
• 3.2.4 接收數(shù)據(jù)的操作語義41-42
• 3.2.5 發(fā)送數(shù)據(jù)的操作語義42-43
• 3.2.6 讀取設(shè)備狀態(tài)的操作語義43-44
• 3.3 閃存設(shè)備驅(qū)動的驗(yàn)證44-48
• 3.3.1 讀操作44-45
• 3.3.2 寫操作45-46
• 3.3.3 擦除操作46
• 3.3.4 讀取狀態(tài)命令46-47
• 3.3.5 讀取設(shè)備參數(shù)命令47
• 3.3.6. 重置命令47-48
• 3.3.7 NAND閃存設(shè)備模型的性質(zhì)48
• 3.4 本章小結(jié)48-50
• 第4章 閃存轉(zhuǎn)換層算法的證明框架50-60
• 4.1 閃存轉(zhuǎn)換層算法50-52
• 4.2 閃存轉(zhuǎn)換層算法的正確性定義52-53
• 4.3 閃存轉(zhuǎn)換層算法正確性的形式化證明框架53-59
• 4.4 本章小結(jié)59-60
• 第5章 一個(gè)實(shí)際的閃存轉(zhuǎn)換層算法的證明60-76
• 5.1 BAST算法介紹60-69
• 5.1.1 塊的信息表和頁映射表63
• 5.1.2 空閑塊隊(duì)列63-65
• 5.1.3 BAST的讀算法65-66
• 5.1.4 BAST的寫算法66-69
• 5.2 BAST算法的全局不變式69-75
• 5.3 本章小結(jié)75-76
• 第6章 總結(jié)76-80
• 6.1 工作總結(jié)76-77
• 6.2 未來可能的研究工作77-80
• 參考文獻(xiàn)80-82
• 致謝82-84
• 在讀期間發(fā)表的學(xué)術(shù)論文與取得的其他研究成果84

【參考文獻(xiàn)】

中國期刊全文數(shù)據(jù)庫 前1條

1 李勝廣;張其善;;閃存設(shè)備在嵌入式Linux系統(tǒng)中的應(yīng)用[J];計(jì)算機(jī)工程;2007年02期

  本文關(guān)鍵詞：一種對NAND閃存硬件和閃存轉(zhuǎn)換層軟件的形式化建模，由筆耕文化傳播整理發(fā)布。

本文編號：293825