TTEthernet is a communication infrastructure for mixed-criticality systems that integrates dataflow from applications with different criticality levels on a single network. For applications of highest criticality TTEthernet provides time-triggered communication. As synchronized local clocks are the fundamental prerequisite for time-triggered communication, the correctness of the synchronization strategy is therefore essential.
In this talk we discuss the formal assessment of two aspects of the TTEthernet synchronization strategy: the compression function and the startup protocol. The compression function is a core element of the clock synchronization service and 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 in its verification. The startup protocol consists of several sub-algorithms: coldstart, integration, clique detection, and restart and the focus of the formal assessment is in the interaction of these procedures.
Wilfried Steiner received a Master's and a PhD degree in Computer Science and Engineering from Vienna University of Technology. His research is focused on algorithms and services that enable dependable time-triggered communication. Wilfried Steiner is affiliated with TTTech Computertechnik AG as a Senior Research Engineer and was awarded a Marie Curie International Outgoing Fellowship in 2009. This fellowship is hosted by SRI International under the acronym CoMMiCS (Complexity Management for Mixed-Criticality Systems). At SRI International, Wilfried Steiner continues research in the application of SRI International developed tools for the verification, configuration, and further development of TTEthernet and related protocols.