Code Generation for Event-B

http://arxiv.org/pdf/1602.02004.pdf

Universidade da Madeira Centro de Ciencias Exactas e da Engenharia 

PhD THESIS presented in fulfilment of the requirement for the degree of Doctor of Philosophy 

Major: Software Engineering 

Code Generation for Event-B 

presented by V´ICTOR ALFONSO RIVERA ZU´ NIGA ˜ 

supervised by NESTOR CATA ´ NO COLLAZOS ˜ June 2014 

Abstract Stepwise refinement and Design-by-Contract are two formal approaches for modelling systems. These approaches are widely used in the development of systems. Both approaches have (dis-)advantages: in stepwise refinement a model starts with an abstraction of the system and more details are added through refinements. Each refinement must be provably consistent with the previous one. Hence, reasoning about abstract models is possible. A high level of expertise is necessary in mathematics to have a good command of the underlying languages, techniques and tools, making this approach less popular. Design-by-Contract, on the other hand, works on the program rather than the program model, so developers in the software industry are more likely to have expertise in it. However, the benefit of reasoning over more abstract models is lost. A question arises: is it possible to combine both approaches in the development of systems, providing the user with the benefits of both? This thesis answers this question by translating the stepwise refinement method with EventB to Design-by-Contract with Java and JML, so users can take full advantage of both formal approaches without losing their benefits. This thesis presents a set of syntactic rules that translates Event-B to JML-annotated Java code. It also presents the implementation of the syntactic rules as the EventB2Java tool. We used EventB2Java to translate several Event-B models. The tool generated JML-annotated Java code for all the considered Event-B models that serve as final implementation. We also used EventB2Java for the development of two software applications. Additionally, we compared EventB2Java against two other tools that also generate Java code from Event-B models. EventB2- Java enables users to start the software development process in Event-B, where users can model the system and prove its consistency, to then transition to JML-annotated Java code, where users can continue the development process. Key Words— Modelling system by stepwise refinement, Event-B, Designby-Contract, Java, JML, EventB2Java