Concurrent Models of Flash Memory Device Behaviour
Citation:
Andrew Butterfield, Art O Cathain, Concurrent Models of Flash Memory Device Behaviour, Lecture Notes in Computer Science - Formal Methods: Foundations and Applications, 12th Brazilian Symposium on Formal Methods (SBMF 2009), Gramado, Brazil, 19-21 August, Jim Woodcock, Marcel Oliveira, 5902, Springer, 2009, 70-83Download Item:
Abstract:
We present a CSP model of the internal behaviour of Flash Memory, based on its specification by the Open Nand-Flash Interface (ONFi) consortium. This contributes directly to the low-level modelling of the data-storage technology that is the target of the POSIX filestore mini-challenge. The key objective was to ensure that the internal behaviour was well-specified, and that it was consistent with the specification of the external interface of such devices. The FDR toolkit was used to perform the revelent refinement/model-checking. In addition to uncovering errors and possible sources of misinterpretation in the ONFi standard, this work also describes a methodology for model data-entry based on a ?state-chart? dialect of XML (SCXML) using XSLT to translate into CSP, and HTML, to support validation.
Sponsor
Grant Number
Science Foundation Ireland (SFI)
Author's Homepage:
http://people.tcd.ie/butrfeldDescription:
PUBLISHEDGramado, Brazil
Author: BUTTERFIELD, ANDREW
Other Titles:
Lecture Notes in Computer Science - Formal Methods: Foundations and Applications12th Brazilian Symposium on Formal Methods (SBMF 2009)
Publisher:
SpringerType of material:
Conference PaperCollections
Series/Report no:
5902Availability:
Full text availableKeywords:
formal methods, flash memory, concurrency theory, model checkingSubject (TCD):
Smart & Sustainable PlanetMetadata
Show full item recordLicences: