We formalize the correctness of a fault-tolerant scheduler in a time-triggered architecture. Where previous research elaborated on real-time protocol correctness, we extend this work to gate-level hardware. This requires a sophisticated analysis of analog bit-level synchronization and transmission. Our case-study is a concrete automotive bus controller (ABC), inspired by the FlexRay standard. For a set of interconnected ABCs, vulnerable to sudden failure, we prove at gate-level, that all operating ABCs are synchronized tightly enough such that messages are broadcast correctly. This includes formal arguments for startup, failures, and reintegration of nodes at arbitrary times. To the best of our knowledge, this is the first effort tackling fault-tolerant scheduling correctness at gate-level.

Transition systems which do not perform domain-specific operations on their state variables can be efficiently reduced. We present two different algorithms which automatically eliminate domain-specific operations and reduce the domains of occurring variables from infinite to small domains. Our work extends earlier techniques which are applicable solely to combinatorial properties to temporal properties of transition systems. We have implemented our algorithm as a proof method in the Isabelle/HOL theorem prover and applied it to bit-level hardware designs. To demonstrate the efficiency of our technique, we fully automatically verify a liveness property of a pipelined processor and correctness of a memory management unit.