NASA NTRS · 20120003666
Integrated Formal Analysis of Timed-Triggered Ethernet
Abstract
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.
Keep this discovery
Explore connections, maps & timelines
Dutertre, Bruno, Shankar, Nstarajan, Owre, Sam. 2012-03-01. Integrated Formal Analysis of Timed-Triggered Ethernet. https://ntrs.nasa.gov/citations/20120003666
Cite the original work for its findings. Save a collection to share your selection of sources.