Industrial deployment of system engineering methods providing high dependability and productivity


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

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)

PDF - Accepted Version


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

Deploy-Project - All right reserved