View source for Development of a flash-based filestore

Nowadays, many formal methods are used in the area of software development accompanied by a number of advanced theories and tools. However, more experiments are still required in order to provide significant evidence that will convince and encourage users to use, and gain more benefits from, those theories and tools. Event-B is a formalism used for specifying and reasoning about systems. Rodin is an open and extensible toolset for Event-B specification, refinement and proof. The flash file system is a complex system that is challenging to specify and verify at this moment in time. This system was chosen as a case study for our experiments, carried out using Event-B and the Rodin tool. The experiments were aimed at developing a rigorous model of flash-based file system, and providing useful evidence and guidelines to developers and the software industry. We believe that these would convince users and make formal methods more accessible. 


===An Incremental Refinement Approach to a Development of a Flash-Based File System in Event-B=== 

The work on the development of a flash-based file system in Event-B is reported in a PhD thesis by Kriangsak Damchoom<ref>[http://eprints.ecs.soton.ac.uk/21655/ Damchoom, K. (2010) An Incremental Refinement Approach to a Development of a Flash-Based File System in Event-B. PhD thesis, University of Southampton.]
</ref>.

Other papers and Rodin achives are available below.

=== Modelling and proof of a Tree-structured File System===
By ''Damchoom, Kriangsak and Butler, Michael and Abrial, Jean-Raymond''.<ref>[http://deploy-eprints.ecs.soton.ac.uk/22/ Damchoom, Kriangsak and Butler, Michael and Abrial, Jean-Raymond (2008) Modelling and proof of a Tree-structured File System. In: ICFEM 2008.]</ref>

We present a verified model of a tree-structured ﬁle system which was carried out using Event-B and the Rodin platform. The model is focused on basic functionalities aﬀecting the tree structure including create, copy, delete and move. This work is aimed at constructing a clear and accurate model with all proof obligations discharged. While constructing the model of a ﬁle system, we begin with an abstract model of a ﬁle system and subsequently reﬁne it by adding more details through reﬁnement steps. We have found that careful formulation of invariants and useful theorems that can be reused for discharging similar proof obligations make models simpler and easier to prove.

=== Applying Event and Machine Decomposition to a Flash-Based Filestore] ===
By ''Damchoom, Kriangsak and Butler, Michael.<ref>[http://deploy-eprints.ecs.soton.ac.uk/125/ Damchoom, Kriangsak and Butler, Michael Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B. In: SBMF 2009, 19-21 August 2009, Gramado, Brazil.]</ref>

=== An Incremental Refinement Approach to a Development of a Flash File System [http://deploy-eprints.ecs.soton.ac.uk/243/  archive] ===
By ''Damchoom, Kriangsak and Butler, Michael''.

An incremental refinement was chosen as a strategy in our development. The refinement
was used for two different purposes: feature augmentation and structural refinement (covering event and
machine decomposition). Several techniques and styles of modelling were investigated and compared; to
produce some useful guidelines for modelling, refinement and proof. The model of the flash-based file system
we have completed covers three main issues: fault-tolerance, concurrency and wear-levelling process. Our
model can deal with concurrent read/write operations and other processes such as block relocation and
block erasure. The model tolerates faults that may occur during reading/writing of files. We believe our
development acts as an exemplar that other developers can learn from.

=== Multi-Levelled Refinement and Evolution of a Flash File System Model in Event-B and Rodin [http://deploy-eprints.ecs.soton.ac.uk/243/ archive ] ===
By ''Damchoom, Kriangsak and Butler, Michael''.

This work is an extension of the work presented above. The focus of this work is to outline an evolution of the model when the requirements change. Evolution of the models is necessary when
the requirements change. The point is how to deal with this. How much changes that impact the models? How reusability
can be achieved? and how flexibility of the language and tool are?

==References==
<references/>