Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

EB4EB: A Framework for Reflexive Event-B

Abstract : Event-B is a correct-by-construction rigorous statebased method offering features for formal modelling and proof automation. An inductive proof schema allows to prove system properties, in particular invariants.In the current setup, verifying other properties such as deadlock-freeness, reachability, event scheduling, liveness, etc., requires adhoc modelling.These properties can be established partially using model checkers or by using third party interactive provers.Other crucial aspects, such as deadlock-freeness, are difficult to express. The availabilty of a meta-modelling mechanism for explicit manipulation of Event-B concepts would allow to deal with higher order modelling concepts and to define generic properties and associated proof obligations. In this paper, we propose EB4EB, an Event-B based modelling framework allowing to manipulate Event-B features explicitly based on meta modelling concepts. This framework relies on a set of Event-B theories defining data-types, operators, welldefined conditions, theorems and proof rules. It preserves the core logical foundation, including semantics, of original Event-B models. Based on the instantiation of the introduced features at meta level, deep and shallow modelling approaches are proposed to exploit this framework. In addition, a case study is developed to demonstrate the use of our framework applying the deep and shallow embedding approaches. The whole framework is supported by the Rodin platform handling Event-B models and proofs. Index Terms-Reflection, refinement and proof, meta-models, model instantiation, new proof obligations, theories, Event-B.
Complete list of metadata

https://hal.archives-ouvertes.fr/hal-03540955
Contributor : Peter Riviere Connect in order to contact the contributor
Submitted on : Monday, January 24, 2022 - 12:50:25 PM
Last modification on : Monday, July 4, 2022 - 9:20:15 AM
Long-term archiving on: : Monday, April 25, 2022 - 7:06:47 PM

File

ICECCS_22_camera_ready_final_v...
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03540955, version 1

Citation

Peter Riviere, Neeraj K. Singh, yamine Aït-Ameur. EB4EB: A Framework for Reflexive Event-B. 2022. ⟨hal-03540955⟩

Share

Metrics

Record views

38

Files downloads

12