A Machine-Checked Proof for a Translation of Event-B Machines to JML

TL;DR

This paper provides a formal, machine-checked proof that translating Event-B models into JML specifications preserves their semantics, ensuring the correctness of the translation process within a formal framework.

Contribution

It introduces a formal, verified translation from Event-B to JML, validated through a machine-checked proof using the Rodin platform, enhancing trustworthiness of model translation.

Findings

The translation preserves semantics between Event-B and JML.

The proof is formalized and verified within the Event-B framework.

The approach covers invariants and initialising events, but not full machines or contexts.

Abstract

We present a machine-checked soundness proof of a translation of Event-B to the Java Modeling Language (JML). The translation is based on an operator EventB2Jml that maps Evnet-B events to JML method specifications, and deterministic and non-deterministic assignments to JML method post-conditions. This translation has previously been implemented as the EventB2Jml tool. We adopted a taking our own medicine approach in the formalisation of our proof so that Event-B as well as JML are formalised in Event-B and the proof is discharged with the Rodin platform. Hence, for any Event-B substitution (whether an event or an assignment) and for the JML method specification obtained by applying EventB2Jml to the substitution, we prove that the semantics of the JML method specification is simulated by the semantics of the substitution. Therefore, the JML specification obtained as translation from the Event-B substitution is a refinement of the substitution. Our proof includes invariants and the standard Event-B initialising event, but it does not include full machines or Event-B contexts. We assume that the semantics of JML and Event-B operate both on the same initial and final states, and we justify our assumption.