TTEthernet Synchronization Services and Report on the Formal Methods

  • 2010-05-11

TTEthernet is a communication infrastructure for mixed-criticality systems that integrates dataflow from applications with criticality levels on single network

Abstract

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.

Biography

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.

Speakers

Note: This is one of the thousands of items we imported from the old website. We’re in the process of reviewing each and every one, but if you notice something strange about this particular one, please let us know. — Thanks!