Flash Memory Modelling

This page describes the Flash Memory modelling work done at TCD as part of the POSIX filestore mini-challenge.

Work so far

• Original Z model of flash device at top-level (with Jim Woodcock).
• Z-model reworked using Z-Eves (with Leo Freitas and Jim Woodcock).
• CSP model of internal behaviour of flash devices (ONFi 1.0)
  M.Sc Dissertation by Art O'Cathain .
  Published at SBMF 2009.
  The following material is available under the following BSD-like license:
  • SCXML Sources (.ZIP archive)
  • XSLT Sources (.ZIP archive)
  • CSP Sources (.ZIP archive)
  • HTML pages generated from SCXML via XSLT
• CSP model of internal behaviour of flash devices (ONFi 2.1) with Arshad Beg.
  The following material is available under the following BSD-like license:
  • SCXML Sources (.ZIP archive)
  • XSLT Sources (.ZIP archive)
  • CSP Sources (.ZIP archive)
  • HTML pages generated from SCXML via XSLT

Work in progress

• Continuing reworking/analysis with Z-Eves (with Leo Freitas and Jim Woodcock).
• Circus models encompassing both the above Z and CSP models (on hold)

This page was last udpated on September 6th 2010 by Andrew Butterfield.