Verifying Timing Properties of Safety-Critical Embedded Software by Abstract Interpretation

International audienceMany tasks in safety-critical embedded systems have hard real-time characteristics. A schedulability analysis has to be performed in order to guarantee that all timing constraints will be met. It requires the worst-case execution time (WCET) of each task in the system to be known prior to its execution. AbsInt's worst-case execution time an-alyzer aiT computes safe and precise upper bounds for the WCETs of tasks taking into account cache and pipeline behavior. Information required for WCET estimation such as computed branch targets and loop bounds is determined by static analysis. For complex situations where aiT's analysis methods do not succeed, a convenient specification and annotation language was developed. The analysis results are determined without the need to change the code and hold for all executions with arbitrary input