In this paper, we address the problem of developing synchronous bus protocols with Event-B. The interest of using Event-B lies in its parameterized nature, as well as its refinement-based modeling methodology and its formal verification semantics. A synchronous, generic model was created to serve as a basis for synchronous bus protocols with a centralized arbiter. Bus protocols and their properties can then be specified as refinements of the generic model: properties are specified and verified with the Event-B proof semantics, their preservation being enforced in the construction of correct refinements. We use the AMBA bus protocol as an application example of our synchronous model, with emphasis in its arbitration phase and the mutual exclusion property.
['Ricardo Bedin França', 'Leandro Buss Becker', 'Jean-Paul Bodeveix', 'Jean-Marie Farines', 'Mamoun Filali']
Towards Safe Design of Synchronous Bus Protocols in Event-B