---
abstract: "Event-B is a formal method used for specifying and reasoning about\r\nsystems. Rodin is a toolset for developing system models in\r\nEvent-B. Our experiment which is outlined in this paper is aimed\r\nat applying Event-B and Rodin to a flash-based filestore.\r\nRefinement 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\r\noutline evidence of the applicability of the method and tool\r\ntogether with some guidelines.\r\n"
accompaniment: []
book_title: ~
commentary: ~
completion_time: ~
composition_type: ~
conductors_id: []
conductors_name: []
contact_email: ~
copyright_holders: []
corp_creators: []
creators_id:
  - kd06r@ecs.soton.ac.uk
  - mjb@ecs.soton.ac.uk
creators_name:
  - family: Damchoom
    given: Kriangsak
    honourific: ''
    lineage: ''
  - family: Butler
    given: Michael
    honourific: ''
    lineage: ''
data_type: ~
date: ~
date_type: ~
datestamp: 2009-06-20 09:49:55
department: ~
dir: disk0/00/00/01/25
divisions: []
edit_lock_since: ~
edit_lock_until: ~
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 125
event_dates: 19-21 August 2009
event_location: 'Gramado, Brazil'
event_title: SBMF 2009
event_type: workshop
exhibitors_id: []
exhibitors_name: []
fileinfo: /style/images/fileicons/application_zip.png;/125/1/FlashFileSysPrj.zip|/style/images/fileicons/application_pdf.png;/125/3/FileSysSBMF2009.pdf
full_text_status: public
funders: []
id_number: ~
importid: ~
institution: University of Southampton
isbn: ~
ispublished: pub
issn: ~
item_issues_comment: []
item_issues_count: 0
item_issues_description: []
item_issues_id: []
item_issues_reported_by: []
item_issues_resolved_by: []
item_issues_status: []
item_issues_timestamp: []
item_issues_type: []
keywords: ~
lastmod: 2010-04-19 15:05:56
latitude: ~
learning_level: ~
longitude: ~
lyricists_id: []
lyricists_name: []
metadata_visibility: show
monograph_type: ~
note: ~
num_pieces: ~
number: ~
official_url: ~
output_media: ~
pagerange: ~
pages: ~
patent_applicant: ~
pedagogic_type: ~
place_of_pub: ~
pres_type: paper
producers_id: []
producers_name: []
projects: []
publication: ~
publisher: ~
refereed: TRUE
referencetext: ~
related_url_type: []
related_url_url: []
relation_type: []
relation_uri: []
rev_number: 29
series: ~
skill_areas: []
source: ~
status_changed: 2009-06-20 09:49:55
subjects:
  - Refinement
  - Event-Bsemantics
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B
type: conference_item
userid: 19
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>