An abstract interpretation-based timing validation of hard real-time avionics software

Hard real-time avionics systems like flight control software are expected to always react in time. Consequently, it is essential for the timing validation of the software that the worst-case execution time (WCET) of all tasks on a given hardware configuration be known. Modern processor components like caches, pipelines, and branch prediction complicate the determination of the WCET considerably since the execution time of a single instruction may depend on the execution history. The safe, yet overly pessimistic assumption of no cache hits, no overlapping executions in the processor pipeline, and constantly mispredieted branches results in a serious overestimation of the WCET Our approach to WCET prediction was implemented for the Motorola ColdFire 5307. It includes a static prediction of cache and pipeline behavior, producing much tighter upper bounds for the execution times. The WCET analysis tool works on real applications. It is safe in the sense that the computed WCET is always an upper bound of the real WCET It requires much less effort, while producing more precise results than conventional measurement-based methods.