一种对NAND闪存硬件和闪存转换层软件的形式化建模
| 摘要 | 第1-7页 |
| ABSTRACT | 第7-9页 |
| 目录 | 第9-12页 |
| 第1章 绪论 | 第12-20页 |
| ·研究背景 | 第12-16页 |
| ·NAND闪存 | 第12-14页 |
| ·闪存转换层 | 第14页 |
| ·基于定理证明的程序验证 | 第14-16页 |
| ·研究内容与研究方法 | 第16-18页 |
| ·研究难点与本文贡献 | 第18-19页 |
| ·符号规范 | 第19页 |
| ·组织结构 | 第19-20页 |
| 第2章 NAND闪存模型的形式化 | 第20-30页 |
| ·形式化验证工具COQ | 第20-21页 |
| ·NAND闪存存储结构 | 第21-22页 |
| ·NAND闪存工作结构 | 第22-23页 |
| ·NAND闪存模型 | 第23-28页 |
| ·数据单元 | 第23-24页 |
| ·页 | 第24-25页 |
| ·块 | 第25-26页 |
| ·Plane | 第26页 |
| ·逻辑单元 | 第26-27页 |
| ·Target | 第27页 |
| ·设备 | 第27-28页 |
| ·本章小结 | 第28-30页 |
| 第3章 NAND闪存操作的形式化 | 第30-50页 |
| ·NAND闪存的操作 | 第30-31页 |
| ·NAND闪存命令的形式化语义 | 第31-44页 |
| ·发送指令的操作语义 | 第32-36页 |
| ·发送地址的操作语义 | 第36-37页 |
| ·等待设备的操作语义 | 第37-41页 |
| ·接收数据的操作语义 | 第41-42页 |
| ·发送数据的操作语义 | 第42-43页 |
| ·读取设备状态的操作语义 | 第43-44页 |
| ·闪存设备驱动的验证 | 第44-48页 |
| ·读操作 | 第44-45页 |
| ·写操作 | 第45-46页 |
| ·擦除操作 | 第46页 |
| ·读取状态命令 | 第46-47页 |
| ·读取设备参数命令 | 第47页 |
| ·重置命令 | 第47-48页 |
| ·NAND闪存设备模型的性质 | 第48页 |
| ·本章小结 | 第48-50页 |
| 第4章 闪存转换层算法的证明框架 | 第50-60页 |
| ·闪存转换层算法 | 第50-52页 |
| ·闪存转换层算法的正确性定义 | 第52-53页 |
| ·闪存转换层算法正确性的形式化证明框架 | 第53-59页 |
| ·本章小结 | 第59-60页 |
| 第5章 一个实际的闪存转换层算法的证明 | 第60-76页 |
| ·BAST算法介绍 | 第60-69页 |
| ·块的信息表和页映射表 | 第63页 |
| ·空闲块队列 | 第63-65页 |
| ·BAST的读算法 | 第65-66页 |
| ·BAST的写算法 | 第66-69页 |
| ·BAST算法的全局不变式 | 第69-75页 |
| ·本章小结 | 第75-76页 |
| 第6章 总结 | 第76-80页 |
| ·工作总结 | 第76-77页 |
| ·未来可能的研究工作 | 第77-80页 |
| 参考文献 | 第80-82页 |
| 致谢 | 第82-84页 |
| 在读期间发表的学术论文与取得的其他研究成果 | 第84页 |
