{'fraction_non_alphanumeric': 0.026817219477769938, 'fraction_numerical': 0.0014114326040931546, 'mean_word_length': 5.387387387387387, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
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.