---
abstract: "Event-B is a formal method for system-level modelling and\r\nanalysis.  Key features of Event-B are the use of\r\nset theory as a modelling notation, the use of refinement to\r\nrepresent systems at different abstraction levels and the use of\r\nmathematical proof to verify consistency between refinement\r\nlevels.   In this article we present the Rodin modelling tool that\r\n  seamlessly integrates modelling and proving. \r\nWe outline how the Event-B language was designed to facilitate proof\r\nand how the tool has been designed to support changes to models\r\nwhile minimising the impact of changes on existing proofs.\r\nWe outline the important features of the prover architecture and \r\nexplain how well-definedness is treated.\r\nThe tool is extensible and configurable so that it can\r\n  be adapted more easily to different application domains and\r\n  development methods."
accompaniment: []
book_title: ~
commentary: ~
completion_time: ~
composition_type: ~
conductors_id: []
conductors_name: []
contact_email: ~
copyright_holders: []
corp_creators: []
creators_id:
  - ~
  - mjb@ecs.soton.ac.uk
  - sth@ecs.soton.ac.uk
  - htson@inf.ethz.ch
  - ~
  - ~
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: 2009
date_type: ~
datestamp: 2009-07-02 12:34:50
department: ~
dir: disk0/00/00/01/30
divisions: []
edit_lock_since: ~
edit_lock_until: ~
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 130
event_dates: ~
event_location: ~
event_title: ~
event_type: ~
exhibitors_id: []
exhibitors_name: []
fileinfo: /style/images/fileicons/application_pdf.png;/130/1/main.pdf
full_text_status: public
funders: []
id_number: ~
importid: ~
institution: ~
isbn: ~
ispublished: unpub
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: technical_report
note: Under review.
num_pieces: ~
number: ~
official_url: ~
output_media: ~
pagerange: ~
pages: ~
patent_applicant: ~
pedagogic_type: ~
place_of_pub: ~
pres_type: ~
producers_id: []
producers_name: []
projects: []
publication: ~
publisher: DEPLOY Project
refereed: ~
referencetext: ~
related_url_type: []
related_url_url: []
relation_type: []
relation_uri: []
rev_number: 26
series: ~
skill_areas: []
source: ~
status_changed: 2009-07-02 12:34:50
subjects:
  - theory
  - 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: monograph
userid: 1
volume: ~