声明
摘要
第1章 绪论
1.1 研究背景
1.1.1 NAND闪存
1.1.2 闪存转换层
1.1.3 基于定理证明的程序验证
1.2 研究内容与研究方法
1.3 研究难点与本文贡献
1.4 符号规范
1.5 组织结构
第2章 NAND闪存模型的形式化
2.1 形式化验证工具Coq
2.2 NAND闪存存储结构
2.3 NAND闪存工作结构
2.4 NAND闪存模型
2.4.1 数据单元
2.4.2 页
2.4.3 块
2.4.4 Plane
2.4.5 逻辑单元
2.4.6 Target
2.4.7 设备
2.5 本章小结
第3章 NAND闪存操作的形式化
3.1 NAND闪存的操作
3.2 NAND闪存命令的形式化语义
3.2.1 发送指令的操作语义
3.2.2 发送地址的操作语义
3.2.3 等待设备的操作语义
3.2.4 接收数据的操作语义
3.2.5 发送数据的操作语义
3.2.6 读取设备状态的操作语义
3.3 闪存设备驱动的验证
3.3.1 读操作
3.3.2 写操作
3.3.3 擦除操作
3.3.4 读取状态命令
3.3.5 读取设备参数命令
3.3.6.重置命令
3.3.7 NAND闪存设备模型的性质
3.4 本章小结
第4章 闪存转换层算法的证明框架
4.1 闪存转换层算法
4.2 闪存转换层算法的正确性定义
4.3 闪存转换层算法正确性的形式化证明框架
4.4 本章小结
第5章 一个实际的闪存转换层算法的证明
5.1 BAST算法介绍
5.1.1 块的信息表和页映射表
5.1.2 空闲块队列
5.1.3 BAST的读算法
5.1.4 BAST的写算法
5.2 BAST算法的全局不变式
5.3 本章小结
第6章 总结
6.1 工作总结
6.2 未来可能的研究工作
参考文献
致谢
在读期间发表的学术论文与取得的其他研究成果