---
abstract: 'The Event-B method is a formal approach to modelling systems, using refinement. Initial specification is done at a high level of abstraction; detail is added in refinement steps as the development proceeds toward implementation. In previous work we developed an approach to bridge the gap between abstract specifications and implementations using an implementation level specification notation. In this paper we present details of the tool support for our notation and some of our experiences using the tool.'
accompaniment: []
book_title: ~
commentary: ~
completion_time: ~
composition_type: ~
conductors_id: []
conductors_name: []
contact_email: ~
copyright_holders: []
corp_creators: []
creators_id: []
creators_name:
  - family: Edmunds
    given: Andrew
    honourific: ''
    lineage: ''
  - family: Butler
    given: Michael
    honourific: ''
    lineage: ''
data_type: ~
date: 2010-02
date_type: ~
datestamp: 2010-02-01 09:32:10
department: ~
dir: disk0/00/00/01/97
divisions: []
edit_lock_since: ~
edit_lock_until: ~
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 197
event_dates: ~
event_location: ~
event_title: WS-TBFM2010
event_type: workshop
exhibitors_id: []
exhibitors_name: []
fileinfo: /style/images/fileicons/application_pdf.png;/197/1/wstbfm2010_submission_13.pdf
full_text_status: public
funders: []
id_number: ~
importid: ~
institution: ~
isbn: ~
ispublished: inpress
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: 'Event-B Tools, Code Generation, Concurrency'
lastmod: 2010-04-19 15:06:00
latitude: ~
learning_level: ~
longitude: ~
lyricists_id: []
lyricists_name: []
metadata_visibility: show
monograph_type: ~
note: ~
num_pieces: ~
number: ~
official_url: http://eprints.ecs.soton.ac.uk/18434/
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: 28
series: ~
skill_areas: []
source: ~
status_changed: 2010-02-01 09:32:10
subjects:
  - Code_generation
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: Tool Support for Event-B Code Generation
type: conference_item
userid: 187
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>