Loading...
Date
2009
Abstract
We present a CSP model of the internal behaviour of Flash Memory, based on its speci cation 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 lestore mini-challenge. The key objective was to ensure that the internal behaviour was well-speci ed, and that it was consistent with the specification of the external interface of such devices. The FDR toolkit was used to perform the relevant 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.
Supervisor
Description
peer-reviewed
Publisher
Springer
Citation
Lecture Notes in Computer Science; 5902/2009/ pp.70-83
Files
Keywords
ULRR Identifiers
Funding code
Funding Information
Science Foundation Ireland (SFI)