From Event-B to Verified C via HLL

TL;DR

This paper presents a formal method for translating Event-B models to C code through an intermediate HLL language, ensuring correctness via formal proofs at each step.

Contribution

It introduces a systematic approach for correct translation from Event-B to C using HLL, including proof of invariants and properties, with automated code generation and verification.

Findings

Successful translation of Event-B models to C with correctness guarantees

Formal proof of invariants and properties at the HLL level

Automated and manual code generation with equivalence verification

Abstract

This work addresses the correct translation of an Event-B model to C code via an intermediate formal language, HLL. The proof of correctness follows two main steps. First, the final refinement of the Event-B model, including invariants, is translated to HLL. At that point, additional properties (e.g., deadlock-freeness, liveness properties, etc.) are added to the HLL model. The proof of the invariants and additional properties at the HLL level guarantees the correctness of the translation. Second, the C code is automatically generated from the HLL model for most of the system functions and manually for the remaining ones; in this case, the HLL model provides formal contracts to the software developer. An equivalence proof between the C code and the HLL model guarantees the correctness of the code.