creators_name: Damchoom, Kriangsak
creators_name: Butler, Michael
creators_id: kd06r@ecs.soton.ac.uk
creators_id: mjb@ecs.soton.ac.uk
type: conference_item
datestamp: 2009-06-20 09:49:55
lastmod: 2010-04-19 15:05:56
metadata_visibility: show
title: Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B
ispublished: pub
subjects: Refinement
subjects: Event-Bsemantics
full_text_status: public
pres_type: paper
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 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.

event_title: SBMF 2009
event_location: Gramado, Brazil
event_dates: 19-21 August 2009
event_type: workshop
institution: University of Southampton
refereed: TRUE
citation:   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.     
document_url: http://deploy-eprints.ecs.soton.ac.uk/125/1/FlashFileSysPrj.zip
document_url: http://deploy-eprints.ecs.soton.ac.uk/125/3/FileSysSBMF2009.pdf