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.
Resources
| Name | Format | Description | Link |
|---|---|---|---|
| tte_compression.dmp | Text | 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). | Open resource |
| tte_synchro.sal | Binary | 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). | Open resource |
| tte_synchro_fixed.sal | Binary | tte_synchro_fixed.sal | Open resource |
| tte_synchro_var.sal | Binary | tte_synchro_var.sal | Open resource |