EB4EB, standing for Event-B for Event-B , is a framework that supports the formalisation of Event-B models using first-order logic and set-theory, so that it becomes possible to manipulate them as first-class objects. This framework relies on an Event-B algebraic theory, which serves as a meta-theory formalising, explicitly, all of the features of an Event-B machine. States, events, invariants, variants, etc... are formalised through data-types and operators. When this meta-theory is instantiated, an Event-B model becomes a first-order logic and set-theoretic formula, described in an Event-B context. Because it can handle machine elements as terms in formulas, the EB4EB framework enables the definition of new specific proof obligations and analyses . Such analyses may then be applied to any EB4EB machines in order to establish advanced properties, not natively present in the Event-B method, such as deadlock-freeness or liveness requirements. These analyses are non-intrusive since they do not require to alter the machine in order to be performed. In the previous formalisation of the EB4EB framework only states and events were handled, limiting the expressive reasoning power of the framework. This paper presents an extension of the EB4EB framework to support parameterised events, an important feature of Event-B. This extension is not straightforward in EB4EB. Indeed, the typing system supported by Event-B theories is not rich enough to describe such extension in a constructive manner as for the other Event-B features formalised in EB4EB. The proposed solution, described in this paper, consists in defining an axiomatic formalisation of event parameters definitions. We also show that the proof obligations and model analyses we have defined scale to handle event parameters. The approach is illustrated on different case studies we have developed.

The Event-B method enables correct by construction modeling of systems. It relies on set theory and first-order logic, to describe a series of refined system models expressed as a set of events modifying state variables. Invariants and theorems are introduced to express system properties submitted to the proof system associated with Event-B. While Event-B has proven its efficiency for the proof of this type of property, it does not offer powerful means allowing the explicit description of properties other than safety and specific forms of reachability. Checking other properties such as deadlock-freeness, liveness, or event scheduling requires ad hoc modeling techniques and external tools such as model checkers or other proof systems. This article presentsEB4EB, a new modeling framework offering the capability to introduce formally defined Event-B extensions, in particular new proof obligations corresponding to new properties. It is based on metamodeling techniques. It includes a theory (a metatheory) modeling Event-B and offers means for explicit manipulation of Event-B features and an extension mechanism to explicitly formalize and prove other properties. This reflexive framework relies on a trace-based semantics of Event-B and introduces a set of Event-B theories defining data types, operators, well-defined conditions, theorems, and proof rules to define Event-B constructs and their semantics. Deep and shallow instantiation mechanisms are set up to instantiate the obtained metatheory. The EB4EB framework and its instantiation mechanisms are developed in Event-B using the Rodin platform ensuring correctness and internal consistency of the defined theories. Lamport's clock example, instantiating EB4EB in both shallow and deep mechanisms, is used to evaluate the proposed approach.

System engineering advocates a thorough under-standing of the engineering domain or certification standards (aeronautics, railway, medical, etc.) associated to the system under design. In this context, engineering domain knowledge plays a predominant role in system design and/or certification. Furthermore, it is a prerequisite to achieve the effectiveness and performance of the designed system. This article proposes a formal method for describing and setting up domain-specific behavioural analyses. It defines a formal verification technique for dynamic properties entailed by engineering domain knowledge where Event-B formal models are annotated and analysed in a non-intrusive way, i.e. without destructive alteration. This method is based on the formalisation of behavioural properties analyses relying on domain knowledge as an ontology on the one hand and a meta-theory for Event-B on the other hand. The proposed method is illustrated using a critical interactive system.

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.