Code generation for Event-B

Event-B is a modelling language and a formal methods approach for correct construction of software. This paper presents our work on code generation for Event-B, including the definition of a syntactic translation from Event-B to JML-annotated Java programs, the implementation of the translation as the EventB2Java tool, and two case studies on the use of EventB2Java. The first case study is on implementing an Android application with the aid of the EventB2Java tool, and the second on testing an Event-B specification of the Tokeneer security-critical system. Additionally, we have benchmarked our EventB2Java tool against two other Java code generators for Event-B.