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)
![[img]](../style/images/fileicons/application_pdf.png)
| PDF - Accepted Version 829Kb |
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.
| Item Type: | Book Section |
|---|---|
| Subjects: | Methodology > Refinement Methodology > Proof and model checking Tool developments > Model checking Tool developments > Rodin plug-ins Event-B > Event-B Theory |
| ID Code: | 186 |
| Deposited By: | Prof Michael Leuschel |
| Deposited On: | 11 Jan 2010 13:51 |
| Last Modified: | 19 Apr 2010 16:05 |
Repository Staff Only: item control page
