Paper Info
Title
Translating event-B to JML-specified Java programs
Abstract
We present a translation from Event-B machines to JML-specified Java class implementations and the EventB2Java Rodin plug-in that automates the translation. Producing JML specifications in addition to Java implementations enables users to write bespoke implementations that can then be checked for correctness using existing JML tools. We have validated the proposed translation by applying the EventB-2Java tool to various programs and systems.
Year
DOI
Venue
2014
10.1145/2554850.2554897
SAC
Keywords
Field
DocType
eventb2java,methodologies,refinement calculus,combined formal methods,jml,tools,rodin,event-b,automated translation
Bespoke,Programming language,Refinement calculus,Computer science,Correctness,Implementation,Java Modeling Language,Java
Conference
Citations 
PageRank 
References 
7
0.57
16
Authors
2
Name
Order
Citations
PageRank
Víctor Rivera15212.94
Nestor Cataño2574.77