EventB2Java: A code generator for Event-B

Abstract

Event-B is a formal specification language and a methodology used to build software systems. Formal specifications are more useful when they can be executed. An executable formal specification provides insight on the behaviour of the system being modelled w.r.t an expected behaviour. This paper presents a tool that generates executable implementations of Event-B models. The tool is implemented as a plug-in of the Rodin platform, an Eclipse IDE that provides a set of tools to work with Event-B models. Our tool has extensively been used for generating code for Event-B models of Android applications, reactive systems, Smart Cards, searching algorithms, among others. The first author regularly uses EventB2Java in teaching to help master students of Software Engineering to get a better grasp of the behaviour of a model in Event-B and to detect inconsistencies in the model.