EB4EB: A Framework for Reflexive Event-B - Archive ouverte HAL Access content directly
Conference Papers Year :

EB4EB: A Framework for Reflexive Event-B

(1, 2) , (1, 2) , (1, 2)
1
2

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.
Fichier principal
Vignette du fichier
ICECCS_22_camera_ready_final_version.pdf (366.02 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03540955 , version 1 (24-01-2022)

Identifiers

Cite

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⟩
100 View
22 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More