Reliable and Precise WCET Determination

   AbsInt follows an approach to compute reliable run-time guarantees which is both well-based on theoretical foundations and practical from a software engineering and an efficiency point of view. Several aspects are essential to our approach:

• Modularity: As far as possible for a given processor architecture, the task of determining the WCET is structured into a sequence of subtasks that can be solved in isolation. Interference between processor components may prevent this modularity.

• Adequacy of methods: Each sub-task is tackled by appropriate methods. This guarantees efficiency of computation and precision of results.

• Genericity: Generic and generative methods are used whenever possible. This allows a large number of different processor architectures and the evolution of processor families to be properly dealt with.

   These principles lead to an understandable, maintainable, efficient, and provably correct system. In the following, an overview of the methods used in the AbsInt approach to WCET determination is given. A sample pipeline model for the Motorola ColdFire MCF5307 processor is presented.

Next: Introduction | Contents | Home