Design and modeling of a protocol to enforce consistency among replicated masters in FTT-CAN

• Tipo: Artigo em Livro de Atas de Conferência Internacional
• Data: 2004

Autores

Rodriguez Navas, G (Autor) Outra; Rigo, J (Autor) Outra; Proenza, J (Autor) Outra; Ferreira, J (Autor) Outra; Luis Almeida (Autor) Outra; Fonseca, JA (Autor) Outra

Ata de Conferência Internacional

Título: IEEE International Workshop on Factory Communication Systems - Proceedings, WFCS

Páginas: 229-238

Indexação

Scopus - 6 Citações

Outras Informações

ID Authenticus: P-007-CZP

Abstract (EN): The Flexible Time-Triggered CAN (FTT-CAN) is a master/slave network which uses replicated masters in order to avoid the single point of failure that a single master would represent. Each FTT-CAN replicated masters holds a replica of a communications requirements table, and slaves may request online updates of this table. These updates are the only source of inconsistency among the master replicas. This work addresses the design and modeling of a distributed protocol for updating this replicated communication requirements table in a consistent way, despite faults in the channel as well as physical faults in the nodes. The protocol is thoroughly described, a simulation and verification model of the protocol is presented, and the key properties to be satisfied by the protocol are formulated over this verification model. Finally, these properties are verified for the case of three replicas of the master and one slave. The verification model has been specified using the formal description language PROMELA (PRO-tocol MEta LAnguage), and the formal verification has been carried out with the Spin (Simple PROMELA Interpreter) model checking tool. © 2004 IEEE.

Idioma: Inglês

Tipo (Avaliação Docente): Científica