Abstract
This paper describes the formal modeling and analysis of a design for a flash-based filesystem in Alloy. We model the basic operations of a filesystem as well as features that are crucial to NAND flash hardware, such as wear-leveling and erase-unit reclamation. In addition, we address the issue of fault tolerance by modeling a mechanism for recovery from interrupted filesystem operations due to unexpected power loss. We analyze the correctness of our flash filesystem model by checking trace inclusion against a POSIX-compliant abstract filesystem, in which a file is modeled simply as an array of data elements. The analysis is fully automatic and complete within a finite scope. © 2008 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Kang, E., & Jackson, D. (2008). Formal modeling and analysis of a flash filesystem in Alloy. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5238 LNCS, pp. 294–308). https://doi.org/10.1007/978-3-540-87603-8_23
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
