I am working to enhance the Event-B methods with the possibility to describe new Proof Obligations parameterize by Domain Theories.

I develop a Reflexive framework of Event-B using the Theory Plug-in, see more details here.

The models are presented below :

EB4EB Framework

The Event B Theory that encode the machine concept as a Data types theory.

The meta theory that represented all the proof obligations and the operator that invoke POs

Some proof rules have been developed to help the automatization side

Peano axiom of Abrial and new operator

Traces semantics of Event-B express in EB4EB

Correctness of Invariant Proof Obligations

Multiple extension of Event-B have formalized in EB4EB:

Definition