Skip to Main content Skip to Navigation
New interface
Conference 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 : Thursday, July 21, 2022 - 3:53:45 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

Citation

Peter Riviere, Neeraj K. Singh, Yamine Aït-Ameur. EB4EB: A Framework for Reflexive Event-B. 2022 26th International Conference on Engineering of Complex Computer Systems (ICECCS), Mar 2022, Hiroshima, Japan. pp. 71-80, ⟨10.1109/ICECCS54210.2022.00017⟩. ⟨hal-03540955⟩

Share

Metrics

Record views

100

Files downloads

22