EB4EB: A Framework for Reflexive Event-B

Event-B is a correct-by-construction rigorous state-based 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 prop-erties 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, well-defined 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.