Development of a flash-based filestore

Modelling and proof of a Tree-structured File System

By Damchoom, Kriangsak and Butler, Michael and Abrial, Jean-Raymond. in ICFEM 2008

Modelling and proof of a Tree-structured File System

By Damchoom, Kriangsak and Butler, Michael. in SBMF 2009

An Incremental Refinement Approach to a Development of a Flash File System

By Damchoom, Kriangsak and Butler, Michael.

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 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

By Damchoom, Kriangsak and Butler, Michael. Event-B is a formal method used for specifying and reasoning about systems. Rodin is a 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 was chosen as a strategy in our development. Evolution of the models are also necessary when the requirements have changes. In this work, we outline some changes that impact the models, how reusability can be achieved and how flexibility of the language and tool are. We believe our exemplar would be useful for other developers to learn from.