形式化建模运行在NAND闪存上的DFTL算法

Formal Modeling of the DFTL Algorithm for Based on the NAND Flash

为了保证一种非常经典的适用大规模存储地NAND闪存上的DFTL算法的正确性,对DFTL算法采用了形式化建模的方法来建立一个高可信的形式化模型.根据DFTL算法提出者的设计,我们以此为依据,对DFTL算法的基本数据结构,读写操作和垃圾回收操作以及基本性质进行了形式化的建模和验证,并对文中提出的垃圾回收算法进行了适当的修改和优化,以证明垃圾回收算法的正确性.最后我们针对DFTL算法,设计了一个验证框架,在这个验证框架和形式化的NAND闪存模型的基础上,对DFTL算法的的一些基本性质进行了验证.

In this paper, in order to guarantee the correctness of a very classical algorithm DFTL which based on the mass storageNAND flash, we use the formal methods to analysis and model a high trustworthy model of the DFTL algorithm. According to the au-thor＇ s design, we model the basic data structure, the read-write operation, the garbage collection operation and the nature of the DFTLalgodthra. And then in order to prove the correctness of garbage collection algorithm, we model the garbage collection algorithm whichwe have taken some measures to optimize and improve. At last, we design a erification framework and we have proved some basicproperties of the DFTL algorithm based on this framework and a formal model of NAND flash.