Reflexive Event-B: Semantics and Correctness The EB4EB framework

15 pagesThe Event-B method enables correct by construction modelling 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 to Event-B. While Event-B has proven its efficiency for the proof of this type of properties, it does not offer powerful means allowing the explicit description of properties other than safety and specific forms of reachability. Checking other properties like deadlock-freeness, liveness or event scheduling, etc. requires ad hoc modelling techniques and external tools such as model checkers or other proof systems. This paper presents EB4EB, a new modelling framework offering the capability to introduce formally defined Event-B extensions, in particular new proof obligations corresponding to new properties. It is based on meta-modelling techniques. It includes a theory (a meta-theory) modelling Event-B and offers means for explicit manipulation of Event-B features and an extension mechanism to explicitly formalise 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 meta-theory. 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