Multi-level Animation Sample Clauses

Multi-level Animation. Prior versions of ProB only supported the animation of a single refinement level. Abstract variables and predicates referring to them were ignored. To support validation of Event-B models such as the ones generated by Bosch, this short coming had to be addressed. In [4] and [5] we extended ProB in a way that all refinement levels of a model can be animated simultaneously. First, this can give the user a deeper insight into how the model behaves and how the refinement levels are related to each other. Second, we can now find errors in context of refinement. This include violation of the gluing invariant or not satisfiable witnesses for abstract variables. If such errors are present in a model, the corresponding proof obligation cannot be discharged. But without an animator it is not always easy to see for an user if this is caused by the complexity of the proof or by an error. In the articles we summarized Event-B's current refinement methodology and showed for each proof obligation how the algorithm would find a counter-example. We presented empirical results and discussed how the algorithm can be combined with symmetry reduction.