Integrated Formal Analysis of Timed-Triggered Ethernet
Bruno Dutertre, Nstarajan Shankar, Sam Owre · NASA STI Repository (National Aeronautics and Space Administration) · 2012
We present new results related to the verification of the Timed-Triggered Ethernet (TTE) clock synchronization protocol. This work extends previous verification of TTE based on model checking. We identify a suboptimal design choice in a compression function used in clock synchronization, and propose an improvement. We compare the original design and the improved definition using the SAL model checker.