The TTEthernet synchronisation protocols and their formal verification Online publication date: Tue, 29-Apr-2014
by Wilfried Steiner; Bruno Dutertre
International Journal of Critical Computer-Based Systems (IJCCBS), Vol. 4, No. 3, 2013
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.
Existing subscribers:
Go to Inderscience Online Journals to access the Full Text of this article.
If you are not a subscriber and you just want to read the full contents of this article, buy online access here.Complimentary Subscribers, Editors or Members of the Editorial Board of the International Journal of Critical Computer-Based Systems (IJCCBS):
Login with your Inderscience username and password:
Want to subscribe?
A subscription gives you complete access to all articles in the current issue, as well as to all articles in the previous three years (where applicable). See our Orders page to subscribe.
If you still need assistance, please email subs@inderscience.com