SAL and PVS Model of TTEthernet Synchronization Protocol

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

Summary

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)
License
N/A (edit)
Programming Language
N/A (edit)
Version
N/A (edit)

Source Files

tte_synchro.sal
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
tte_synchro_var.sal
11.5 KB 17 downloads
tte_synchro_fixed.sal
10.5 KB 18 downloads
tte_compression.dmp
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

Support/Documentation

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

Discussions

Add New Comment