一种对NAND闪存硬件和闪存转换层软件的形式化建模

发布时间：2017-04-08 22:15

  本文关键词：一种对NAND闪存硬件和闪存转换层软件的形式化建模，，由笔耕文化传播整理发布。

【摘要】：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闪存的高可信嵌入式软件的开发提供一个坚实的基础
【关键词】：形式化验证 闪存转换层 闪存设备 形式化建模 高可信软件 存储系统
【学位授予单位】：中国科学技术大学
【学位级别】：硕士
【学位授予年份】：2015
【分类号】：TP333
【目录】：

• 摘要5-7
• ABSTRACT7-9
• 目录9-12
• 第1章 绪论12-20
• 1.1 研究背景12-16
• 1.1.1 NAND闪存12-14
• 1.1.2 闪存转换层14
• 1.1.3 基于定理证明的程序验证14-16
• 1.2 研究内容与研究方法16-18
• 1.3 研究难点与本文贡献18-19
• 1.4 符号规范19
• 1.5 组织结构19-20
• 第2章 NAND闪存模型的形式化20-30
• 2.1 形式化验证工具COQ20-21
• 2.2 NAND闪存存储结构21-22
• 2.3 NAND闪存工作结构22-23
• 2.4 NAND闪存模型23-28
• 2.4.1 数据单元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 设备27-28
• 2.5 本章小结28-30
• 第3章 NAND闪存操作的形式化30-50
• 3.1 NAND闪存的操作30-31
• 3.2 NAND闪存命令的形式化语义31-44
• 3.2.1 发送指令的操作语义32-36
• 3.2.2 发送地址的操作语义36-37
• 3.2.3 等待设备的操作语义37-41
• 3.2.4 接收数据的操作语义41-42
• 3.2.5 发送数据的操作语义42-43
• 3.2.6 读取设备状态的操作语义43-44
• 3.3 闪存设备驱动的验证44-48
• 3.3.1 读操作44-45
• 3.3.2 写操作45-46
• 3.3.3 擦除操作46
• 3.3.4 读取状态命令46-47
• 3.3.5 读取设备参数命令47
• 3.3.6. 重置命令47-48
• 3.3.7 NAND闪存设备模型的性质48
• 3.4 本章小结48-50
• 第4章 闪存转换层算法的证明框架50-60
• 4.1 闪存转换层算法50-52
• 4.2 闪存转换层算法的正确性定义52-53
• 4.3 闪存转换层算法正确性的形式化证明框架53-59
• 4.4 本章小结59-60
• 第5章 一个实际的闪存转换层算法的证明60-76
• 5.1 BAST算法介绍60-69
• 5.1.1 块的信息表和页映射表63
• 5.1.2 空闲块队列63-65
• 5.1.3 BAST的读算法65-66
• 5.1.4 BAST的写算法66-69
• 5.2 BAST算法的全局不变式69-75
• 5.3 本章小结75-76
• 第6章 总结76-80
• 6.1 工作总结76-77
• 6.2 未来可能的研究工作77-80
• 参考文献80-82
• 致谢82-84
• 在读期间发表的学术论文与取得的其他研究成果84

【参考文献】

中国期刊全文数据库 前1条

1 李胜广;张其善;;闪存设备在嵌入式Linux系统中的应用[J];计算机工程;2007年02期

  本文关键词：一种对NAND闪存硬件和闪存转换层软件的形式化建模，由笔耕文化传播整理发布。

本文编号：293825