NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Collections About News Help Login
Back to Results
Integrated Formal Analysis of Timed-Triggered EthernetWe 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.
Document ID
20120003666
Acquisition Source
Langley Research Center
Document Type
Contractor Report (CR)
Authors
Dutertre, Bruno (SRI International Corp. Menlo Park, CA, United States)
Shankar, Nstarajan (SRI International Corp. Menlo Park, CA, United States)
Owre, Sam (SRI International Corp. Menlo Park, CA, United States)
Date Acquired
August 25, 2013
Publication Date
March 1, 2012
Subject Category
Computer Systems
Report/Patent Number
NASA/CR-2012-217554
NF1676L-14373
Report Number: NASA/CR-2012-217554
Report Number: NF1676L-14373
Funding Number(s)
TASK: NNL10AB32T
WBS: WBS 534723.02.02.07.30
Distribution Limits
Public
Copyright
Public Use Permitted.

Related Records

There are no records associated with this record.
No Preview Available