University of Limerick Institutional Repository

Mechanising a formal model of flash memory

DSpace Repository

Show simple item record

dc.contributor.author Butterfield, Andrew
dc.contributor.author Freitas, Leo
dc.contributor.author Woodcock, Jim
dc.date.accessioned 2010-12-20T12:23:59Z
dc.date.available 2010-12-20T12:23:59Z
dc.date.issued 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.identifier.uri http://hdl.handle.net/10344/614
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 DSpace


Browse

My Account

Statistics