Towards Safe Design of Synchronous Bus Protocols in Event-B

Ricardo Bedin FrançaLeandro Buss BeckerJean-Paul BodeveixJean-Marie FarinesMamoun Filali

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.

Caso o link acima esteja inválido, faça uma busca pelo texto completo na Web: Buscar na Web

Biblioteca Digital Brasileira de Computação - Contato:
     Mantida por: