Skip to Main content Skip to Navigation
Conference papers

Proving the Fidelity of Simulations of Event-B Models

Faqing Yang 1 Jean-Pierre Jacquot 1 Jeanine Souquières 1 
1 DEDALE - Development of specifications
LORIA - FM - Department of Formal Methods
Abstract : A 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [15 references]  Display  Hide  Download
Contributor : Faqing Yang Connect in order to contact the contributor
Submitted on : Sunday, December 22, 2013 - 7:00:04 AM
Last modification on : Saturday, October 16, 2021 - 11:26:08 AM
Long-term archiving on: : Monday, March 24, 2014 - 9:15:35 AM


Files produced by the author(s)


  • HAL Id : hal-00908066, version 1



Faqing Yang, Jean-Pierre Jacquot, Jeanine Souquières. Proving the Fidelity of Simulations of Event-B Models. The 15th IEEE International Symposium on High Assurance Systems Engineering (HASE), Jan 2014, Miami, United States. ⟨hal-00908066⟩



Record views


Files downloads