title: Refinement-Animation for Event-B - Towards a Method of Validation
creator: Hallerstede, Stefan
creator: Leuschel, Michael
creator: Plagge, Daniel
subject: Refinement
subject: Proof and model checking
subject: Model checking
subject: Rodin plug-ins
subject: Event-B Theory
description: 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.
publisher: Springer-Verlag
type: Book Section
type: PeerReviewed
format: application/pdf
identifier: http://deploy-eprints.ecs.soton.ac.uk/186/1/multi_refine.pdf
identifier:   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)  
relation: http://deploy-eprints.ecs.soton.ac.uk/186/

<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>