Refinement-Animation for Event-B - Towards a Method of Validation

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.

• Type: Conference
• Year: 2010
• Where: ASM
• Authors: Stefan Hallerstede, Michael Leuschel, Daniel Plagge
• Keywords: ASM 2010, Computational Biology, Multiple Levels, Simultaneous Animation, Simultaneous Multi-level Animation