University of Limerick Institutional Repository

Mechanising a formal model of flash memory

DSpace Repository

Show simple item record Butterfield, Andrew Freitas, Leo Woodcock, Jim 2010-12-20T12:23:59Z 2010-12-20T12:23:59Z 2007
dc.identifier.citation Andrew Butterfield, Leo Freitas, Jim Woodcock, Mechanising a Formal Model of Flash Memory, Science of Computer Programming, 74, 4, 2009, 219-237 en_US
dc.description peer-reviewed en_US
dc.description.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. en_US
dc.language.iso eng en_US
dc.publisher Elsevier en_US
dc.relation.ispartofseries Science of Computer Programming;74/ 4/ 219-237
dc.subject grand challenge en_US
dc.subject theorem proving en_US
dc.subject verifcation en_US
dc.subject theorem proving en_US
dc.title Mechanising a formal model of flash memory en_US
dc.type Article en_US
dc.type.supercollection all_ul_research en_US
dc.type.supercollection ul_published_reviewed en_US
dc.type.restriction none en
dc.type.restriction none en

Files in this item

This item appears in the following Collection(s)

Show simple item record

Search ULIR


My Account