Formalising Flash Memory: First Steps

We present first steps in the construction of formal models of NAND Flash memory, based on a recently emerged open standard for such devices. The model is at a level of abstraction that captures the internal architecture of such a device, as well as the commands that are used to operate it. The model is intended as a key step in a plan to develop a verified filestore system, by providing a description of the hardware devices that would be used in it implementation.

• Type: Conference
• Year: 2007
• Where: ICECCS
• Authors: Andrew Butterfield, Jim Woodcock
• Keywords: Hardware, ICECCS 2007, NAND Flash Memory, Verified filestore System, first Steps