Formal Modeling and Analysis of a Flash Filesystem in Alloy

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 clusion 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.

• Type: Conference
• Year: 2008
• Where: ASM
• Authors: Eunsuk Kang, Daniel Jackson
• Keywords: ASM 2008, Computational Biology, Filesystem, Flash-based Filesystem, Interrupted Filesystem Operations