Formalising Flash Memory: First Steps

	This Article
	Subscribers, please Login Purchase article: $19 PDF IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Andrew Butterfield Articles by Jim Woodcock

12th IEEE International Conference on Engineering Complex Computer Systems (ICECCS 2007)

Auckland, New Zealand

July 11-July 14

ISBN: 0-7695-2895-3

	ASCII Text	x
	Andrew Butterfield, Jim Woodcock, "Formalising Flash Memory: First Steps," Engineering of Complex Computer Systems, IEEE International Conference on, pp. 251-260, 12th IEEE International Conference on Engineering Complex Computer Systems (ICECCS 2007), 2007.

	BibTex	x
	@article{ 10.1109/ICECCS.2007.23, author = {Andrew Butterfield and Jim Woodcock}, title = {Formalising Flash Memory: First Steps}, journal ={Engineering of Complex Computer Systems, IEEE International Conference on}, volume = {0}, year = {2007}, isbn = {0-7695-2895-3}, pages = {251-260}, doi = {http://doi.ieeecomputersociety.org/10.1109/ICECCS.2007.23}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Engineering of Complex Computer Systems, IEEE International Conference on TI - Formalising Flash Memory: First Steps SN - 0-7695-2895-3 SP251 EP260 A1 - Andrew Butterfield, A1 - Jim Woodcock, PY - 2007 KW - null VL - 0 JA - Engineering of Complex Computer Systems, IEEE International Conference on ER -

Andrew Butterfield, Trinity College Dublin, Ireland

Jim Woodcock, University of York, UK

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ICECCS.2007.23

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.

Citation:

Andrew Butterfield, Jim Woodcock, "Formalising Flash Memory: First Steps," iceccs, pp.251-260, 12th IEEE International Conference on Engineering Complex Computer Systems (ICECCS 2007), 2007

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.