Project Overview

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.

Contributors

Eunsuk Kang, Daniel Jackson

Relevant Links

Modeling and analysis of a flash filesystem Paper