形式化建模運行在NAND閃存上的DFTL算法

張必紅，郭 宇，李兆鵬

(中國科學技術大學 蘇州研究院軟件安全實驗室，江蘇 蘇州 215123)

1 引 言

隨著科技和閃存技術的發展，閃存已經是現代電子設備作為存儲的主要選擇之一了.但是，閃存固有的物理特性使它相對于傳統的磁性存儲介質，有很大的區別.比如，閃存有“寫前擦除”的限定，所以在修改之前必須先要擦除，但是擦除卻是以塊為單位的，要比寫的單位頁大得多.因為這個局限以及磨損均衡，斷電保護等原因，在閃存的設計中，有個中間轉換層FTL(Flash Translation Layer)的概念被提了出來，FTL算法的核心是進行邏輯地址到物理地址的映射，也就是說如果一個邏輯地址映射到一個物理地址，而這個物理地址已經寫了數據了，而現在需要進行更新，那只能寫到一個空白的頁，然后在映射表中把新的物理地址取代原來的舊的物理地址，映射到要修改的邏輯地址，這樣來完成更新操作.一般典型的FTL算法的功能除了地址映射，還包括垃圾回收，壞塊管理，斷電保護，磨損均衡等.常用的FTL算法有BAST算法，FAST算法，LAST算法，DFTL算法等[1-4].DFTL算法相比較于與其它算法，DFTL算法在企業級規模的工作負載中表現尤其優異，特別在系統響應時間，隨機讀寫，大規模負載中均表現出性能優越.

我們可以看出DFTL算法很重要，但同時它也有著它的復雜性.為了保證閃存的性能，可靠，以及穩定，這類算法通常比其他存儲介質的管理軟件更為復雜，也更容易出現問題.在工業界SSD的各大廠商的競爭中，FTL層的設計是體現核心競爭力的地方.因為FTL層設計包括元數據管理，數據布局映射、磨損均衡、垃圾回收、緩存策略等，由此可見，FTL算法的重要性和復雜性.

正是由于DFTL算法的復雜和重要性，安全性需要得到可靠的保證，我們就決定采用形式化建模的方法來建立一個可靠的形式化模型.而形式化驗證存儲系統這方面的研究相當火熱，一直以來，完全驗證一個文件系統是個非常吸引人的目標[5].在這方面，最接近目標的努力由Schellhorn，Pfahler等在緩慢地進步著[6-9].但是目前驗證的文件系統，他們的底層只驗證到了讀寫硬盤這一層，而作為閃存內部算法的FTL層，則目前基本上沒有人研究.因為DFTL算法適用于有大規模請求的NAND閃存(SSD)，有著廣闊的市場應用場景，所以我們選擇對DFTL算法進行形式化建模.

本文的貢獻點在于以下：

1)本文根據DFTL算法的基本性質和操作，對DFTL算法的基本數據結構，進行了形式化建模.

2)本文根據DFTL算法讀寫操作的策略，對DFTL算法的讀寫操作和圾回收算法進行了分層形式化的建模.

3)本文對DFTL算法的一些基本性質進行了驗證.

本文形式化建模的代碼為可機器檢查的代碼，源代碼已經開源*源地址https://github.com/zbh24/formal_dftl.

2 背 景

2.1 NAND閃存及DFTL算法

NAND閃存是一種半導體存儲器，有讀，寫，擦除等基本操作，但擦除的單位是要比寫的單位頁大.相對于傳統的機械硬盤，具有隨機訪問快，功耗低，噪聲低等優點.但局限性也很明顯，就是有“寫前擦除”的限定.針對這種限制，有原地更新和異地更新兩種策略.原地更新就是：把當前塊中合法的其他數據拷貝到緩存中，然后擦除整個塊兒，再對這個空白塊中相對應的頁進行更新，再把其他合法數據寫回.因為擦除速度相對讀寫速度慢，代價大，現實中一般不會采用原地更新.而異地更新則是把當前頁標志為非法的(常用策略是把這種標志記錄在OOB中)，再把更新的數據寫到新的頁中，而記錄這種映射關系就是在FTL中，而這種標志為非法的垃圾塊在最后是需要進行垃圾回收，從而重新變為合法的空白塊.

FTL設計有很多種，如果我們基于映射關系來進行分類，我們可以分為基于塊映射的，基于頁映射的，和混合映射的.基于塊映射就是一個數據塊對應一個日志塊，寫數據時向數據塊寫數據，而要更新數據時則向對應的日志塊寫數據，典型的基于塊映射的有BAST算法.基于頁映射則是每一個頁對應一個日志頁，更新數據時則寫到對應的日志頁，典型的頁映射算法有DFTL算法.而把這兩種基于塊和基于頁進行混合起來設計的算法，典型的有FAST算法.

DFTL算法是一種基于全相聯頁映射的FTL算法.它其實并沒有明確的日志塊的概念，它把所有的塊分為兩種，一種數據塊，即是記錄數據的塊，塊中只記錄數據.一種為映射塊，即是記錄這種映射的塊，塊中只記錄映射數據.DFTL不僅采用了基于頁映射的策略，它還利用了訪問數據的局部性原理，會在閃存內存中記錄最近訪問的映射記錄，而全部的映射記錄則記錄在閃存的物理介質上.另外，每頁的狀態可以分為擦除，數據頁，映射頁，非法頁.DFTL算法會在閃存內存中保存兩張表，一張為CMT表(cache_mapping_table)，即為一張有固定容量的緩存表，來記錄最近訪問的這種映射關系，而淘汰時一般采用LRU(最近最久未使用)算法.另一張為GTD表(global_translation_table)，來記錄所有的邏輯地址到映射頁的這種映射.

這個讀算法流程如下，如果一個請求的邏輯地址在CMT中，那么就直接在CMT中找到對應的物理塊和在其中的偏移，讀出相應數據.如果請求的邏輯地址沒有命中CMT，那么就需要查看CMT緩存表是否滿了，如果滿了，則犧牲一項并且同時判斷犧牲的這一項是不是最新的，最新的則需要寫回到映射塊中.然后，就把這條最新的映射記錄更新到CMT緩存表中，然后再從CMT中讀出相應的物理塊和頁號，接著從物理塊中讀出數據來.

圖1 DFTL讀算法示例Fig.1 Example of DFTL read algorithm

圖1展示了一個具體的DFTL讀算法的例子，一個邏輯地址(lpn = 1234)訪問，首先，CMT里沒有找到，然后去GTD表查詢，找到這條記錄存儲在映射塊的第47頁中，然后在影射頁讀出相應的映射記錄，然后去數據頁(Dppn = 704)讀出數據來，同時把這條最新的訪問記錄更新到CMT表中.

DFTL寫算法的邏輯相對簡單，DFTL算法會一直保持兩個塊，current_data_blcok(當前數據塊)和current_trans_block(當前映射塊).寫算法是直接從current_data_block中分配一個空白頁，然后把數據寫進去，然后再更新到CMT表.如果current_data_blcok滿了，則從自由塊中分配一個新塊來當做新的current_data_blcok.

隨著讀寫的不斷進行，非法頁會越來越多，為了使它們可以重新使用，就需要垃圾回收也就是擦除操作來進行.垃圾回收對于數據塊和映射塊采用不同的策略.如果是映射塊，則把合法的映射頁復制到當前映射塊，然后更新CMT.如果是數據塊，則把合法的數據頁復制到當前數據塊，然后再更新對應的映射頁和CMT表.具體算法的形式化定義會在后面進行說明.下面的兩張圖分別展示了映射塊和數據塊的回收過程.

圖2 DFTL映射塊的垃圾回收Fig.2 Example of the translation block garage collection

圖2是一個具體的映射塊的回收例子，選中映射塊Block1，然后把合法的數據拷貝到當前的映射塊Block2中，然后再去更新相應的全局映射表(GTD)的記錄.

圖3的數據塊回收，首先選中一個數據塊，然后把合法的數據拷貝到當前的數據塊，接著對于記錄這條映射記錄的映射塊也進行回收，把含有這條記錄的映射塊標記為非法，然后在當前的映射塊里分配一頁，更新新的映射記錄，最后來更新GTD表和CMT表.

圖3 DFTL數據塊的垃圾回收Fig.3 Example of the data block garage collection

DFTL算法的主要操作流程，就是是由以上讀操作，寫操作，和針對映射塊和數據塊的垃圾回收算法構成的.

2.2 形式化工具Coq

Coq是一個交互式的定理證明工具，在Coq里面可以形式化定義程序和程序規范，并且可以自動或者半自動地尋找證明項.Coq是建立在構造演算的基礎上的，雖然Coq并不是一個完全自動的定理證明工具，但是它提供了一些尋找證明的策略，并提供了一種語言(Ltac)可以讓用戶自己定義證明策略.目前Coq在形式化領域已經得到比較廣泛的應用，比如一個已經被形式化驗證的C語言編譯器CompCert[10].

3 DFTL算法數據結構的形式化定義

3.1 FTL的組成

根據DFTL算法提出者的設計，我們把DFTL算法形式化建模成以下6個部分：

Record FTL：Set：=

mk _FTL {

ftl_bi_table：block_info_table；

ftl_free_blocks：block_queue；

ftl_cmt_table：cache_mapping_table；

ftl_gtd_table：global_mapping_directory；

current_data_block：block_no；

current_trans_block：block_no

}.

這6個部分分別表示為所有的塊的信息表，所有空閑塊的列表，部分映射的緩存表，全局映射目錄表，當前的數據塊號，當前的映射塊號.下面我們將分別建模每個模塊.

3.2 ftl_bi_table

ftl_bi_table的類型是block_info_table，block_info_table是所有塊詳細信息的列表，具體包括以下部分：每個塊的狀態，已經使用了多少頁，擦除次數和每頁狀態的列表，這些頁的狀態包括擦除，數據頁，映射頁，非法頁.具體結構如下：

Record block_info：Set：=

mk_bi {

bi_state：ftl_block_state；

bi_used_pages：nat；

bi_erase_count：nat；

bi_page_state：page_state_table

}.

Definition block_info_table：= list block_info.

3.3 ftl_free_blocks

ftl_free_blocks的類型是block_queue，block_queue是所有自由塊號的列表，它是一個先進先出的隊列.每當一個塊寫完時，需要申請新塊的時候，就從這個列表中出隊一個塊，當一個塊被回收時，就加入到這個隊列中.具體結構如下：

Definition block_queue：= list block_no.

3.4 ftl_cmt_table

ftl_cmt_table的類型是cache_mapping_table，cache_mapping_table是一個有固定長度緩存記錄的列表，這些記錄的替換原則則遵循LRU算法.每條記錄包括：邏輯地址，物理地址(物理塊號和在塊內偏移)，以及臟位(is_drity).如果標志位為臟位，則在淘汰時需要到把這條記錄，寫回到相應的塊中，否則淘汰時可以直接丟棄.具體定義結構如下：

Inductive cmt_record：Set：=

| cmt_empty

| cmt_trans (lpn：page_no)(pbn：block_no)

(offset：nat)(is_dirty：flag).

Definition cache_mapping_table：= list cmt_record.

3.5 ftl_gtd_table

ftl_gtd_table的類型是global_mapping_directory，global_mapping_directory是所有映射塊的目錄表.每個合法的邏輯地址都有一個對應的映射目錄號，而所有的映射目錄號都會給分配一個映射頁，這些映射頁里就寫著真正的映射記錄.全局映射目錄表的結構如下：

Inductive gtd_record：Set：=

| gtd_empty

| gtd_trans(pbn：block_no)(offset：nat).

Definition global_mapping_directory：= list gtd_record.

3.6 current_data_block和current_trans_block

current_data_blcok和current_trans_block的類型都是自然數(nat)，分別代表著當前的數據塊號和映射塊號.當需要寫一個數據頁時，先檢查當前的數據塊是否還有空閑頁，有空閑頁就向里面寫入數據，沒有則分配一個新的數據塊，然后把這個新的數據塊號更新為當前的數據塊號.每當需要寫一個映射頁時，映射塊也是執行類似的操作過程.

4 DFTL算法的形式化定義

4.1 DFTL算法的讀過程

根據DFTL算法的原論文描述，我們形式化定義讀算法操作如圖4所示.

圖4 DFTL讀算法
Fig.4 DFTL read algorithm

根據DFTL算法的操作語義，我們進行了分層次抽象，從最頂層的FTL讀函數接口到最底層調用NAND硬件接口.具體抽象定義如下，首先我們最頂層的DFTL讀算法函數簽名定義為：

Definition FTL_read(c：chip)(f：FTL)(lpn：page_no)：option(prod data(prod chip FTL)).

表示為輸入chip，FTL和邏輯頁號，輸出為數據，新的chip閃存和FTL.接下來，對于讀具體操作，我們會判斷當前邏輯頁號是否在CMT中.當邏輯頁號不在CMT中同時CMT也滿了的時候，采用LRU淘汰策略，我們形式化定義LRU淘汰策略時采用淘汰最久最未被使用，為此針對CMT，我們定義了如下四個函數remove_cmt，remove_head，insert_cmt，append_tail.

再接著，我們會進行判斷，被淘汰的這條記錄的標志位是否為臟位，如果是臟位，則我們需要將被淘汰的記錄寫回到NAND物理介質中去.關于寫回去這個函數，我們抽象出它的操作語義，定義函數簽名如下：

Definition copy_trans_page(c：chip)(f：FTL)(lpn：page_no)(trans_pbn：block_no)(trans_off：nat)(pbn：block_no)(off：nat)：option(prod chip FTL).

分別表示為輸入NAND，FTL，邏輯頁號以及它對應的映射塊和在映射塊中的偏移，以及對應新的數據塊和在數據塊中的偏移，輸出為新的chip和FTL.這個函數具體形式化語義為，當這條最新的映射記錄被寫回NAND物理介質中時，如果對應的映射頁里沒有時，則我們把這條映射記錄添加到對應的映射頁里，否則我們就把最新的映射記錄更新到對應的映射頁里.

再往下，我們需要對GTD和CMT進行查找，更新，插入等操作.所以我們對GTD和CMT這類數據結構都定義了查找，更新，插入等操作.

最后，我們得到了邏輯頁號對應的物理頁號時，調用read_block函數，在這個函數里調用了一個已經被形式化建模的NAND閃存模型的接口[11]，從而讀出數據來，我們的DFTL算法是運行在這個已經被形式化定義的NAND閃存模型上，這就是整個DFTL讀算法分層次形式化定義的基本結構.

4.2 DFTL算法的寫過程

DFTL算法的寫操作形式化定義如下：首先直接檢測當前數據塊是否滿了，如果滿了則申請新的一塊，然后分配一個新的數據頁，直接把數據寫進數據頁里面，接著再把這條記錄寫到對應的CMT中，對CMT進行更新操作.具體邏輯見圖5.

圖5 DFTL寫算法
Fig.5 DFTL write algorithm

和FTL讀函數一樣，我們也采用了分層形式化建模，首先最頂層FTL寫函數的函數簽名如下：

Definition FTL_write(c：chip)(f：FTL)(lpn：page_no)(d：data)：option(prod chip FTL).

分別表示為輸入chip，FTL，邏輯頁號和數據，操作完成以后，輸出一個新的chip閃存和FTL.

然后，在FTL_write函數中需要對CMT進行更新，關于CMT的更新比較復雜.具體的形式化定義如下：CMT表是一個固定長度的先進先出的隊列，每次讀或者寫都算作一次訪問.在隊尾的是最新訪問的記錄，在隊頭的是最久沒有被訪問的記錄.替換的時候，我們根據不同情況，形式化定義了以下這4種替換策略：

1.CMT滿了且CMT里面沒有對應記錄：去掉第一項，把當前記錄添加到隊列末尾.

2.CMT滿了且CMT有對應的記錄：則把當前記錄移除，添加到隊列末尾.

3.CMT未滿且CMT里面沒有對應記錄：則從頭直接找到第一個空白項，把當前記錄寫進去.

4.CMT未滿且CMT有對應的記錄：則把當前記錄移除，從頭找到第一個空白項，把當前記錄寫進去.

具體可參考cmt_update_when_ftl_write函數，函數簽名如下：

Definition cmt_update_when_ftl_write(c：chip)(f：FTL)(lbn：block_no)(loff：nat)：option(prod chip FTL).

最后，我們需要把數據寫進數據塊中，我們抽象出write_data_block函數，這個函數里面會直接調用NAND閃存模型提供的接口.如果當前數據塊滿了，則需要分配新的塊，我們形式化定義了alloc_block，free_block等函數，這些函數的實現涉及下文的垃圾回收算法，我們將在下節中描述，整個FTL讀函數的形式化定義流程基本就如上所述.

5 DFTL的垃圾回收算法的形式化定義

首先我們定義的垃圾回收過程是發生在申請分配塊的時候，當且僅當剩余塊的數量低于閾值時才會發生調用.至于申請塊的函數形式化定義如下：

Definition alloc_block(c：chip)(f：FTL)(flag：alloc_block_type)：option(prod chip FTL).

它的函數簽名表示如下，輸入chip，FTL，和申請的塊類型，輸出新的chip和FTL.它的操作語義表示：如果剩余塊的數量大于閾值時，則正常分配塊.否則開始進行垃圾回收操作.垃圾回收的函數的簽名如下：

Definition gc(c：chip)(f：FTL)(flag：alloc_block_type)：option(prod chip FTL).

函數的操作語義如下：首先是選擇出要回收的塊，接著對要回收的塊的類型進行判斷，然后再進行垃圾回收操作，數據塊和映射塊對應著不同的垃圾回收策略，下面將分別說明.

5.1 映射塊的垃圾回收

對于映射塊的垃圾回收形式化定義為以下幾個步驟和層次：首先給當前的映射塊分配一個新的塊，注意這個申請操作不受閾值的影響，是總是可以進行的，即不通過調用alloc_block函數來申請塊的.接著從所有的塊中選擇一個映射塊進行垃圾回收，注意選擇哪個回收塊大概要考慮兩個方面，第一這個塊中至少有一個非法的頁，否則沒有必要進行回收操作.第二要注意負載均衡，因為一個塊的擦寫次數是固定的，這里為了簡化操作，只考慮了前者.接著當選擇一個映射塊進行回收時，依次對每個頁進行掃描，如果這個頁是合法的，則從當前映射塊申請一個新的映射頁，把這塊數據復制進去，同時更新GTD，并把這頁設置為非法的，重復以上操作直到這個回收塊的所有頁都被掃描完以后，則可以把這塊映射塊標志為非法塊，擦除后加入自由塊的隊列中，這樣一次對映射塊的垃圾回收操作完成.同時注意，對于原來申請新塊的操作，經過垃圾回收過后，因為新申請塊的空閑頁數大于等于需要回收塊的合法頁數，所以不難證明原來的讀寫操作是總是可以進行下去的.

圖6 映射塊的垃圾回收
Fig.6 Translation block GC

5.2 數據塊的垃圾回收

和映射塊類似，對于數據塊的垃圾回收形式化定義也分為幾層.當需要分配數據塊的時候，剩余塊的數量低于閾值值時，則進行數據塊的垃圾回收操作.首先給當前的數據塊分配一個新的塊，這個操作跟映射塊的垃圾回收第一步是一樣的.接著對數據塊的垃圾回收也是要選擇一個合法的回收塊，依次對每個數據頁進行掃描，如果被掃描的數據頁是非法的數據頁，則跳過這頁并繼續掃描，否則一旦被掃描到的是合法的數據頁，則首先從當前數據塊分配一個新的數據頁，然后把這塊合法的數據頁的數據復制到新的空白數據頁，直到把整個回收塊的數據頁掃描完.注意在這個過程中，如果CMT中有相應的記錄，則進行CMT的更新，并且還要進行映射頁和GTD表的更新.另外也可能會發生當前的映射塊滿了，需要再次申請新的映射塊.所以在數據塊的垃圾回收中可能會多次發生對映射塊的垃圾回收.最后當所有的頁都被掃描完成以后，則標志當前塊為非法，擦除后加入自由塊的隊列中了，至此對數據塊的垃圾回收操作完成.同樣的原來申請的新的數據塊的操作，經過數據塊的垃圾回收過后，總是可以繼續進行下去的.

關于垃圾回收的形式化模型，有兩點需要說明一下：

1)這個垃圾回收的觸發閾值是剩余塊一旦小于等于2塊，則進行垃圾回收操作.因為在數據頁的垃圾回收操作時，可能會發生嵌套1層的映射塊的垃圾回收操作，所以剩余的自由塊的數量必須至少大于等于2，才能使垃圾回收繼續進行下去，否則小于2塊時才進行垃圾回收，則有可能會使操作卡死.

2)關于數據塊的回收操作，我們可以采取批量更新的策略，提高效率，不過這不影響垃圾回收算法的語義，因此我們的形式化時沒有采取這種優化.

圖7 數據塊的垃圾回收
Fig.7 Data block GC

6 形式化模型的基本性質

因為形式化建模DFTL算法是為了保證DFTL算法的正確性，所以我們首先必須正確地描述運行著DFTL算法的NAND閃存的性質.首先我們定義了一個簡單的硬盤模型，然后定義了R關系來保持硬盤和運行DFTL算法的NAND閃存具有一致性，接著定義Inv關系來保證NAND閃存運行過程中的一致性，具體定義如下：

R：?sec,hddreadhdd sec=fldreadfldsec

Inv：?c f,Finvf∧ Rinvc f

以上R表示對于任意一個地址，閃存和硬盤讀出來的數據都是一樣的.Inv表示在運行過程中，FTL軟件的一些性質會始終保持不變并且FTL軟件層和硬件層的一致性也始終保持不變.運行著DFTL算法的NAND閃存具體有以下性質(由于篇幅所限，僅列上部分性質)：

性質1.

Rinit:=R hddinitfldinit

性質1表示一開始整個NAND閃存都是空白的，在任意和硬盤同樣的位置讀出的數據都是一樣的，即是NONE或者0.

性質2.

Writepreservel:= ? c f lpn d,Inv c f

→validlogic_page_no lpn

→?c′ f′,FTLwritec f lpn d

=Some(c′，f′)∧(?c",f",

FTLreadc′f′lpn

=Some(d,(c",f"))

性質2表示，對于任意一個chip，ftl，page_no，data，只要chip和 ftl滿足Inv關系并且這個page_no是合法的，那么就一定可以把數據寫進去，并且在寫過后的閃存同樣的地址讀出的數據和寫進去的數據是一樣的.

性質3.

Writepreserve2:= ? c f lpn d,Inv c f

→validlogic_page_nolpn

→? c′ f′,FTLwritec f lpn d

=Some(c′，f′)∧(? lpn′，

=lpn′<>lpn→FTLreaddatac f lpn′

=FTLreaddatac′ f′ lpn′

性質3表示，對于在任意一個合法的邏輯地址lpn寫入數據之后，在任意的lpn’不等于lpn的地址上讀出的數據跟寫入數據之前是一樣的，即表示DFTL算法在一個邏輯地址寫入數據后，不影響另一個邏輯地址的數據.

以上這些基本性質均在Coq中得到了證明.

7 結束語以及未來工作方向

閃存設備現在使用的已經越來越普遍了，在存儲系統中扮演著一個非常重要的地位，但是閃存設備的復雜性和頻繁出現問題的危害性需要得到重視.本文就是針對閃存中使用的一種比較經典的DFTL算法進行了形式化的建模.首先我們針對DFTL的基本構成和性質，對DFTL的基本數據結構進行了形式化建模，其次我們對DFTL算法的讀操作和寫操作也進行了分層次的形式化定義，再接著我們針對DFTL算法一定會出現的非法塊，也定義了垃圾回收的形式化算法.最后，我們對DFTL算法的一些基本性質在我們的模型上的正確性進行了驗證.我們未來的工作，就是在已經形式化定義好的DFTL模型的基礎上，對DFTL算法的一些更復雜的性質，在一個描述正確性的框架下，進行形式化驗證，來保證DFTL算法的行為約束來符合我們的要求.

[1] Chung T，Park D，Park S，et al.System software for flash memory：a survey[C].In Proceedings of the International Conference on Embedded and Ubiquitous Computing，2006：394-404.

[2] Lee S，Park D，Chung T，et al.A log buffer based flash translation layer using fully associative sector translation[J].IEEE Transactions on Embedded Computing Systems，2007，6(3)：18.

[3] Lee S，Shin D，Kim Y J，et al.LAST：locality-aware sector translation for NAND flash memory-based storage systems[J].ACM SIGOPS Operating Systems Review，2008，42(6)：36-42.

[4] Gupta A，Kim Y，Urgaonkar B.DFTL：a flash translation layer employing demand-based selective caching of page-level address mappings[J].ACM Sigplan Notices，2009，44(3)：229-240.

[5] Joshi R，Holzmann G J.A mini challenge：build a verifiable filesystem[J].Formal Aspects of Computing，2007，19(2)：269-272.

[6] Ernst G，Pfahler J，Schellhorn G，et al.Inside a verified flash file system：Transactions and garbage collection[C].In Proceedings of the 7th Working Conference on Verified Software：Theories，Tools and Experiments.Springer International Publishing，2015：73-93.

[7] Pfahler J，Ernst G，Schellhorn G.Crash-safe refinement for a verified flash file system[R].Technical Report 2014-02，University of Augsburg，2014.

[8] Schellhorn G，Ernst G，Pfahler J，et al.Development of a verified flash file system[C].International Conference on Abstract State Machines，Alloy，B，TLA，VDM，and Z.Springer Berlin Heidelberg，2014：9-24.

[9] Schierl A，Schellhorn G，Haneberg D，et al.Abstract specification of the ubifs file system for flash memory[M].Formal Methods.Springer Berlin Heidelberg，2009：190-206.

[10] Leroy X.Formal verification of a realistic compiler[J].Communications of the ACM，2009，52(7)：107-115.

[11] Yang Long-ying，Guo Yu.Formal modeling for NAND flash hardware[J].Computer Engineering，2015，41(11)：94-99.

附中文參考文獻：

[11] 楊龍嬰，郭 宇.針對NAND閃存硬件的形式化建模[J].計算機工程，2015，41(11)：94-99.