Logotype Mälardalenn University
This web site has been moved.
Please visit our new and improved web site at: http://www.es.mdh.se/
Startpage www.mdh.se

The Static Analysis Research Direction

Researchers involved

Björn Lisper (Professor), Adam Betts (PostDoc), Amine Maref (PostDoc), Stefan Bygde (PhD Student), Marcelo Santos (PhD Student), Jan Gustafsson (Senior Lecturer).

Context and research overview

Static analysis is an important technique to establish properties of program code, including nonfunctional properties such as execution time. It can be used to prove the absence of certain runtime errors, which makes it apt to analyse embedded, safety-critical code. For CBSE, static analysis can be used on two levels: intra-component level, analysing the code of components in isolation, and inter-component level, analysing code assembled from components using the analysis results for the individual components. Our research has targeted both these levels, and we have mainly considered Worst-Case Execution Time (WCET) analysis for safety-critical real-time systems.

Major results

Highlight 18 - Parametric WCET analysis [Show]

Such an analysis returns a parameterized upper WCET bound as a formula in symbolic input parameters. This kind of analysis is appropriate for reusable components, which can be expected to have a highly parameterized behaviour. WCET formulas can also capture dependencies between WCET&s of different components. We have implemented and evaluated a parametric WCET analysis method, including a proof of correctness of its parametric loop bounds analysis. Various improvements have been made in the underlying, supporting analyses. We have developed an efficient parametric WCET calculation method (the "Minimum Propagation Algorithm" [57, 58, 59], best paper award at RTCSA’09).

Highlight 19 - Approximate timing models for early WCET analysis [Show]

We have developed a method to automatically identify approximate timing models for source code from measurements. Such models can be used to compute WCET estimates early in the design process, when doing time budgeting or hardware dimensioning. We have implemented the method and evaluated its use in approximate source-level static WCET analysis, with promising results [60, 61], and methods that replace the problematic fine-grained instrumentation of traditional hybrid analysis with end-to-end timing measurements [62].

Highlight 20 - Hybrid WCET analysis [Show]

Such analysis methods combine static analysis and timing measurements, and they can be appropriate for timing analysis of black- or grey-box components. We have made various improvements to these techniques, in particular utilizing the so-called “instrumentation point graph” which captures the control flow between instrumentation points in the code [63]. We have also developed methods to perform WCET analysis entirely from time stamped traces [64, 65].

Highlight 21 - Improved static WCET analysis techniques[Show]

We have improved static WCET analysis techniques in a number of ways. Worth particular mentioning are a method to perform WCET calculation by abstract interpretation rather than the traditional, ILP-based calculation [66], and a method to find the input vector causing the WCET that uses an efficient search strategy based on static WCET analysis [67]. We have also investigated how to improve in the real WCET by memory positioning of code and data [68].

Highlight 22 - Composable timing models [Show]

Sequential real-time code is assembled from component code by sequential composition. Timing estimates for the resulting code can then be derived from the timing information about the components by simple, compositional timing models. We have investigated the validity of such models with respect to hardware effects stemming from features such as caches and pipelines: a simple, additive timing model [69], and a probabilistic model for execution time distributions ([70], best paper award at CRTS 2011). We also investigated which hardware features were likely to be most influential on the validity of the models.

Highlight 23 - Composable WCET analysis [Show]

We have developed a composable WCET analysis method for component-based systems, where the components have parametric WCET estimates. The method uses Constraint Logic Programming (CLP) to handle conditions ("contracts") on the environments of components [71].

Highlight 24 - SWEET [Show]

SWEET is our prototype WCET analysis tool. Early versions of SWEET existed before PROGRESS, but during the course of PROGRESS SWEET has been developed, and enhanced in a number of ways so it can be considered a major outcome of the project.

  • Mälardalen University |
  • Box 883 |
  • 721 23 Västerås/Eskilstuna |
  • 021-101300, 016-153600 |
  • webmaster |
  • Latest update: 2013.02.25