Paper Info
Title
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.
Year
DOI
Venue
2016
10.1007/978-3-319-40648-0_13
NFM
Keywords
Field
DocType
Code generation,Event-B,EventB2Java,Java,JML,Rodin
Android (operating system),Programming language,Software engineering,Computer science,Formal specification,Implementation,Code generation,Software system,B-Method,Reactive system,Executable
Conference
Volume
ISSN
Citations 
9690
0302-9743
4
PageRank 
References 
Authors
0.55
7
2
Name
Order
Citations
PageRank
Néstor Cataño17711.29
Víctor Rivera25212.94