A Simulation Framework for the Validation of Event-B Specifications
type: Dataset
description: This thesis aims at the specification, verification and validation of safety-critical systems with formal methods, in particular, with Event-B. We assessed the usability of Event-B by the development of platooning control algorithms, specially how it scaled up from a simplified 1D version to a more realistic 2D version. The critical analysis of the 1D platooning model uncovered some anomalous behaviors. The difficulty of expressing the deadlock-freeness theorems in Event-B motivated us to develop a tool, the generator of deadlock-freeness theorems, to automatically construct these theorems. Our assessment confirmed that the mathematical proofs are not sufficient to assure the correctness of a formal specification: a formal specification should also be validated. We believe that the validation activities, like the verification activities, should be associated with each refinement during the development. To do that, we need better validation tools. The state-of-the-art tools which can execute Event-B models failed in highly non-deterministic models. Therefore we designed and implemented a new execution tool, JeB, which is a JavaScript simulation framework for Event-B. JeB allows users to safely insert hand-coded pieces of code to supply deterministic computations where the automatic translation fails. To achieve this goal, we have defined a set of proof-obligations which, when discharged, guarantee the correctness of the simulations with respect to the model.
identifier: NNT: 2013LORR0158
issued: 2026-05-06T05:58:03.637198
language: en
modified: 2026-05-06T05:58:03.637203
contact point: Organization
  fn: CCSD
keyword: b-evenementiel
keyword: event-b
keyword: formal-methods
keyword: infoeu-reposemanticsdoctoralthesis
keyword: infoinfo-flcomputer-science-csformal-languages-and-automata-theory-csfl
keyword: infoinfo-mocomputer-science-csmodeling-and-simulation
keyword: javascript
keyword: methodes-formelles
keyword: simulation
keyword: specification
keyword: theses
keyword: validation
keyword: verification
landing page: https://theses.hal.science/tel-01750224

A Simulation Framework for the Validation of Event-B Specifications
type: Distribution
format: HTML
issued: 2026-05-06T05:58:03.641695
modified: 2026-05-06T05:58:03.619364
access URL: https://theses.hal.science/tel-01750224

test_moissonnage_selune
type: Agent