SAL and PVS Model of TTEthernet Synchronization Protocol
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.
Resources
4 resources available
-
tte_compression.dmp
TXT -
tte_synchro.sal
BIN -
tte_synchro_fixed.sal
BIN -
tte_synchro_var.sal
BIN
Find Related Datasets
Search by Tags
Click any tag below to search for similar datasets
Complete Metadata
| @type | dcat:Dataset |
|---|---|
| accessLevel | public |
| accrualPeriodicity | irregular |
| bureauCode |
[ "026:00" ] |
| contactPoint |
{ "fn": "Kevin Schweiker", "@type": "vcard:Contact", "hasEmail": "mailto:kevin.schweiker@honeywell.com" } |
| description | 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. |
| distribution |
[ { "@type": "dcat:Distribution", "title": "tte_compression.dmp", "format": "TXT", "mediaType": "text/plain", "description": "The following PVS file contains a general specification of TTEthernet's compression function and proofs of several important properties. The specification and proofs were developed using PVS 5.0 (2/11/2012).", "downloadURL": "https://c3.nasa.gov/dashlink/static/media/dataset/tte_compression.dmp" }, { "@type": "dcat:Distribution", "title": "tte_synchro.sal", "format": "BIN", "mediaType": "application/octet-stream", "description": "The following SAL specifications focus on TTEthernet's compression function. They show that better synchronization can be achieved by a simple change to the original TTEthernet definition (2/11/2012).", "downloadURL": "https://c3.nasa.gov/dashlink/static/media/dataset/tte_synchro_2.sal" }, { "@type": "dcat:Distribution", "title": "tte_synchro_fixed.sal", "format": "BIN", "mediaType": "application/octet-stream", "description": "tte_synchro_fixed.sal", "downloadURL": "https://c3.nasa.gov/dashlink/static/media/dataset/tte_synchro_fixed_2.sal" }, { "@type": "dcat:Distribution", "title": "tte_synchro_var.sal", "format": "BIN", "mediaType": "application/octet-stream", "description": "tte_synchro_var.sal", "downloadURL": "https://c3.nasa.gov/dashlink/static/media/dataset/tte_synchro_var_2.sal" } ] |
| identifier | DASHLINK_601 |
| issued | 2012-06-11 |
| keyword |
[ "ames", "dashlink", "nasa" ] |
| landingPage | https://c3.nasa.gov/dashlink/resources/601/ |
| modified | 2025-03-31 |
| programCode |
[ "026:029" ] |
| publisher |
{ "name": "Dashlink", "@type": "org:Organization" } |
| title | SAL and PVS Model of TTEthernet Synchronization Protocol |
