Sciweavers

27
Voted
STTT
2010

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

13 years 8 months ago
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 ent 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 EventB 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.
Jean-Raymond Abrial, Michael J. Butler, Stefan Hal
Added 30 Jan 2011
Updated 30 Jan 2011
Type Journal
Year 2010
Where STTT
Authors Jean-Raymond Abrial, Michael J. Butler, Stefan Hallerstede, Thai Son Hoang, Farhad Mehta, Laurent Voisin
Comments (0)