---
abstract: 'Event-B is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. In this article we present the Rodin modelling tool that seamlessly integrates modelling and proving. We outline how the Event-B language was designed to facilitate proof and how the tool has been designed to support changes to models while minimising the impact of changes on existing proofs. We outline the important features of the prover architecture and explain how well-definedness is treated. The tool is extensible and configurable so that it can be adapted more easily to different application domains and development methods. '
accompaniment: []
book_title: ~
commentary: ~
completion_time: ~
composition_type: ~
conductors_id: []
conductors_name: []
contact_email: ~
copyright_holders: []
corp_creators: []
creators_id: []
creators_name:
  - family: Abrial
    given: Jean-Raymond
    honourific: ''
    lineage: ''
  - family: Butler
    given: Michael
    honourific: ''
    lineage: ''
  - family: Hallerstede
    given: Stefan
    honourific: ''
    lineage: ''
  - family: Hoang
    given: Thai Son
    honourific: ''
    lineage: ''
  - family: Mehta
    given: Farhad
    honourific: ''
    lineage: ''
  - family: Voisin
    given: Laurent
    honourific: ''
    lineage: ''
data_type: ~
date: 2010-04
date_type: ~
datestamp: 2010-12-22 15:10:08
department: ~
dir: disk0/00/00/02/67
divisions: []
edit_lock_since: ~
edit_lock_until: 0
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 267
event_dates: ~
event_location: ~
event_title: ~
event_type: ~
exhibitors_id: []
exhibitors_name: []
fileinfo: ''
full_text_status: none
funders: []
id_number: ~
importid: ~
institution: ~
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-12-22 15:10:08
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/21058/
output_media: ~
pagerange: ~
pages: ~
patent_applicant: ~
pedagogic_type: ~
place_of_pub: ~
pres_type: ~
producers_id: []
producers_name: []
projects: []
publication: International Journal on Software Tools for Technology Transfer (STTT)
publisher: Springer
refereed: TRUE
referencetext: ~
related_url_type: []
related_url_url: []
relation_type: []
relation_uri: []
rev_number: 8
series: ~
skill_areas: []
source: ~
status_changed: 2010-12-22 15:10:08
subjects:
  - Event-Bsemantics
  - deploy_tooldev
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: 'Rodin: An Open Toolset for Modelling and Reasoning in Event-B'
type: article
userid: 1
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>