The French National Research Agency Projects for science

Voir cette page en français

ANR funded project

Société de l'information et de la communication (DS07) 2017
Projet Corteva

A Correct-by-construction methodology for supporting execution time variability in real-time systems

In real-time safety critical systems, it is of paramount importance to guarantee that computation is performed within certain time bounds, otherwise a critical failure may happen. Avionics and aerospace systems, electronic automotive systems, train control systems, etc, are all examples of real-time safety-critical systems. To guarantee correctness, the designer needs first to compute bounds on the execution time of every block of code, and then to guarantee that, in the worst-case, every block is scheduled by the operating system to complete before its deadline.

Today, it is difficult to build efficient and predictable real-time systems on modern processors, because the execution time of a piece of code exhibits a large variability. The worst-case can be hundreds of times larger than the best-case, due to dynamically varying paremeters such as the state of cache memories for instance. Therefore, the designer needs to greatly over-provision the computational capacity of the processors, leading to a higher cost of the system. The continued demand for additional functionalities makes the situation unsustainable in the long term. While some methods have been proposed to deal with
such large variations, they are not immediately applicable because they focus on scheduling without considering the functional aspects of the application.

The overall objective of this project is to contribute to the design and development of the next generation of safety critical embedded real-time systems. In particular, we aim at solving the problem of the large variability of execution times by using sound and provably correct programming models that combine functional and timing aspects.

The main idea can be summarised as follows. First, we will use parametric Worst-Case Execution Time analysis techniques for computing off-line a WCET formula. The formula is parametrised with respect to input values of the code block and to state of the processor cache. Then, we plan to use the formula at run-time to dynamically estimate a tighter upper bound to the execution time. The execution time estimation will be used at run time to dynamically select the
application behaviour so as to avoid deadline misses. The designer will specify the behaviour of the system by using a synchronous language to formally guarantee at the same time functional and timing correctness. Finally, we propose to use a design methodology to help the designer configure the system in the best way.


CRIStAL Centre de Recherche en Informatique, Signal et Automatique de Lille



ANR grant: 523 174 euros
Beginning and duration: - 36 mois


ANR Programme: Société de l'information et de la communication (DS07) 2017

Project ID: ANR-17-CE25-0003

Project coordinator:
Monsieur Giuseppe Lipari (Centre de Recherche en Informatique, Signal et Automatique de Lille)


Back to the previous page


The project coordinator is the author of this abstract and is therefore responsible for the content of the summary. The ANR disclaims all responsibility in connection with its content.