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

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 communication 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 (PROtocol MEta LAnguage), and the formal verification has been carried out with the Spin (Simple PROMELA Interpreter) model checking tool.