1.2.2 Rodin: An Open Toolset for Modelling and Reasoning in Event-B (2009)

This article discusses the design principles of the Rodin platform and the Event-B language and explains the motivation behind it.

The abstract states: “[…] 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 authors J.-R. Abrial, M. Butler, S. Hallerstede, T. S. Hoang, F. Mehta and L. Voisin have published the article in the journal Software Tools and Technology Transfer (STTT).