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.

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 parameters such as the state of cache memories for instance.

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.

Click on the left menu for more information on the project.

The Symbolic WCET computation tool WSymb is released

Posted on Mon 20 April 2020

WSymb, our Symbolic Worst-Case Execution Time computation tool, is now available to the public. The main specificity of WSymb is that, instead of a constant WCET, it computes a WCET formula, where symbols (or parameters) can correspond to various kinds of values unnkown at analysis time. The formula can later be instanciated, when parameter values are known.

Check it out on the CRIStAL gitlab