Proving “no cliques” in a protocol

The trend in the transport industry is to have electronic systems without mechanical backup, so-called “by-wire” systems. Microcomputers control the steering, brakes, powertrain, etc. Robust protocols are needed to make these microcomputers communicate. They should be fault-tolerant and yet not let the microcomputers split into disjoint communicating subsets. TTP (Time-Triggered Protocol) has been proposed for the automotive industry. In this paper, we investigate the clique avoidance mechanism of TTP/C (the latest version of TTP), and prove that it is effective, maybe even too strong