An Event-B framework for the validation of Event-B refinement plugins
This work addresses validation challenges for Event-B plugin developers, but it appears incremental as it builds on existing Event-B refinement concepts.
The authors tackled the problem of validating Event-B refinement plugins by proposing an Event-B framework that models the theoretical foundations of Event-B, enabling reuse of the refinement development process for Event-B itself.
We propose an Event-B framework for modeling the underlying theoretical foundations of Event-B. The aim of this framework is to reuse, for Event-B itself, the refinement development process. This framework introduces first, a functional kernel through an Event-B context, then, it defines Event-B projects, their static and dynamic semantics through Event-B machines. We intend to use this framework for the validation of Event-B plugins related to distribution and for Event-B extensions related to composition and decomposition.