creators_name: Hallerstede, Stefan creators_name: Leuschel, Michael creators_name: Plagge, Daniel creators_id: leuschel@cs.uni-duesseldorf.de creators_id: plagge@cs.uni-duesseldorf.de type: book_section datestamp: 2010-01-11 13:51:00 lastmod: 2010-04-19 15:05:59 metadata_visibility: show title: Refinement-Animation for Event-B - Towards a Method of Validation ispublished: inpress subjects: Refinement subjects: deploy_method_proof subjects: deploy_tooldev_modela subjects: deploy_tooldev_rodinplugins subjects: theory full_text_status: public abstract: 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. series: LNCS publisher: Springer-Verlag refereed: TRUE book_title: Proceedings ABZ 2010 citation: Hallerstede, Stefan and Leuschel, Michael and Plagge, Daniel Refinement-Animation for Event-B - Towards a Method of Validation. In: Proceedings ABZ 2010. LNCS . Springer-Verlag. (In Press) document_url: http://deploy-eprints.ecs.soton.ac.uk/186/1/multi_refine.pdf