SMT-Based Formal Verification of a TTEthernet Synchronization Function

Abstract. TTEthernet is a communication infrastructure for mixedcriticality systems that integrates dataflow from applications with different criticality levels on a single network. For applications of highest criticality, TTEthernet provides a synchronization strategy that tolerates multiple failures. The resulting fault-tolerant timebase can then be used for time-triggered communication to ensure temporal partitioning on the shared network. In this paper, we present the formal verification of the compression function which is a core element of the clock synchronization service of TTEthernet. The compression function is located in the TTEthernet switches: it collects clock readings from the end systems, performs a faulttolerant median calculation, and feedbacks the result to the end systems. While traditionally the formal proof of these types of algorithms is done by theorem proving, we successfully use the model checker sal-inf-bmc incorporating the YICES SMT solver. This approach im...

• Type: Conference
• Year: 2010
• Where: FMICS
• Authors: Wilfried Steiner, Bruno Dutertre
• Keywords: Clock Synchronization Service, Compression Function, End Systems, FMICS 2010, Formal Methods