Show simple item record

dc.contributor.authorBUTTERFIELD, ANDREW
dc.date.accessioned2010-02-25T14:12:52Z
dc.date.available2010-02-25T14:12:52Z
dc.date.issued2009
dc.date.submitted2009en
dc.identifier.citationAndrew Butterfield, Leo Freitas, Jim Woodcock, Mechanising a Formal Model of Flash Memory, Science of Computer Programming, 74, 4, 2009, 219-237en
dc.identifier.otherY
dc.identifier.urihttp://hdl.handle.net/2262/38366
dc.descriptionPUBLISHEDen
dc.description.abstractWe 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
dc.format.extent219-237en
dc.format.extent229725 bytes
dc.format.mimetypeapplication/pdf
dc.language.isoenen
dc.publisherElsevieren
dc.relation.ispartofseriesScience of Computer Programmingen
dc.relation.ispartofseries74en
dc.relation.ispartofseries4en
dc.rightsYen
dc.subjectComputer hardware and architectureen
dc.subjectNAND flash memoryen
dc.titleMechanising a Formal Model of Flash Memoryen
dc.typeJournal Articleen
dc.type.supercollectionscholarly_publicationsen
dc.type.supercollectionrefereed_publicationsen
dc.identifier.peoplefinderurlhttp://people.tcd.ie/butrfeld
dc.identifier.rssinternalid49618
dc.identifier.rssurihttp://dx.doi.org/10.1016/j.scico.2008.09.014en


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record