Abstract
Flash translation layer (FTL) is a part of software running on the NAND flash memory, which is ubiquitous in various devices. FTL algorithm hides the complexity of NAND flash characteristics and provides a simple and standard interface like magnetic disks. In this paper, we present a general and abstract formal model for FTL algorithms, define their functional correctness as refinement, and propose a verification framework. We demonstrate its use by verifying a classic FTL algorithm BAST. Our entire development has been formalized in the proof assistant Coq.
Author supplied keywords
Cite
CITATION STYLE
Qiao, L., Li, S., Yang, H., & Yang, M. (2019). A formal modeling and verification framework for flash translation layer algorithms. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11951 LNCS, pp. 72–88). Springer. https://doi.org/10.1007/978-3-030-35540-1_5
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
