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. © 2009 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Butterfield, A., & Ó Catháin, A. (2009). Concurrent models of flash memory device behaviour. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5902 LNCS, pp. 70–83). https://doi.org/10.1007/978-3-642-10452-7_6
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
