SAL and PVS Model of TTEthernet Synchronization Protocol

A dataset shared by Kevin Schweiker, updated on Jun 11, 2012


Contributing Author(s) :
Bruno Dutertre

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.

show more info
Operating System
N/A (edit)
N/A (edit)
Programming Language
N/A (edit)
N/A (edit)

Source Files

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).
11.2 KB 44 downloads
11.5 KB 17 downloads
10.5 KB 18 downloads
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).
545.8 KB 28 downloads


For any questions, contact this resource's administrator: K2


Add New Comment