Ricardo Bedin França,  Jean-Meire Farines,  J-P. Bodeveix,  Leandro Buss Becker,  Mamoun Filali Amine. 

In a real-time system architecture, the notion of a bus component plays an important role as it forms the backbone of communication among all the devices of the system. For this purpose, we need a precise specification of buses for applications that will run on top of them and for developers who implement device protocols. In this paper, we propose an incremental methodology to elaborate detailed bus protocol descriptions that may be useful in both design and temporal property verification, by specifying a protocol from a simple representation to a complete one by means of successive refinements, thus also permitting the refinement of model properties. The methodology is then tested with AADL and TLA specifications of the PCI bus protocol.

http://www.lbd.dcc.ufmg.br/colecoes/wtr/2007/006.pdf

Processando consulta.