| 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. |
