Concurrent models of flash memory device behaviour

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.