creators_name: Abrial, Jean-Raymond
creators_name: Butler, Michael
creators_name: Hallerstede, Stefan
creators_name: Hoang, Thai Son
creators_name: Mehta, Farhad
creators_name: Voisin, Laurent
creators_id: mjb@ecs.soton.ac.uk
creators_id: sth@ecs.soton.ac.uk
creators_id: htson@inf.ethz.ch
type: monograph
datestamp: 2009-07-02 12:34:50
lastmod: 2010-04-19 15:05:56
metadata_visibility: show
title: Rodin: An Open Toolset for Modelling and Reasoning in Event-B
ispublished: unpub
subjects: theory
subjects: deploy_tooldev
full_text_status: public
monograph_type: technical_report
note: Under review.
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.
date: 2009
publisher: DEPLOY Project
citation:   Abrial, Jean-Raymond and Butler, Michael and Hallerstede, Stefan and Hoang, Thai Son and Mehta, Farhad and Voisin, Laurent  (2009) Rodin: An Open Toolset for Modelling and Reasoning in Event-B.  Technical Report. DEPLOY Project.    (Unpublished)  
document_url: http://deploy-eprints.ecs.soton.ac.uk/130/1/main.pdf