%0 Journal Article
%T 形式化建模运行在NAND闪存上的DFTL算法
%A 张必红
%A 李兆鹏
%A 郭宇
%J 中山大学学报（自然科学版）
%D 2018
%X 摘要 为了保证一种非常经典的适用大规模存储地NAND闪存上的DFTL算法的正确性，对DFTL算法采用了形式化建模的方法来建立一个高可信的形式化模型.根据DFTL算法提出者的设计，我们以此为依据，对DFTL算法的基本数据结构，读写操作和垃圾回收操作以及基本性质进行了形式化的建模和验证，并对文中提出的垃圾回收算法进行了适当的修改和优化，以证明垃圾回收算法的正确性.最后我们针对DFTL算法，设计了一个验证框架，在这个验证框架和形式化的NAND闪存模型的基础上，对DFTL算法的的一些基本性质进行了验证
%K 形式化方法
%K 形式化建模
%K Coq证明
%K 闪存安全
%K 信息安全
%K 闪存转换层算法
%U http://xwxt.sict.ac.cn/CN/abstract/abstract4279.shtml