Proving the Fidelity of Simulations of Event-B Models

International audienceA major hindrance to the use of formal methods is the difficulty to validate the models, particularly at the early stages of the development. We propose to build simulations: programs automatically generated from the specifications but with user-provided implementations of the non-executable traits of the models. We present such a simulation. Of course, the question of the fidelity of the simulation to the model is raised in such a setting. We provide a formal definition of fidelity and the proof obligations that can be attached to each hand-coded element so that fidelity can be proven