Mechanising a formal model of flash memory

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

Full description

Saved in:
Bibliographic Details
Published in:Science of computer programming 2009-02, Vol.74 (4), p.219-237
Main Authors: Butterfield, Andrew, Freitas, Leo, Woodcock, Jim
Format: Article
Language:English
Subjects:
Flash hardware
Grand challenge
Theorem proving
Verification
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0167-6423
1872-7964
DOI:10.1016/j.scico.2008.09.014