SAL and PVS Model of TTEthernet Synchronization Protocol

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
5 tte_synchro_var.sal https://c3.nasa.gov/dashlink/static/media/dataset/tte_synchro_var_2.sal
5 tte_synchro_fixed.sal https://c3.nasa.gov/dashlink/static/media/dataset/tte_synchro_fixed_2.sal
5 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). https://c3.nasa.gov/dashlink/static/media/dataset/tte_synchro_2.sal
47 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). https://c3.nasa.gov/dashlink/static/media/dataset/tte_compression.dmp

Tags

  • dashlink
  • nasa
  • ames

Topics

Categories