Abstract : The validation of formal models is a challenge for formal methods. We propose JeB, a framework which generates and executes simulations of Event-B models, even highly nondeterministic ones. JeB allows users to safely insert pieces of code to supply deterministic computations where the automatic translation fails. We present how JeB translates Event-B model into JavaScript. We define Fidelity as the formal notion which captures the idea of the correctness of a simulation. We define it through proof-obligations.
https://hal.inria.fr/hal-00908056 Contributor : Faqing YangConnect in order to contact the contributor Submitted on : Saturday, December 7, 2013 - 7:00:03 AM Last modification on : Saturday, October 16, 2021 - 11:26:08 AM Long-term archiving on: : Saturday, April 8, 2017 - 2:17:12 AM