Runtime Analysis of Synchronous Programs for Low-Level Real-Time Verification

Synchronous programming languages are well-suited for the implementation and verification of real-time systems. The main benefit for the estimation of real-time constraints is thereby that the macro steps provided by the semantics of synchronous languages can be directly used as building blocks for runtime analysis. We describe a new approach to determine the execution times of the macro steps of a syn-chronous program wrt. given microprocessors and generate real-time formal models endowed with notions of physical time for formal verification purposes. The execution times are exact, since we consider all possible input sequences.