SAL and PVS Model of TTEthernet Synchronization Protocol

Published by Dashlink | National Aeronautics and Space Administration | Metadata Last Checked: August 04, 2025 | Last Modified: 2025-03-31

Timed-Triggered Ethernet (or TTEthernet)is a communication infrastructure that enables the use of Ethernet in real-time, distributed systems. TTEthernet is compatible with traditional IEEE 802.3 switched Ethernet standards, and is designed to support dataflows of mixed criticality on a single network. For traffic of the highest criticality, TTEthernet provides a timed-triggered communication service that relies on a fault-tolerant clock-synchronization protocol. We have developed formal models of parts of the TTEthernet protocols and analyzed safety-critical properties using both SAL and PVS. Related work by Wilfried Steiner is described in the SAL Wiki.

Find Related Datasets

Click any tag below to search for similar datasets

Complete Metadata

bureauCode	[ "026:00" ]
identifier	DASHLINK_601
issued	2012-06-11
landingPage	https://c3.nasa.gov/dashlink/resources/601/
programCode	[ "026:029" ]