University of Limerick Institutional Repository

Modelling flash devices with FDR: progress and limits

DSpace Repository

Show simple item record Beg, Arshad Butterfield, Andrew 2011-02-02T20:53:05Z 2011-02-02T20:53:05Z 2010
dc.description peer-reviewed en_US
dc.description.abstract We present our experience of working with the Failures-Divergence Refinement (FDR) toolkit while extending our modelling of the behaviour of Flash Memory. This effort is a step towards the low-level modelling of data-storage technology that is the target of the POSIX filestore minichallenge. The key objective was to advance previous work presented in [4,2] to cover the full Open Nand-Flash Interface (ONFi) 2.1 model. The previous work covered a sub-model of the mandatory features of ONFi 1.0. The FDR toolkit was used for refinement/ model-checking. In addition to the compression techniques available in FDR, we also experimented with FDR Explorer - an application programming interface (API) that allowed us to get a better picture of FDR performance. This paper summarises the progress we made, and the limits we encountered. We are now able to verify many of the operations in ONFi 2.1 model using full Failures-Divergence refinement checking, rather than just trace refinement. Through the use of compression techniques available in the FDR toolkit and in particular by hiding the events deeper in the model, we were able to get compression of the state-space. The work also reports the number of attempts to compile the full ONFi 2.1 model. en_US
dc.language.iso eng en_US
dc.relation.ispartofseries FIT'10: International Conference on Frontiers of Information Technology Proceedings;
dc.subject failures-divergence refinement en_US
dc.title Modelling flash devices with FDR: progress and limits en_US
dc.type Conference item en_US
dc.type.supercollection all_ul_research en_US
dc.type.supercollection ul_published_reviewed en_US
dc.type.restriction none en
dc.contributor.sponsor SFI
dc.contributor.sponsor PARTLI4
dc.contributor.sponsor HEA

Files in this item

This item appears in the following Collection(s)

Show simple item record

Search ULIR


My Account