Designing and Analyzing a Flash File System with Alloy
Eunsuk Kang, Daniel Jackson · 2009
Abstract Alloy is a lightweight modeling language based on first-order relational logic. The language is expressive enough to describe structurally complex systems, but simple enough to be amenable to fully automated analysis. The Alloy Analyzer, with its SATbased analysis engine, allows one to simulate traces of a system, visualize them, or search for counterexamples to a property. This article illustrates key concepts of Alloy using, as an example, the construction and analysis of a design for a flash file system. In addition to basic file operations, the design includes features that are crucial to NAND flash memory but contribute to increased complexity of the file system, such as wear leveling and erase-unit reclamation. The design also addresses the issues of fault-tolerance by providing a mechanism for recovering from unexpected hardware failures. The article describes the modeling process and discusses the results of the design analysis, which has been carried out by checking trace inclusion of the flash file system against a POSIX-compliant abstract file system. Key words: software design; formal specification; modeling; analysis; Alloy