Why AI + ILP is good for WCET, but MC is not, nor ILP alone

Abstract

A combination of Abstract Interpretation (AI) with Integer Linear Programming (ILP) has been successfully used to determine precise upper bounds on the execution times of real-time programs, commonly called worst-case execution times (WCET). The task solved by abstract interpretation is to verify as many local safety properties as possible, safety properties who correspond to the absence of “timing accidents”. Timing accidents, e.g. cache misses, are reasons for the increase of the execution time of an individual instruction in an execution state. This article attempts to give the answer to the frequently encountered claim, “one could have done it by Model Checking (MC)!”. It shows that it is the characteristic property of abstract interpretation, which proves AI to be applicable and successful, namely that it only needs one fixpoint iteration to compute invariants that allow the derivation of many safety properties. MC seems to encounter an exponential state-space explosion when faced with the same problem. ILP alone has also been used to model a processor architecture and a program whose upper bounds for execution times was to be determined. It is argued why the only ILP-only approach found in the literature has not led to success.