Industrial deployment of system engineering methods providing high dependability and productivity

 

Rodin: An Open Toolset for Modelling and Reasoning in Event-B

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)

[img]
Preview
PDF
609Kb

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.

Item Type:Monograph (Technical Report)
Additional Information:Under review.
Subjects:Event-B > Event-B Theory
Tool developments
ID Code:130
Deposited By:Michael Butler
Deposited On:02 Jul 2009 13:34
Last Modified:19 Apr 2010 16:05

Repository Staff Only: item control page

Deploy-Project - All right reserved