面向空間飛行器的文件系統(tǒng)需求層驗證

李少峰， 楊孟飛， 喬 磊， 姜菁菁， 王婷煜

1. 西安電子科技大學(xué),西安 710071 2. 中國空間技術(shù)研究院,北京 100094 3. 北京控制工程研究所,北京 100094

0 引 言

空間嵌入式環(huán)境比較惡劣，需要對計算機上相關(guān)的器件進行特殊的保護，因為目前工藝的局限性，空間計算機無法像地面計算機一樣擁有充分的系統(tǒng)資源，其系統(tǒng)資源通常都比較小.文件系統(tǒng)的索引結(jié)構(gòu)和元數(shù)據(jù)通常都比較大，為了文件系統(tǒng)的快速響應(yīng)，通常都需要這些數(shù)據(jù)長時間駐留在內(nèi)存中.在空間設(shè)備中，往往沒有足夠的內(nèi)存空間存放這些數(shù)據(jù)，因此，根據(jù)空間設(shè)備的特點，需要設(shè)計專用于空間飛行器的文件系統(tǒng).

NAND型閃存的優(yōu)點在于寫入/擦除速度快、存儲容量大[1]，因此常作為數(shù)據(jù)儲存設(shè)備，在各種計算機系統(tǒng)中得到了廣泛的使用，從嵌入式設(shè)備到筆記本電腦、臺式機和數(shù)據(jù)中心.與傳統(tǒng)磁盤相比，它有了巨大的性能提升并且節(jié)省了功耗，同時，存儲數(shù)據(jù)的量也更大.但是，由于其物理特性，無法進行原地更新，如果系統(tǒng)要覆蓋設(shè)備中的舊數(shù)據(jù)單元，它必須擦除包含該單元的整個塊.所以，在磁盤上廣泛使用的文件系統(tǒng)并不能直接在閃存上使用，例如FAT、EXT3[2]等.

圖1 Nand型閃存為外部存儲設(shè)備的文件系統(tǒng)結(jié)構(gòu)Fig.1 System structure of external storage device with Nand flash

通常的解決方案是設(shè)計閃存轉(zhuǎn)換層FTL(flash translation layer)[3]，如圖1(a)，提供地址映射、垃圾回收、磨損均衡等功能，使得磁盤文件系統(tǒng)可以在閃存上運行.雖然喬磊等[4]通過形式化方法驗證了FTL層的正確性.但是，這樣的解決方案無法充分利用閃存的特性并且十分耗時，在實時性強的嵌入式設(shè)備中無法滿足設(shè)備的時序要求.

專用閃存文件系統(tǒng)是指根據(jù)閃存的特性，設(shè)計可以在其上面運行的文件系統(tǒng)，它直接管理閃存設(shè)備，能充分發(fā)揮閃存的存儲優(yōu)勢，如圖1(b)所示.目前已有的閃存文件系統(tǒng)包括JFFSx[5]、YAFFS[6]、UBIFS[7]等.

空間設(shè)備多采用Nand型閃存作為數(shù)據(jù)的存儲介質(zhì).但是，目前的閃存文件系統(tǒng)的內(nèi)存占用情況都比較大，同時，文件系統(tǒng)的實時性也不夠.因此，設(shè)計專用于空間設(shè)備的閃存文件系統(tǒng)是亟需解決的問題.

另外，采用嚴格的形式化方法對文件系統(tǒng)進行設(shè)計和實現(xiàn)是公認的可靠方法.GALLWAY等[8]使用模型檢測的方法對Linux虛擬文件系統(tǒng)進行了形式化驗證，對系統(tǒng)的實際運行情況進行分析，并對數(shù)據(jù)完整性等約束條件的可滿足性進行驗證.HSSELINK等[9]形式化驗證了一款抽象文件系統(tǒng)，并從文件系統(tǒng)的高層次出發(fā)，逐層進行抽象描述，驗證系統(tǒng)符合規(guī)范.錢振江等[10]對微內(nèi)核架構(gòu)下的VTOS系統(tǒng)中的文件系統(tǒng)模塊進行了形式化的建模與驗證，使用狀態(tài)機模型在Isabelle/HOL定理工具中完成了證明.CHEN等[11]提出第1個具有機器可檢查證明的文件系統(tǒng)FSCQ，使用基于霍爾邏輯擴展的崩潰霍爾邏輯進行驗證.ZOU等[12]提出第1個形式化驗證的、細粒度的并發(fā)文件系統(tǒng)AtomFS.LI等[13]提出了形式化模型來準確描述底層讀寫行為，對文件系統(tǒng)進行驗證.

空間飛行器中應(yīng)用最廣泛的操作系統(tǒng)是SpaceOS[14]，相關(guān)研究團隊對該系統(tǒng)的內(nèi)存管理[15-16]、中斷管理[17-18]、任務(wù)管理[19]等模塊進行了形式化驗證，因此，要開發(fā)一款在空間設(shè)備上使用的文件系統(tǒng)，需要對其進行形式化驗證.

目前，針對文件系統(tǒng)的驗證工作大多都是在系統(tǒng)開發(fā)工作結(jié)束之后，證明所實現(xiàn)代碼符合其針對文件系統(tǒng)建立的形式規(guī)范，從而表明其所驗證文件系統(tǒng)的正確性.而本文嘗試在空間飛行器文件系統(tǒng)的需求分析階段就引入形式化驗證，證明所提出的功能需求是正確的，為后續(xù)的設(shè)計與開發(fā)提供必要的函數(shù)規(guī)范.

空間飛行器以Nand型閃存為外部存儲介質(zhì)，需要利用閃存的特點[20]進行文件系統(tǒng)的研究工作.本文使用形式化的方法提出空間飛行器文件系統(tǒng)的功能需求，并進行驗證，證明所提出需求的正確性.

1 空間飛行器文件系統(tǒng)需求

通用計算機的硬件結(jié)構(gòu)如圖2所示，是典型的I/O總線結(jié)構(gòu).對于通用計算機來說，最常用的便是PCI(peripheral component interconnect)總線.因為總線的傳輸速度快，且內(nèi)存空間也足夠大，所以通用計算機的文件系統(tǒng)往往比較大，占用了過多的內(nèi)存空間.當外部設(shè)備為Flash設(shè)備時，其也往往通過在系統(tǒng)中添加FTL層進行轉(zhuǎn)換.但是對于實時性要求非常高的空間飛行器來說，使用這種方式的文件系統(tǒng)是不合適的.

因此，需要設(shè)計以Nand型閃存為外部存儲設(shè)備的專用閃存文件系統(tǒng).在空間飛行器的應(yīng)用環(huán)境下，其還有以下兩個限制:1)空間設(shè)備的總線使用的是1553B總線，其速度比較慢，相比于高速運行的CPU，其很容易成為系統(tǒng)的瓶頸，所以設(shè)計的文件系統(tǒng)需要減少CPU與外部設(shè)備的交互，從而減少使用總線通信.2)空間設(shè)備的內(nèi)存十分有限，設(shè)計的文件系統(tǒng)應(yīng)該使用較少的內(nèi)存空間.

圖2 I/O總線結(jié)構(gòu)Fig.2 I/O bus structure

接下來針對空間飛行器文件系統(tǒng)的這兩個限制，提出基于閃存的空間專用文件系統(tǒng)需求.針對于文件系統(tǒng)的功能需求，使用標簽FUN表示；對于文件系統(tǒng)對底層操作系統(tǒng)的要求，認為是文件系統(tǒng)所處的環(huán)境，使用標簽ENV表示.

圖3 文件系統(tǒng)需求分層精化Fig.3 Hierarchical refinement of file system requirements

如圖3所示，將嵌入式文件系統(tǒng)的需求分為7層進行精化分析.并針對每一層提出功能需求和所處環(huán)境要求，然后提煉出需滿足的性質(zhì)并進行相應(yīng)的驗證.

1.1 數(shù)據(jù)讀寫(L1)

首先考慮文件系統(tǒng)最基本的需求，將內(nèi)存中的數(shù)據(jù)寫入到存儲設(shè)備中，達到持久化存儲數(shù)據(jù)的目的.當程序需要使用數(shù)據(jù)時，從存儲設(shè)備中讀出相應(yīng)的數(shù)據(jù)到內(nèi)存中.

FUN1寫入數(shù)據(jù)將數(shù)據(jù)從內(nèi)存拷貝到外存FUN2讀取數(shù)據(jù)將數(shù)據(jù)從外存拷貝到內(nèi)存

對于文件所處的環(huán)境定義如下：

ENV1假定文件是一個數(shù)據(jù)項的序列ENV2文件在內(nèi)存與外存之間以一個個片段的方式傳輸ENV3外存的物理介質(zhì)是閃存

1.2 文件創(chuàng)建(L2)

在寫文件之前，需要判斷該文件是否存在，如果不存在則創(chuàng)建該文件，并從文件數(shù)據(jù)區(qū)域開始寫入文件.

FUN3創(chuàng)建文件是建立文件名到文件元數(shù)據(jù)位置的映射關(guān)系FUN4新創(chuàng)建的文件元數(shù)據(jù),內(nèi)容為空,即不包含文件實際的存儲位置信息

文件目錄和文件元數(shù)據(jù)所處的環(huán)境如下：

ENV4文件名到文件元數(shù)據(jù)位置的映射關(guān)系本質(zhì)上就是文件目錄,其在文件系統(tǒng)運行期間存儲在內(nèi)存中ENV5文件的元數(shù)據(jù)在文件系統(tǒng)運行期間存儲在內(nèi)存中

1.3 文件刪除(L3)

與文件創(chuàng)建對應(yīng)，當文件數(shù)據(jù)過時后，需要對文件進行刪除.

FUN5刪除文件是將文件名到文件元數(shù)據(jù)位置的映射信息刪除,并刪除文件元數(shù)據(jù)和文件數(shù)據(jù)FUN6刪除文件數(shù)據(jù)是將文件數(shù)據(jù)所在的閃存頁的狀態(tài)標記為無效

1.4 文件讀取(L4)

文件讀取是通過文件元數(shù)據(jù)信息，將文件的數(shù)據(jù)信息讀取到內(nèi)存中.

FUN7通過文件元數(shù)據(jù),將文件讀取分解為n段數(shù)據(jù)讀取(n>0)

文件讀取的環(huán)境如下：

ENV6每一段數(shù)據(jù)的大小與閃存的最小數(shù)據(jù)單元閃存頁的大小一致

1.5 文件寫入(L5)

對于文件寫入分為兩個方面：不改變文件原有數(shù)據(jù)和改變文件原有數(shù)據(jù)兩種情況.

FUN8文件尾部添加數(shù)據(jù)時,進行數(shù)據(jù)寫入操作,并更新文件的元數(shù)據(jù)FUN9更改原有數(shù)據(jù)時,先刪除原有數(shù)據(jù),再寫入新的數(shù)據(jù),更新文件元數(shù)據(jù)

文件寫入的環(huán)境如下：

ENV7寫入數(shù)據(jù)的大小與閃存的最小數(shù)據(jù)單元閃存頁的大小一致

1.6 文件系統(tǒng)掛載與卸載(L6)

文件目錄是指文件名到文件元數(shù)據(jù)的映射。文件系統(tǒng)的掛載就是將這個映射結(jié)構(gòu)讀取到內(nèi)存中.文件系統(tǒng)的卸載就是將最新的映射結(jié)構(gòu)寫入到外存中，從而保證文件的持久化存儲.

FUN10文件掛載是將文件名到文件元數(shù)據(jù)的映射結(jié)構(gòu)讀取到內(nèi)存中FUN11文件卸載是將文件名到文件元數(shù)據(jù)的映射結(jié)構(gòu)寫入到外存中

1.7 垃圾回收(L7)

在文件系統(tǒng)運行一段時間后，需要執(zhí)行垃圾回收工作.對擁有較少有效頁的塊進行刪除，將其有效數(shù)據(jù)拷貝到新的塊上.

FUN12從所有被使用的塊中查找最合適垃圾回收的塊FUN13刪除塊之前需要將其有效數(shù)據(jù)拷貝到一個新的塊上FUN14拷貝頁上的數(shù)據(jù)后需要更新其對應(yīng)文件的元數(shù)據(jù)

2 文件系統(tǒng)需求建模

上一節(jié)通過分層精化的方法，建立了閃存文件系統(tǒng)所需要實現(xiàn)的14條功能需求和7條環(huán)境需求.另外，本文也提到空間飛行器對文件系統(tǒng)的兩條限制需求：1)減少CPU和外部設(shè)備的交互；2)內(nèi)存空間使用盡可能少.本小節(jié)使用交互式定理證明器Coq對文件系統(tǒng)的需求進行建模.

2.1 數(shù)據(jù)結(jié)構(gòu)

在第1節(jié)中，通過本文對文件系統(tǒng)的需求精化，可以得出文件系統(tǒng)需要如下兩個結(jié)構(gòu)：

1)文件目錄：文件名到文件元數(shù)據(jù)地址的映射.

2)文件元數(shù)據(jù)：文件數(shù)據(jù)具體分布在哪個閃存頁的信息數(shù)據(jù).

在形式化建模分析階段，可以直接省略文件元數(shù)據(jù)地址到文件元數(shù)據(jù)的讀取階段，直接對文件名到文件元數(shù)據(jù)進行抽象.

2.2 模型抽象

實際應(yīng)用中文件系統(tǒng)所管理的文件成千上萬，對其建模無法進行有效的分析.因此，對文件系統(tǒng)進行抽象，假設(shè)文件存儲的閃存有4個塊，而每一塊有6個頁.并且閃存中只存儲文件實際數(shù)據(jù)，文件目錄和文件元數(shù)據(jù)和都放在內(nèi)存中.

(1)文件描述

針對閃存進行建模時不需要考慮內(nèi)存中的文件目錄和文件元數(shù)據(jù)，所以文件在該模型下可以表示為

Inductive block: Type:=|b1 |b2 |b3 |b4.Inductive chunk: Type:=|c1 |c2 |c3 |c4 |c5 |c6.Inductive Ichunk: Type:=

| ic (b: block) (c: chunk).Notation "x - y":= (ic x y).Inductive Inode: Type:=| chunk_nil| chunk_cons (c:Ichunk) (cl: Inode).Notation "c:: cl":= (chunk_cons c cl).Notation "[ ]":= chunk_nil.Notation "[ x;..; y ]":= (chunk_cons x.. (chunk_cons y chunk_nil)..).

Inode就是文件元數(shù)據(jù)的抽象，此時，使用符號“[b1-c1;b1-c3;b1-c5]”即表示文件占用了塊b1的c1、c3、c5閃存頁.

(2)閃存抽象

接下來描述閃存的抽象，簡化模型中假設(shè)閃存有24個頁，所以可以使用閃存頁的狀態(tài)鏈表來抽象系統(tǒng)閃存的狀態(tài).

Inductive chunkState: Type:=|u |f|d.Inductive ChunkList: Type:=CL (s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12s13 s14 s15 s16 s17 s18 s19 s20 s21 s22s23 s24: chunkState).

其中u指的是閃存頁狀態(tài)是被使用，f指的是閃存頁狀態(tài)是未使用，d指的是閃存頁狀態(tài)是有數(shù)據(jù)但已被刪除.如圖4所示，閃存頁狀態(tài)的變換是單向的，f到u，u到d，d再到f，形成循環(huán)，從而使得閃存頁可以被循環(huán)使用.

圖4 閃存頁狀態(tài)的轉(zhuǎn)換Fig.4 Flash chunk state transition

ChunkList就是被定義為這24個閃存頁的狀態(tài)鏈表，使用這個閃存狀態(tài)列表來抽象文件系統(tǒng)的閃存狀態(tài).

(3)內(nèi)存抽象

文件目錄和文件元數(shù)據(jù)都放在內(nèi)存中.文件目錄是通過文件名找到其對應(yīng)的文件元數(shù)據(jù)，所以文件系統(tǒng)在內(nèi)存中可以抽象為Inode的鏈表.

Inductive fileList: Type:=FL (f1 f2 f3 f4: Inode).

假設(shè)模型中有4個文件，因此使用fileList來抽象文件系統(tǒng)中的內(nèi)存狀態(tài).例如，“FL [b1-c1;b1-c2;b1-c3] [b1-c5;b1-c6;b2-c2] [b1-c4;b2-c1] []”表示4個文件中前3個文件有數(shù)據(jù)，第4個文件為空.這4種文件類型也基本覆蓋了在實際使用時文件的分布情況.

(4)系統(tǒng)抽象

文件系統(tǒng)需要對內(nèi)存和外存進行操作，因此關(guān)于文件系統(tǒng)的抽象就需要涉及到內(nèi)存與外存.而空間專用文件系統(tǒng)的外存就是閃存，所以綜合前面的分析，文件系統(tǒng)的模型抽象如表1：

表1 文件系統(tǒng)狀態(tài)的抽象Tab.1 Abstraction of file system state

所以，文件系統(tǒng)狀態(tài)在Coq中抽象如下：

Inductive sysState: Type:=sS (ms:fileList) (fs:ChunkList).

2.3 模型建立

在第1節(jié)文件功能分層精化基礎(chǔ)上，進行形式化建模.

(1)模型初始化

本文在對文件系統(tǒng)建立模型時，將文件數(shù)量固定為4個文件，并且涉及到所有文件的分布情況.4個文件分布情況的設(shè)定如下：第1個文件為連續(xù)的文件，其占用一個塊；第2個文件不連續(xù)，且占用兩個塊；第3個文件不連續(xù)，占用一個塊；第4個文件為空文件.另外，由于閃存的特點是必須按頁順序?qū)懭?，所以前兩個塊被使用，一個塊全部使用，另一個塊部分使用，后兩個塊為空.因此，初始狀態(tài)s0如下：

Definition fileList0:= FL[b1-c1;b1-c2;b1-c3;b1-c4] [b1-c5;b1-c6;b2-c2] [b1-c1;b2-c3] [].Definition chunkList0:= CL u uuuuuuuuuu f ffffffffffff.Definition sysState0:= sS fileList0 chunkList0.

(2)行為描述

行為的具體描述如表2所示.對于文件寫入，抽象兩個行為，其一是向文件f4寫入，也就是向一個空文件寫入數(shù)據(jù)，另一個是向f1寫入，也就是向有數(shù)據(jù)的文件末尾添加數(shù)據(jù).對于文件刪除，抽象一個行為，刪除文件f1.對于垃圾回收操作，抽象一個行為，回收閃存塊b1的數(shù)據(jù).

表2 模型抽象行為描述Tab.2 Model abstract behavior description

在這4個抽象行為的作用下，系統(tǒng)狀態(tài)的轉(zhuǎn)移如圖5所示.

圖5 狀態(tài)轉(zhuǎn)移圖Fig.5 State transition diagram

狀態(tài)sinit是系統(tǒng)最開始的狀態(tài)，它和其他狀態(tài)都是采用虛線連接到一起，表示狀態(tài)sinit通過有限步驟后可以到達其他任意的狀態(tài).sinit描述如下：

Definition fileList0:=FL[] [] [] [].Definition chunkList0:=CL f fffffffffffffffffffffff.Definition sysState0:=sSfileListInitchunkListInit.

(3)狀態(tài)描述

初始狀態(tài)在模型初始化中已經(jīng)描述過了，下面對狀態(tài)轉(zhuǎn)移圖中的s1、s2、s3、s4進行描述.

Definition fileList1:=FL [b1-c1;b1-c2;b1-c3;b1-c4] [b1-c5;b1-c6;b2-c2] [b1-c1;b2-c3] [b2-c4;b2-c5].Definition chunkList1:=CL u uuuuuuuuuu f ffffffffffff.Definition sysState1:= sS fileList1 chunkList1.Definition fileList2:=FL [b1-c1;b1-c2;b1-c3;b1-c4;b2-c6]

[b1-c5;b1-c6;b2-c2] [b1-c1;b2-c3] [b2-c4;b2-c5].Definition chunkList2:=CL u uuuuuuuuuuu f fffffffffff.Definition sysState2:= sS fileList2 chunkList2.Definition fileList3:=FL [] [b1-c5;b1-c6;b2-c2][b1-c1;b2-c3] [b2-c4;b2-c5].Definition chunkList3:=CL d ddd u uuuuuu d f fffffffffff.Definition sysState3:= sS fileList3 chunkList3.Definition fileList4:=FL [] [b3-c1;b3-c2;b2-c2][b1-c1;b2-c3] [b2-c4;b2-c5].Definition chunkList4:=CL f fffff u uuuuuu f ffffffffff.Definition sysState4:= sS fileList4 chunkList4.

2.4 性質(zhì)規(guī)約

結(jié)合文件系統(tǒng)操作的精化描述，以及針對文件系統(tǒng)狀態(tài)建立的模型，提出以下幾條性質(zhì)，并通過證明這幾條性質(zhì)的正確性，表明針對文件系統(tǒng)提出的需求是正確的.

?P1:對文件執(zhí)行完寫操作后，該文件的元數(shù)據(jù)大小會增長.

?P2:執(zhí)行完寫n個頁的操作，頁狀態(tài)列表上u狀態(tài)的頁會增長n個.

?P3:文件元數(shù)據(jù)鏈表上文件對應(yīng)頁的狀態(tài)一定是使用狀態(tài)u.

?P4:刪除文件后，該文件元數(shù)據(jù)對應(yīng)頁的狀態(tài)一定是刪除狀態(tài)d.

?P5:清除某一塊后，該塊對應(yīng)的頁的狀態(tài)為空閑f.

?P6:執(zhí)行清除塊操作時，頁狀態(tài)列表上u狀態(tài)的頁的數(shù)量是不變的.

以上性質(zhì)的形式化描述如圖6所示.符號f、fl、cl、b分別表示文件、文件元數(shù)據(jù)列表、閃存頁狀態(tài)列表、閃存塊.符號f’、fl’、cl’、b’表示的是經(jīng)過函數(shù)操作后的元素.其中，write(f,n)表示往文件f中寫入n個頁的數(shù)據(jù)，size(f)表示文件f的閃存頁個數(shù)，getChunk(f)表示得出文件f對應(yīng)的閃存頁，state(c)表示閃存頁的狀態(tài)，delete(f)表示刪除文件f，getBCh(b)表示得出閃存塊b對應(yīng)的閃存頁，count(cl,u)表示統(tǒng)計閃存頁狀態(tài)列表cl中狀態(tài)為u的閃存頁的數(shù)量.

圖6 性質(zhì)的形式化描述Fig.6 Formal description of properties

3 形式化驗證

在第2節(jié)的簡化模型中，一共有5個文件系統(tǒng)狀態(tài)s0～s4、抽象的4個事件W1、W2、D1、E1以及6個需要證明的全局性質(zhì).

3.1 狀態(tài)轉(zhuǎn)移函數(shù)

首先根據(jù)文件系統(tǒng)相關(guān)操作的定義，在Coq中定義由事件觸發(fā)的狀態(tài)轉(zhuǎn)換函數(shù).

Function transfer(ev:event)(fs: sysState):option sysState:=match ev with…

函數(shù)transfer的代碼比較大，就不在這里展開具體的描述，接下來證明s0～s4之間的轉(zhuǎn)換是正確的.從s0出發(fā)，通過函數(shù)transfer參數(shù)event的不同，證明其可以轉(zhuǎn)換到其他狀態(tài).

3.2 性質(zhì)證明

性質(zhì)P1和P2是針對文件寫操作的，事件W1、W2是關(guān)于寫操作的，所涉及的狀態(tài)關(guān)于s0、s1、s2.因此，在Coq中證明P1和P2的正確性需要證明如下4個定理的正確性.

Theorem P1W1: sizeF (getF4 fileList1) >sizeF (getF4 fileList0).Theorem P1W2: sizeF (getF1 fileL-ist2) >sizeF (getF1 fileList1).Theorem P2W1: count chunkList1 u > count chunkList0 u.Theorem P2W2: count chunkList2 u > count chunkList1 u.

其中g(shù)etF4是根據(jù)文件列表得到第4個文件，getF1是根據(jù)文件列表得到第1個文件，sizeF是根據(jù)文件得到文件大小信息，count是對閃存頁的狀態(tài)信息進行統(tǒng)計.

性質(zhì)P3，文件元數(shù)據(jù)鏈表上文件對應(yīng)頁的狀態(tài)一定是使用狀態(tài)u.對于任意系統(tǒng)狀態(tài)都應(yīng)該是滿足的，因此需要證明如下5個定理.

Theorem P3S0: isUesd (getCSList sysState0) = true.Theorem P3S1: isUesd (getCSList sysState1) = true.Theorem P3S2: isUesd (getCSList sysState2) = true.Theorem P3S3: isUesd (getCSList sysState3) = true.Theorem P3S4: isUesd (getCSList sysState4) = true.

其中，getCSList是根據(jù)系統(tǒng)狀態(tài)得到閃存頁狀態(tài)，isUesd是根據(jù)閃存頁狀態(tài)列表判斷狀態(tài)是否是使用狀態(tài).

性質(zhì)P4是針對刪除一個文件后的性質(zhì).因此需要針對事件D1后的系統(tǒng)狀態(tài)s3進行證明.

Theorem P4D1: isdeleted (getFileCS (getF1 fileList2) chunkList3) = true.

其中，getFileCS是根據(jù)文件找到該文件對應(yīng)的閃存頁列表，isdeleted是根據(jù)文件的閃存頁狀態(tài)列表判斷是否是刪除狀態(tài).

性質(zhì)P5和性質(zhì)P6都是針對清除閃存塊的性質(zhì)，因此需要針對事件E1后的系統(tǒng)狀態(tài)s4進行證明.

Theorem P5E1: isfreed (getBlockCS chunkList4 b1) = true.Theorem P6E1: count chunkList4 u = count chunkList3 u.

其中，getBlockCS是根據(jù)閃存塊得出該閃存塊對應(yīng)頁的狀態(tài)列表，isfreed是根據(jù)閃存頁狀態(tài)列表判斷是否是空閑狀態(tài).

通過對以上定理的證明，表明在2.4節(jié)規(guī)約的6條閃存文件系統(tǒng)需求的性質(zhì)是正確的，從而得出在第1節(jié)所提出的文件系統(tǒng)的功能需求是邏輯正確的.表3中給出驗證文件系統(tǒng)需求的Coq代碼行數(shù)統(tǒng)計.

表3 Coq代碼統(tǒng)計Tab.3 Coq code line statistics

針對航天用閃存文件系統(tǒng)需求的建模與驗證一共花費了2人月，這里面定理驗證部分是最花費時間的部分，占據(jù)了整個證明時間的70%.因為在驗證過程中，如果某條性質(zhì)證明出現(xiàn)問題，則會重新檢查前面函數(shù)的定義是否正確，有時會發(fā)現(xiàn)該函數(shù)定義的不充分，從而需要不斷完善函數(shù)定義，直到完成所有的定理證明工作.通過閃存文件系統(tǒng)需求層的驗證，表明本文提出的閃存文件系統(tǒng)需求的正確性，得出的空間閃存文件系統(tǒng)的規(guī)范可以指導(dǎo)接下來的設(shè)計.

3.3 閃存文件系統(tǒng)需求規(guī)范

從第1節(jié)的分層精化中，可以知道閃存文件系統(tǒng)的基本函數(shù)功能包括文件創(chuàng)建、文件刪除、文件寫入、文件讀取.通過對需求的形式化驗證后，可以得出這些函數(shù)對應(yīng)的需求規(guī)范，如圖7所示.

圖7 文件系統(tǒng)基本函數(shù)需求規(guī)范Fig.7 File system basic function requirements specification

其中文件讀取并不涉及到系統(tǒng)狀態(tài)的改變，只是在內(nèi)存中有讀取的數(shù)據(jù)data文件的掛載與卸載只是元數(shù)據(jù)列表在閃存中的存儲和讀取過程，垃圾回收需要涉及到在設(shè)計閃存文件系統(tǒng)時具體的邏輯地址到物理地址映射機制，在本文提出的需求模型中無法進行形式化規(guī)范.通過本文對文件系統(tǒng)需求層的驗證，建立的文件創(chuàng)建、文件刪除、文件寫入、文件讀取的函數(shù)規(guī)范，可以很好地指導(dǎo)閃存文件系統(tǒng)的設(shè)計與實現(xiàn).

4 結(jié) 論

本文基于空間飛行器的實際需求，以閃存為外部存儲設(shè)備時，通過對需求的分層精化，確定面向空間應(yīng)用的閃存文件系統(tǒng)的功能需求，并對需求進行形式化描述和建模，建立了事件驅(qū)動的狀態(tài)轉(zhuǎn)移模型.并提出在狀態(tài)轉(zhuǎn)移過程中，系統(tǒng)所滿足的全局性質(zhì)，在驗證工具Coq中完成相關(guān)的驗證.最終證明了本文提出的需求是正確的，并建立了面向空間應(yīng)用的閃存文件系統(tǒng)的需求規(guī)范，這為之后開發(fā)安全可靠的空間閃存專用文件系統(tǒng)建立了很好的基礎(chǔ).