Sciweavers

SBMF
2009
Springer

Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B

14 years 4 months ago
Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B
Abstract. Event-B is a formal method used for specifying and reasoning about systems. Rodin is a toolset for developing system models in Event-B. Our experiment which is outlined in this paper is aimed at applying Event-B and Rodin to a flash-based filestore. Refinement is a useful mechanism that allows developers to sharpen models step by step. Two uses of refinement, feature augmentation and structural refinement, were employed in our development. Event decomposition and machine decomposition are structural refinement techniques on which we focus in this work. We present an outline of a verified refinement chain for the flash filestore. We also outline evidence of the applicability of the method and tool together with some guidelines. Key words: refinement, event decomposition, machine decomposition, file system, flash memory, proof, Event-B, Rodin
Kriangsak Damchoom, Michael J. Butler
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where SBMF
Authors Kriangsak Damchoom, Michael J. Butler
Comments (0)