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 -
BIN
tte_synchro.sal
BIN -
BIN
tte_synchro_fixed.sal
BIN -
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 |
