面向空间飞行器的文件系统需求层验证

李少峰， 杨孟飞， 乔 磊， 姜菁菁， 王婷煜

1. 西安电子科技大学,西安 710071 2. 中国空间技术研究院,北京 100094 3. 北京控制工程研究所,北京 100094

0 引 言

空间嵌入式环境比较恶劣，需要对计算机上相关的器件进行特殊的保护，因为目前工艺的局限性，空间计算机无法像地面计算机一样拥有充分的系统资源，其系统资源通常都比较小.文件系统的索引结构和元数据通常都比较大，为了文件系统的快速响应，通常都需要这些数据长时间驻留在内存中.在空间设备中，往往没有足够的内存空间存放这些数据，因此，根据空间设备的特点，需要设计专用于空间飞行器的文件系统.

NAND型闪存的优点在于写入/擦除速度快、存储容量大[1]，因此常作为数据储存设备，在各种计算机系统中得到了广泛的使用，从嵌入式设备到笔记本电脑、台式机和数据中心.与传统磁盘相比，它有了巨大的性能提升并且节省了功耗，同时，存储数据的量也更大.但是，由于其物理特性，无法进行原地更新，如果系统要覆盖设备中的旧数据单元，它必须擦除包含该单元的整个块.所以，在磁盘上广泛使用的文件系统并不能直接在闪存上使用，例如FAT、EXT3[2]等.

图1 Nand型闪存为外部存储设备的文件系统结构Fig.1 System structure of external storage device with Nand flash

通常的解决方案是设计闪存转换层FTL(flash translation layer)[3]，如图1(a)，提供地址映射、垃圾回收、磨损均衡等功能，使得磁盘文件系统可以在闪存上运行.虽然乔磊等[4]通过形式化方法验证了FTL层的正确性.但是，这样的解决方案无法充分利用闪存的特性并且十分耗时，在实时性强的嵌入式设备中无法满足设备的时序要求.

专用闪存文件系统是指根据闪存的特性，设计可以在其上面运行的文件系统，它直接管理闪存设备，能充分发挥闪存的存储优势，如图1(b)所示.目前已有的闪存文件系统包括JFFSx[5]、YAFFS[6]、UBIFS[7]等.

空间设备多采用Nand型闪存作为数据的存储介质.但是，目前的闪存文件系统的内存占用情况都比较大，同时，文件系统的实时性也不够.因此，设计专用于空间设备的闪存文件系统是亟需解决的问题.

另外，采用严格的形式化方法对文件系统进行设计和实现是公认的可靠方法.GALLWAY等[8]使用模型检测的方法对Linux虚拟文件系统进行了形式化验证，对系统的实际运行情况进行分析，并对数据完整性等约束条件的可满足性进行验证.HSSELINK等[9]形式化验证了一款抽象文件系统，并从文件系统的高层次出发，逐层进行抽象描述，验证系统符合规范.钱振江等[10]对微内核架构下的VTOS系统中的文件系统模块进行了形式化的建模与验证，使用状态机模型在Isabelle/HOL定理工具中完成了证明.CHEN等[11]提出第1个具有机器可检查证明的文件系统FSCQ，使用基于霍尔逻辑扩展的崩溃霍尔逻辑进行验证.ZOU等[12]提出第1个形式化验证的、细粒度的并发文件系统AtomFS.LI等[13]提出了形式化模型来准确描述底层读写行为，对文件系统进行验证.

空间飞行器中应用最广泛的操作系统是SpaceOS[14]，相关研究团队对该系统的内存管理[15-16]、中断管理[17-18]、任务管理[19]等模块进行了形式化验证，因此，要开发一款在空间设备上使用的文件系统，需要对其进行形式化验证.

目前，针对文件系统的验证工作大多都是在系统开发工作结束之后，证明所实现代码符合其针对文件系统建立的形式规范，从而表明其所验证文件系统的正确性.而本文尝试在空间飞行器文件系统的需求分析阶段就引入形式化验证，证明所提出的功能需求是正确的，为后续的设计与开发提供必要的函数规范.

空间飞行器以Nand型闪存为外部存储介质，需要利用闪存的特点[20]进行文件系统的研究工作.本文使用形式化的方法提出空间飞行器文件系统的功能需求，并进行验证，证明所提出需求的正确性.

1 空间飞行器文件系统需求

通用计算机的硬件结构如图2所示，是典型的I/O总线结构.对于通用计算机来说，最常用的便是PCI(peripheral component interconnect)总线.因为总线的传输速度快，且内存空间也足够大，所以通用计算机的文件系统往往比较大，占用了过多的内存空间.当外部设备为Flash设备时，其也往往通过在系统中添加FTL层进行转换.但是对于实时性要求非常高的空间飞行器来说，使用这种方式的文件系统是不合适的.

因此，需要设计以Nand型闪存为外部存储设备的专用闪存文件系统.在空间飞行器的应用环境下，其还有以下两个限制:1)空间设备的总线使用的是1553B总线，其速度比较慢，相比于高速运行的CPU，其很容易成为系统的瓶颈，所以设计的文件系统需要减少CPU与外部设备的交互，从而减少使用总线通信.2)空间设备的内存十分有限，设计的文件系统应该使用较少的内存空间.

图2 I/O总线结构Fig.2 I/O bus structure

接下来针对空间飞行器文件系统的这两个限制，提出基于闪存的空间专用文件系统需求.针对于文件系统的功能需求，使用标签FUN表示；对于文件系统对底层操作系统的要求，认为是文件系统所处的环境，使用标签ENV表示.

图3 文件系统需求分层精化Fig.3 Hierarchical refinement of file system requirements

如图3所示，将嵌入式文件系统的需求分为7层进行精化分析.并针对每一层提出功能需求和所处环境要求，然后提炼出需满足的性质并进行相应的验证.

1.1 数据读写(L1)

首先考虑文件系统最基本的需求，将内存中的数据写入到存储设备中，达到持久化存储数据的目的.当程序需要使用数据时，从存储设备中读出相应的数据到内存中.

FUN1写入数据将数据从内存拷贝到外存FUN2读取数据将数据从外存拷贝到内存

对于文件所处的环境定义如下：

ENV1假定文件是一个数据项的序列ENV2文件在内存与外存之间以一个个片段的方式传输ENV3外存的物理介质是闪存

1.2 文件创建(L2)

在写文件之前，需要判断该文件是否存在，如果不存在则创建该文件，并从文件数据区域开始写入文件.

FUN3创建文件是建立文件名到文件元数据位置的映射关系FUN4新创建的文件元数据,内容为空,即不包含文件实际的存储位置信息

文件目录和文件元数据所处的环境如下：

ENV4文件名到文件元数据位置的映射关系本质上就是文件目录,其在文件系统运行期间存储在内存中ENV5文件的元数据在文件系统运行期间存储在内存中

1.3 文件删除(L3)

与文件创建对应，当文件数据过时后，需要对文件进行删除.

FUN5删除文件是将文件名到文件元数据位置的映射信息删除,并删除文件元数据和文件数据FUN6删除文件数据是将文件数据所在的闪存页的状态标记为无效

1.4 文件读取(L4)

文件读取是通过文件元数据信息，将文件的数据信息读取到内存中.

FUN7通过文件元数据,将文件读取分解为n段数据读取(n>0)

文件读取的环境如下：

ENV6每一段数据的大小与闪存的最小数据单元闪存页的大小一致

1.5 文件写入(L5)

对于文件写入分为两个方面：不改变文件原有数据和改变文件原有数据两种情况.

FUN8文件尾部添加数据时,进行数据写入操作,并更新文件的元数据FUN9更改原有数据时,先删除原有数据,再写入新的数据,更新文件元数据

文件写入的环境如下：

ENV7写入数据的大小与闪存的最小数据单元闪存页的大小一致

1.6 文件系统挂载与卸载(L6)

文件目录是指文件名到文件元数据的映射。文件系统的挂载就是将这个映射结构读取到内存中.文件系统的卸载就是将最新的映射结构写入到外存中，从而保证文件的持久化存储.

FUN10文件挂载是将文件名到文件元数据的映射结构读取到内存中FUN11文件卸载是将文件名到文件元数据的映射结构写入到外存中

1.7 垃圾回收(L7)

在文件系统运行一段时间后，需要执行垃圾回收工作.对拥有较少有效页的块进行删除，将其有效数据拷贝到新的块上.

FUN12从所有被使用的块中查找最合适垃圾回收的块FUN13删除块之前需要将其有效数据拷贝到一个新的块上FUN14拷贝页上的数据后需要更新其对应文件的元数据

2 文件系统需求建模

上一节通过分层精化的方法，建立了闪存文件系统所需要实现的14条功能需求和7条环境需求.另外，本文也提到空间飞行器对文件系统的两条限制需求：1)减少CPU和外部设备的交互；2)内存空间使用尽可能少.本小节使用交互式定理证明器Coq对文件系统的需求进行建模.

2.1 数据结构

在第1节中，通过本文对文件系统的需求精化，可以得出文件系统需要如下两个结构：

1)文件目录：文件名到文件元数据地址的映射.

2)文件元数据：文件数据具体分布在哪个闪存页的信息数据.

在形式化建模分析阶段，可以直接省略文件元数据地址到文件元数据的读取阶段，直接对文件名到文件元数据进行抽象.

2.2 模型抽象

实际应用中文件系统所管理的文件成千上万，对其建模无法进行有效的分析.因此，对文件系统进行抽象，假设文件存储的闪存有4个块，而每一块有6个页.并且闪存中只存储文件实际数据，文件目录和文件元数据和都放在内存中.

(1)文件描述

针对闪存进行建模时不需要考虑内存中的文件目录和文件元数据，所以文件在该模型下可以表示为

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就是文件元数据的抽象，此时，使用符号“[b1-c1;b1-c3;b1-c5]”即表示文件占用了块b1的c1、c3、c5闪存页.

(2)闪存抽象

接下来描述闪存的抽象，简化模型中假设闪存有24个页，所以可以使用闪存页的状态链表来抽象系统闪存的状态.

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指的是闪存页状态是被使用，f指的是闪存页状态是未使用，d指的是闪存页状态是有数据但已被删除.如图4所示，闪存页状态的变换是单向的，f到u，u到d，d再到f，形成循环，从而使得闪存页可以被循环使用.

图4 闪存页状态的转换Fig.4 Flash chunk state transition

ChunkList就是被定义为这24个闪存页的状态链表，使用这个闪存状态列表来抽象文件系统的闪存状态.

(3)内存抽象

文件目录和文件元数据都放在内存中.文件目录是通过文件名找到其对应的文件元数据，所以文件系统在内存中可以抽象为Inode的链表.

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

假设模型中有4个文件，因此使用fileList来抽象文件系统中的内存状态.例如，“FL [b1-c1;b1-c2;b1-c3] [b1-c5;b1-c6;b2-c2] [b1-c4;b2-c1] []”表示4个文件中前3个文件有数据，第4个文件为空.这4种文件类型也基本覆盖了在实际使用时文件的分布情况.

(4)系统抽象

文件系统需要对内存和外存进行操作，因此关于文件系统的抽象就需要涉及到内存与外存.而空间专用文件系统的外存就是闪存，所以综合前面的分析，文件系统的模型抽象如表1：

表1 文件系统状态的抽象Tab.1 Abstraction of file system state

所以，文件系统状态在Coq中抽象如下：

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

2.3 模型建立

在第1节文件功能分层精化基础上，进行形式化建模.

(1)模型初始化

本文在对文件系统建立模型时，将文件数量固定为4个文件，并且涉及到所有文件的分布情况.4个文件分布情况的设定如下：第1个文件为连续的文件，其占用一个块；第2个文件不连续，且占用两个块；第3个文件不连续，占用一个块；第4个文件为空文件.另外，由于闪存的特点是必须按页顺序写入，所以前两个块被使用，一个块全部使用，另一个块部分使用，后两个块为空.因此，初始状态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写入，也就是向一个空文件写入数据，另一个是向f1写入，也就是向有数据的文件末尾添加数据.对于文件删除，抽象一个行为，删除文件f1.对于垃圾回收操作，抽象一个行为，回收闪存块b1的数据.

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

在这4个抽象行为的作用下，系统状态的转移如图5所示.

图5 状态转移图Fig.5 State transition diagram

状态sinit是系统最开始的状态，它和其他状态都是采用虚线连接到一起，表示状态sinit通过有限步骤后可以到达其他任意的状态.sinit描述如下：

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

(3)状态描述

初始状态在模型初始化中已经描述过了，下面对状态转移图中的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 性质规约

结合文件系统操作的精化描述，以及针对文件系统状态建立的模型，提出以下几条性质，并通过证明这几条性质的正确性，表明针对文件系统提出的需求是正确的.

•P1:对文件执行完写操作后，该文件的元数据大小会增长.

•P2:执行完写n个页的操作，页状态列表上u状态的页会增长n个.

•P3:文件元数据链表上文件对应页的状态一定是使用状态u.

•P4:删除文件后，该文件元数据对应页的状态一定是删除状态d.

•P5:清除某一块后，该块对应的页的状态为空闲f.

•P6:执行清除块操作时，页状态列表上u状态的页的数量是不变的.

以上性质的形式化描述如图6所示.符号f、fl、cl、b分别表示文件、文件元数据列表、闪存页状态列表、闪存块.符号f’、fl’、cl’、b’表示的是经过函数操作后的元素.其中，write(f,n)表示往文件f中写入n个页的数据，size(f)表示文件f的闪存页个数，getChunk(f)表示得出文件f对应的闪存页，state(c)表示闪存页的状态，delete(f)表示删除文件f，getBCh(b)表示得出闪存块b对应的闪存页，count(cl,u)表示统计闪存页状态列表cl中状态为u的闪存页的数量.

图6 性质的形式化描述Fig.6 Formal description of properties

3 形式化验证

在第2节的简化模型中，一共有5个文件系统状态s0～s4、抽象的4个事件W1、W2、D1、E1以及6个需要证明的全局性质.

3.1 状态转移函数

首先根据文件系统相关操作的定义，在Coq中定义由事件触发的状态转换函数.

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

函数transfer的代码比较大，就不在这里展开具体的描述，接下来证明s0～s4之间的转换是正确的.从s0出发，通过函数transfer参数event的不同，证明其可以转换到其他状态.

3.2 性质证明

性质P1和P2是针对文件写操作的，事件W1、W2是关于写操作的，所涉及的状态关于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.

其中getF4是根据文件列表得到第4个文件，getF1是根据文件列表得到第1个文件，sizeF是根据文件得到文件大小信息，count是对闪存页的状态信息进行统计.

性质P3，文件元数据链表上文件对应页的状态一定是使用状态u.对于任意系统状态都应该是满足的，因此需要证明如下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是根据系统状态得到闪存页状态，isUesd是根据闪存页状态列表判断状态是否是使用状态.

性质P4是针对删除一个文件后的性质.因此需要针对事件D1后的系统状态s3进行证明.

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

其中，getFileCS是根据文件找到该文件对应的闪存页列表，isdeleted是根据文件的闪存页状态列表判断是否是删除状态.

性质P5和性质P6都是针对清除闪存块的性质，因此需要针对事件E1后的系统状态s4进行证明.

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

其中，getBlockCS是根据闪存块得出该闪存块对应页的状态列表，isfreed是根据闪存页状态列表判断是否是空闲状态.

通过对以上定理的证明，表明在2.4节规约的6条闪存文件系统需求的性质是正确的，从而得出在第1节所提出的文件系统的功能需求是逻辑正确的.表3中给出验证文件系统需求的Coq代码行数统计.

表3 Coq代码统计Tab.3 Coq code line statistics

针对航天用闪存文件系统需求的建模与验证一共花费了2人月，这里面定理验证部分是最花费时间的部分，占据了整个证明时间的70%.因为在验证过程中，如果某条性质证明出现问题，则会重新检查前面函数的定义是否正确，有时会发现该函数定义的不充分，从而需要不断完善函数定义，直到完成所有的定理证明工作.通过闪存文件系统需求层的验证，表明本文提出的闪存文件系统需求的正确性，得出的空间闪存文件系统的规范可以指导接下来的设计.

3.3 闪存文件系统需求规范

从第1节的分层精化中，可以知道闪存文件系统的基本函数功能包括文件创建、文件删除、文件写入、文件读取.通过对需求的形式化验证后，可以得出这些函数对应的需求规范，如图7所示.

图7 文件系统基本函数需求规范Fig.7 File system basic function requirements specification

其中文件读取并不涉及到系统状态的改变，只是在内存中有读取的数据data文件的挂载与卸载只是元数据列表在闪存中的存储和读取过程，垃圾回收需要涉及到在设计闪存文件系统时具体的逻辑地址到物理地址映射机制，在本文提出的需求模型中无法进行形式化规范.通过本文对文件系统需求层的验证，建立的文件创建、文件删除、文件写入、文件读取的函数规范，可以很好地指导闪存文件系统的设计与实现.

4 结 论

本文基于空间飞行器的实际需求，以闪存为外部存储设备时，通过对需求的分层精化，确定面向空间应用的闪存文件系统的功能需求，并对需求进行形式化描述和建模，建立了事件驱动的状态转移模型.并提出在状态转移过程中，系统所满足的全局性质，在验证工具Coq中完成相关的验证.最终证明了本文提出的需求是正确的，并建立了面向空间应用的闪存文件系统的需求规范，这为之后开发安全可靠的空间闪存专用文件系统建立了很好的基础.