Symmetry Reduction of Time-Triggered Ethernet Protocol

Time-Triggered Ethernet is a relatively new protocol for safety-critical Local Area Network environments, known for its reliability and efficiency in providing seamless fail-safe communication. This paper presents a formal verification of the TTEthernet protocol, based on an interpretation of the TTEthernet specification document, applied to two formal network scenarios that represent a real-time, safety-critical setting. The conceptual model of both scenarios are modeled using the probabilistic timed automata, then, encoded into PRISM code. Also, a set of precise functional requirements is derived from the TTEthernet specification document and expressed using PCTL. Using this approach, the TTEthernet protocol was verified as applied to real-life network environments and one faulty state was identified within one of the settings, thus revealing a possible weak point in TTEthernet protocol.