Detail

Verifiable WCET by abstract interpretation

Modern real-time systems demand safe determination of bounds on the execution times of programs.

Static analysis methods provide sound and efficient mechanisms for determining execution time bounds, regardless of knowledge on input data. We present a calculational and compositional development of a functional static analyzer using the theory of abstract interpretation. A particular instantiation of our data flow framework was created for the static analysis of the worst-case execution time (WCET) of a program.

The target platform for program analysis is the ARM9 microprocessor platform, commonly used by many embedded systems. The verification of embedded programs is performed directly in the compiled assembly code and uses the WCET as the safety parameter. We reuse the notion of certificate in the context of Abstract-Carrying Code (ACC) and extend this framework with a verification mechanism for linear programming (LP) using the duality theory of LP.

Taking advantage of the generality of the framework, the WCET analysis is extended to multicore architectures with shared resources by applying the latency-rate (LR) server model to obtain sound upper-bounds of execution times of programs sharing resources. The soundness of the approach is proven with respect to a calculational fixpoint semantics for multicores, which is able to express all possible sequential ways of accessing shared resources. Experimental results show that the loss in precision introduced by the LR model is about 10% on average and is fairly compensated by the gain in analysis time, which is above 99%.