Exact low-level runtime analysis of synchronous programs for formal verification of real-time systems

Synchronous programming languages are well-suited for the implementation and verification of real-time systems. We describe a new approach to determine the execution times of synchronous programs wrt. given micropro-cessors and generate real-time formal models endowed with notions of physical time for formal verification purposes by means of model-checking. The execution times are exact, since we consider all possible input sequences. In order to benefit from the native mathematical operators of the target CPU, we avoid the conversion of these operators to their logical equivalents, usually performed by other model-checking algorithms. For this purpose, we introduce a new technique that constructs a transition system which preserves mathematical operations as atomic actions