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.