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

• Type: Article in International Conference Proceedings Book
• Date: 2004

Authors

Rodriguez Navas, G (Author) Other; Rigo, J (Author) Other; Proenza, J (Author) Other; Ferreira, J (Author) Other; Luis Almeida (Author) Other; Fonseca, JA (Author) Other

Conference proceedings International

Title: IEEE International Workshop on Factory Communication Systems - Proceedings, WFCS

Pages: 229-238

Indexing

Scopus - 6 Citations

Other information

Authenticus ID: 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.

Language: English

Type (Professor's evaluation): Scientific