Model-based analysis of Timed-Triggered Ethernet

Timed-Triggered Ethernet (TTEthernet) is a communication infrastructure that enables the use of Ethernet networks in real-time, distributed applications. The core of TTEthernet is a set of fault-tolerant protocols for clock synchronization, startup, and clique detection and resolution. We present recent work on model-based analysis of the TTEthernet startup and synchronization protocols. We first use automated test-generation tools to drive high-coverage testing of prototype TTEthernet hardware, based on a state-machine model of the TTEthernet protocols. With almost no human guidance, this technique enables us to achieve MC/DC coverage of the startup protocol under valid fault scenarios. We then focus on the TTEthernet clock-synchronization protocol. We develop correctness proofs of key properties of this protocol using the PVS interactive theorem prover [1]. As a result of this formalization, we have identified a suboptimal design choice in the clock-compression function defined in the TTEthernet draft standard [2]. We propose an alternative definition and, using model-checking tools, we show that the new function achieves better clock precision than the original. These results demonstrate effective use of modeling and formal techniques in proof and test of a fault-tolerant network infrastructure relevant to avionics and other embedded systems.