Concurrent Models of Flash Memory Device Behaviour - BUTTERFIELD, ANDREW (Springer, 2009)
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.
Lecture Notes in Computer Science - Formal Methods: Foundations and Applications
12th Brazilian Symposium on Formal Methods (SBMF 2009)
PUBLISHED
Gramado, Brazil
Keywords: formal methods; flash memory; concurrency theory; model checking; Smart & Sustainable Planet