Modeling and Analysis of a Flash File System
As a contribution to the second pilot project in the Verified Software Repository (VSR), we have formally modeled and analyzed a design of a flash file system in Alloy. Our model includes basic operations of a file system as well as features that are crucial to NAND flash hardware, such as wear-leveling and garbage collection. In addition, our design addresses the issue of fault-tolerance by modeling a mechanism for recovery from interrupted file operations due to unexpected power loss. We have analyzed the correctness of the design by checking trace inclusion against a POSIX-compliant abstract file system.
Alloy Model of the Flash File System
The Alloy model is available for download. Here is a description of the files in the archive:
- abstractFilesystem.als: Model of a POSIX-compliant abstract file system
- flash.als: Model of the NAND flash hardware
- blockManager.als: Model for a layer between the flash hardware and the client-level file system interface
- concreteFilesystem.als: Top-level file system interface
- faultToleranceUnit.als: Fault-tolerance mechanism
- refinement.als: Refinement properties between the concrete and abstract file systems
In addition, for each of the .als files in the above list, we have also included a custom visualization file (with an extension .thm) for simulation runs.
Members
- Eunsuk Kang (SDG)
- Daniel Jackson (SDG)