Title: The TTEthernet synchronisation protocols and their formal verification
Authors: Wilfried Steiner; Bruno Dutertre
TTTech Computertechnik AG, Schönbrunnerstr. 7, A-1040 Vienna, Austria
SRI International, Computer Science Laboratory, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, USA
Abstract: 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.
Keywords: clock synchronisation; fault tolerance; formal verification; model checking; TTEthernet; SAE AS6802; synchronisation protocols; critical computer-based systems; distributed systems; Ethernet; latency; jitter.
Int. J. of Critical Computer-Based Systems, 2013 Vol.4, No.3, pp.280 - 300
Submission date: 01 Oct 2012
Date of acceptance: 01 May 2013
Available online: 22 Dec 2013