Modeling and Analysis of a Flash Filesystem
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 filesystem in Alloy. Our model includes 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 have addressed 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 our flash filesystem model by checking trace inclusion against a POSIX-compliant abstract filesystem.
Alloy Model of the Flash Filesystem
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 filesystem
- flash.als - Model of the NAND flash hardware
- concreteFilesystem.als - Flash filesystem model
- refinement.als - Refinement properties for file operations
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)