Validation of formal models by refinement animation

We provide a detailed description of refinement in Event-B, both as a contribution in itself and as a foundation for the approach to simultaneous animation of multiple levels of refinement that we propose. We present an algorithm for simultaneous multi-level animation of refinement, and show how it can be used to detect a variety of errors that occur frequently when using refinement. The algorithm has been implemented in ProB and we applied it to several case studies, showing that multi-level animation is tractable also on larger models. We present empirical results and discuss how the algorithm can be combined with symmetry reduction.

► Animation and formal proof are complementary validation techniques.
► Applied to systems constructed by refinement combined use can be very beneficial.
► However, for a formal method to incorporate animation and proof common concepts are required.
► In the Event-B formal method such a concept is available in the form of “witnesses”.
► We present some results from case studies and review some existing tools for animation of formal models.