University of Limerick
Browse
Merchandising a formal model ( Butterfield).pdf (224.34 kB)

Mechanising a formal model of flash memory

Download (224.34 kB)
journal contribution
posted on 2010-12-20, 12:23 authored by Andrew Butterfield, Leo Freitas, Jim Woodcock
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.

History

Publication

Science of Computer Programming;74/ 4/ 219-237

Publisher

Elsevier

Note

peer-reviewed

Language

English

Usage metrics

    University of Limerick

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC