| Designing and Analyzing a Flash File System with Alloy |
| Received:February 01, 2009 Revised:August 09, 2009 Download PDF |
| Eunsuk Kang,Daniel Jackson. Designing and Analyzing a Flash File System with Alloy. International Journal of Software and Informatics, 2009,3(2):129~148 |
| Hits: 4954 |
| Download times: 3397 |
|
| Fund:This work is supported by the National Science Foundation under Grant Nos. 0541183 and 0438897,
and by the Nokia Corporation as part of a collaboration between Nokia Research and MIT’s Com
-puter Science and Arti.cial Intelligence Lab. |
|
| Abstract:Alloy is a lightweight modeling language based on .rst-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 SAT-based 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 .ash .le system. In addition to basic .le operations, the design includes features that are crucial to NAND .ash memory but contribute to increased complexity of the .le 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 .ash .le system against a POSIX-compliant abstract .le system. |
| keywords:software design formal speci.cation modeling analysis Alloy |
| View Full Text View/Add Comment Download reader |
|
|
|
