
TL;DR
This paper introduces EventB2Java, a tool that translates Event-B models into JML-annotated Java code, enabling seamless integration of formal modeling and implementation for system development.
Contribution
It presents a set of syntactic translation rules and an implementation tool that bridges Event-B and Java/JML, facilitating combined use of stepwise refinement and Design-by-Contract.
Findings
Successfully translated multiple Event-B models to JML-annotated Java code.
Enabled development of two software applications using the tool.
Compared EventB2Java with other Event-B code generation tools, demonstrating its effectiveness.
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. This thesis aims to answer, is it possible to combine both approaches in the development of systems, providing the user with the benefits of both? We answer this question by translating the stepwise refinement method with Event-B 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 the tool to translate several Event-B models. It generated JML-annotated Java code for all the considered models that serve as initial implementation. We…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsModel-Driven Software Engineering Techniques · Software Testing and Debugging Techniques · Advanced Software Engineering Methodologies
