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
