Event-B and the Rodin tool use a number of simple techniques that make the modelling method around them effective in practical applications. We present two of these techniques, anticipation and witnesses. It is interesting how a couple of very simple techniques are so important for the method to work. Finally we propose a small enhancement of Event-B that would extend the use of witnesses.
Main Research Area:
Refinement Based Methods for the Construction of Dependable Systems, 2009