Rodin: an open toolset for modelling and reasoning in Event-B

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....

Full description

Saved in:
Bibliographic Details
Published in:International journal on software tools for technology transfer 2010-11, Vol.12 (6), p.447-466
Main Authors: Abrial, Jean-Raymond, Butler, Michael, Hallerstede, Stefan, Hoang, Thai Son, Mehta, Farhad, Voisin, Laurent
Format: Article
Language:English
Subjects:
Applied sciences
Computer programs
Computer Science
Computer science
control theory
systems
Computer simulation
Consistency
Exact sciences and technology
Formal method
Logic and foundations
Mathematical analysis
Mathematical logic, foundations, set theory
Mathematical models
Mathematics
Modelling
Programming languages
Proof theory and constructive mathematics
Proving
Sciences and techniques of general use
Software
Software Engineering
Software Engineering/Programming and Operating Systems
Technology transfer
Theory of Computation
Vstte 2008
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1433-2779
1433-2787
DOI:10.1007/s10009-010-0145-y