"125","Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B","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 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.  ","http://deploy-eprints.ecs.soton.ac.uk/125/","Damchoom, Kriangsak and Butler, Michael","UNSPECIFIED","       <span class=\"person_name\">Damchoom, Kriangsak</span> and <span class=\"person_name\">Butler, Michael</span>       <a href=\"http://deploy-eprints.ecs.soton.ac.uk/125/\"><em>Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B.</em></a>       In: SBMF 2009, 19-21 August 2009, Gramado, Brazil.           ","kd06r@ecs.soton.ac.uk,mjb@ecs.soton.ac.uk",""