Name
Abstract | ||
|---|---|---|
We present second steps in the construction of formal models of NAND flash memory, based on a recently emerged open standard for such devices. The model is intended as a key part of a pilot project to develop a verified file store system based on flash memory. The project was proposed by Joshi and Holzmann as a contribution to the Grand Challenge in Verified Software, and involves constructing a highly assured flash file store for use in space-flight missions. The model is at a level of abstraction that captures the internal architecture of NAND flash devices. In this paper, we focus on mechanising the state model and its initialisation operation, where most of the conceptual complexity resides. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1016/j.scico.2008.09.014 | Sci. Comput. Program. |
Keywords | Field | DocType |
theorem proving,file store system,flash memory,formal model,nand flash memory,nand flash device,grand challenge,state model,verified software,veriflcation,verification,flash file store,pilot project,∞ash hardware,flash hardware,open standard | Open standard,Architecture,Flash file system,Programming language,Flash memory,Flash memory emulator,Computer science,Automated theorem proving,NAND gate,Software | Journal |
Volume | Issue | ISSN |
74 | 4 | Science of Computer Programming |
Citations | PageRank | References |
20 | 0.86 | 19 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Andrew Butterfield | 1 | 105 | 9.95 |
| Leo Freitas | 2 | 109 | 9.09 |
| Jim Woodcock | 3 | 21 | 2.62 |