Formal Modeling Of NAND Hardware And Flash Translation Layer

As a popular storage medium, NAND flash has been widely used among various computer systems, such as embedded devices, desktop PCs, commercial databases and massive data center. Furthermore, it has been introduced to safety-critical systems, like aerospace and military fields for its high storage density and favorable shock resistance. In those important fields, the application of NAND flash has been increasing dramatically. The physical characteristics of NAND flash are quite different from common hard disk drives. To hide properties, there is a unique layer named flash translation layer, FTL. Due to the properties and the layer, NAND flash is more complicated than other stroage media. Thus, it makes sense to build high-confidence software system on NAND flash by formally verifing and modeling NAND flash.First, according to an open NAND Flash interface specification named ONFI that is recognized by many companies, in this thesis, a formal model for the realistic semantics of NAND flash hardware is built by formal languages. It includes the storage architecture of NAND flash defined by ONFI, the inner workflow of the commands, the command set of the NAND flash and several flash operations defined upon the model. The model is defined in a popular theorem proof assistant, Coq. This model can be used to define and verify the software based on NAND flash storage system.Second, this thesis proposes a general framework to prove the correctness of flash translation layers by using invariant-based proof techniques. This thesis also defines their functional correctness as refinement.The correctness suggests that if there are a hard disk and a flash device, when we send the same sequence of read/write commands to the two devices simultaneously, we expect to get exactly the same data from them. For instance, a classical flash translation algorithm BAST is verified completely. It shows the framework can be used to prove correctness of various flash translation layer algorithms.This thesis provide an abstract model of formal NAND flash and a formal framework to verify flash translation layer algorithm as a solid base for further verification work of embedded operating system and software on NAND flash.