Compilers and Timing Analysis

aiT
Worst-Case Execution Time Analyzer

aiT Worst-Case Execution Time Analyzer

In real-time systems, timely task completion is of the essence. Each real-time task has to be completed within a specified time frame in order
to ensure that the system works correctly. In other words, it is essential that the WCET of each task is known.

Computing the WCET is a challenge: Testing by repeatedly measuring the execution time of a task is typically not safe: it is often impossible
to prove that the conditions determining maximum execution time have been taken into account. Modern processor components like caches and pipelines complicate the task of determining the WCET considerably, since the execution time of a single instruction may depend on the execution history. Analysis methods that do not consider cache and pipeline behavior typically overestimate the WCET by an order of magnitude or more, thus leading to a substantial waste of hardware resources.

aiT WCET Analyzers provide the solution to these problems: they statically analyze a task’s intrinsic cache and pipeline behavior based on formal cache and pipeline models. This enables correct and tight upper bounds to be computed for the worst-case execution time.
The analyzers compute the results automatically. The computed WCET bounds are valid for all possible inputs and each execution of a task under any circumstances. Thus, aiT enhances safety and saves valuable development time.

The analyzers are based on the technique of abstract interpretation. A graphical user interface supports the visualization of the worst-case
program path and the interactive inspection of all pipeline and cache states at arbitrary program points. aiT-computed tight bounds reflect the
actual performance of an embedded system. aiT WCET Analyzers directly analyze binary executables. They are widely independent of the compiler and source code language used.

The WCET determination is composed of several different tasks.
  • Reconstruction of the control flow from binary executables
  • Value analysis: computation of address ranges for instructions accessing memory
  • Cache analysis: classification of memory references as cache misses or hits
  • Pipeline analysis: predicting the behavior of the program on the processor pipeline
  • Path analysis: determination of the worst-case execution path of the program
  • Analysis of loops and recursive procedures

aiT was designed by Saarland University and AbsInt Angewandte Informatik GmbH according to the requirements of Airbus France for validating the timing behavior of critical avionics software. A publication of Airbus on the use of aiT is available here

aiT, its infrastructure to analyze binary code and internal program representation are widely used by academics within Artist II and outside.

Recent Publications

Christian Ferdinand, Florian Martin, Christoph Cullmann, Marc Schlickling,
Ingmar Stein, Stephan Thesing and Reinhold Heckmann.
New Developments in WCET Analysis.
In Thomas Reps, Mooly Sagiv, and Jörg Bauer, editors,
Program Analysis and Compilation, Theory and Practice. Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday (Lecture Notes in Computer Science 4444), pages 12-52. Springer, 2007.

Christian Ferdinand, Reinhold Heckmann, Hans-Joerg Wolff, Christian Renz, Oleg Parshin, Reinhard Wilhelm.
Towards Model-Driven Development of Hard
Real-Time Systems - Integrating ASCET-MD and aiT/StackAnalyzer.
In Proceedings of the Automotive Software Workshop in San Diego, 2006, San Diego, USA, March 2006.

Christian Ferdinand, Reinhold Heckmann and Bärbel Franzen.
Static Memory and Timing Analysis of Embedded Systems Code.
In Perry Groot, editor, Proceedings of the 3rd European Symposium on Verification and Validation of Software Systems (VVSS 2007) on March 23, 2007 at Eindhoven, The Netherlands (TUE Computer Science Reports 07-04), pages 153-163. Eindhoven, 2007

Links

aiT
Timing Validation

(c) Artist Consortium, All Rights Reserved - 2006, 2007, 2008, 2009

Réalisation Axome - Création de sites Internet