The Case for Using Simulation to Validate Event-B Specifications

This paper addresses the validation of formal specifications in Event-B through the execution of the specification. Current tools for Event-B, animators and translators, can execute only a restricted set of specifications. So, we propose a third technique, simulation, in which users and tools co-operate to produce an executable instance of the model. After a short presentation of Event-B and our simulation framework, JeB, we show how to use it on two reasonably complex specifications. Observations and analysis from the point of view of validation are presented and discussed.