Title: The TTEthernet synchronisation protocols and their formal verification

Authors: Wilfried Steiner; Bruno Dutertre

Addresses: 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.

DOI: 10.1504/IJCCBS.2013.058398

International Journal of Critical Computer-Based Systems, 2013 Vol.4 No.3, pp.280 - 300

Received: 03 Oct 2012
Accepted: 01 May 2013
Published online: 29 Apr 2014 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article