The TTEthernet synchronisation protocols and their formal verification
Wilfried Steiner, Bruno Dutertre · International Journal of Critical Computer-Based Systems · 2013
TTEthernet is a communication platform for critical, distributed computer-based systems. NASA has selected one of TTEthernet’s high-end configurations for the Orion programme. In other configurations, TTEthernet implements the communication backbone of new energy machineries such as wind turbines. One of TTEthernet’s unique features is the integration of applications with differing latency, jitter, and fault-tolerance requirements in a single physical Ethernet network, thereby significantly reducing the amount of wiring in a distributed system. The most critical applications can communicate using time-triggered messages for which a fault-tolerant high-precision network-wide timebase is required. Formal methods are key in the design of protocols that establish and maintain such a timebase and, thus, have been heavily used already during the design phase of TTEthernet. This paper summarises the formal analysis and verification activities of the TTEthernet synchronisation protocols and discusses protocol updates implemented in the TTEthernet standard SAE AS6802.