NAND闪存已经成为主流的存储介质,并被广泛地应用到嵌入式、桌面、服务器以及数据中心等各种计算机系统中,并仍迅速地挤占传统纯磁性材料存储介质的市场。与此同时,在航空航天、国防军工,核电,医疗设备等一些安全攸关领域,NAND闪存也因其存储密度高、抗震性好、低功耗等特点得到了越来越多的应用。然而NAND闪存的一些独有的物理特性导致了其与传统机械硬盘相比,具有天然的存储不稳定性。例如NAND闪存存在着磨损的问题,即经过多次读写之后的闪存单元会变得越来越不稳定,而且超过一定的擦除次数之后,存储单元就会彻底报废。又例如闪存单元读写会引入电流干扰,即在写一个存储单元时,电流引起相邻的存储单元的位翻转。NAND闪存的这些物理特性就对管理NAND的软件提出了更高的要求。一种较为常见的解决方案引入一个被称为闪存转换层(Flash Translation Layer, FTL)的软件层,用以隐藏这些物理特性,使得NAND闪存可以像传统的机械硬盘一样进行任意读写。在过去的十多年里,有大量FTL软件相关的算法被提出。为了兼顾稳定性、性能,可靠性,这类算法通常比其他存储介质的管理软件更为复杂,也更容易出现问题。为了构建高可信的基于NAND闪存存储的系统软件,通过严格的形式化方法对NAND闪存硬件进行建模,对管理NAND闪存的FTL软件层的行为进行正确性验证具有一定的理论和实际意义。首先,本文根据一个被众多闪存生产厂商广泛接受认可的NAND闪存接口标准ONFI3.0,采用形式化语言对NAND闪存硬件的真实语义进行形式化建模。本文提出的形式化模型包括ONFI所定义的NAND闪存硬件的存储层次结构、闪存硬件芯片处理命令的内部工作流程、闪存硬件的命令集,以及在此基础之上定义的闪存的基本操作。本文的NAND闪存形式化模型在定理证明工具Coq中定义实现。在Coq工具中,该模型的一些性质也得到了完整地证明。该模型可以直接被用来作为验证基于NAND闪存硬件的存储系统软件的基础。其次,本文使用基于不变式的证明方法建立了一个通用的、可以验证各种闪存转换层正确性的形式化框架。所谓的正确性是指：在正确的初始条件下,,一个运行着正确的闪存转换层算法的NAND闪存与一块传统机械硬盘在相同的读写命令序列之后将输出同样的数据。在该形式化框架中,本文首次定义了一个经典的闪存转换层算法(BAST),并证明了算法的正确性。本文所建立的形式化NAND闪存模型和闪存转换层算法证明框架为验证其上运行的嵌入式操作系统及其它嵌入式软件提供了严格的形式化模型,并将为基于NAND闪存的高可信嵌入式软件的开发提供一个坚实的基础