Testing Implementation Soundness of a WCET Analysis Tool

We have developed and implemented the only widely used sound WCET analysis technology. The claim of soundness is a strong one, given the many necessary component techniques of WCET analysis and the need to incorporate an abstraction of the execution platform. This article deals with the qualification of the AbsInt timing-analysis tool, aiT, as required by several international standards for safety-critical software. We briefly sketch these requirements, give a short description of our timing-analysis method, and then concentrate on the most complex part, the microarchitectural analysis. This analysis phase uses an abstraction of the execution platform. To arrive at this abstraction is a complex, error-prone process. The main focus of the article is the technique to validate the abstract execution platform by trace validation.