Verification of Realtime Systems

time system from the gates until the assembler level.
This requires to argue simultaneously about i) hardware models with
different clock domains ii) serial interfaces iii) clock synchronisation
algorithms and iv) processor correctness. Then we outline how to obtain
formal correctnes proofs for distributed applications running on such
systems by combining i) ordinary correctness proofs for the local
computations and ii) worst case execution time analysis.