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

The main ideas of the project can be summarized as follows:

1. We will use parametric Worst-Case Execution Time (WCET) analysis techniques for computing off-line a WCET formula. The formula is parametrized with respect to elements such as the input values of the code block or the state of the processor cache;
2. We plan to use the formula at run-time to estimate a tighter WCET bound dynamically;

3. Based on this estimate we will dynamically adapt the application behaviour so as to avoid deadline misses;

4. The designer will specify the possible adaptations of the system by using a synchronous language to formally guarantee at the same time functional and timing correctness;

5. We propose to use a design methodology to help the designer configure the system in the best way.


Corteva relies on the expertise of its partner and reuses some of their previous work, namely:

- CPAL: a language to model, simulate, verify and program Cyber-Physical Systems;

- Prelude: a synchronous language for programming real-time embedded control systems;

- Symbolic WCET analysis: a technique for computing parametric WCET formulae.

The project is currently in its second year. The requirement analysis and the specification of the case study is completed, the other workpackages are currently work in progress.

Combining Abstract interpretation with parametric WCET analysis (best paper at VMCAI)

Publications:

- Santinelli, Luca, et al. «Schedulability analysis for mixed critical cyber physical systems.« 2018 IEEE Industrial Cyber-Physical Systems (ICPS). IEEE, 2018.

- Santinelli, Luca, and Zhishan Guo. «A Sensitivity Analysis for Mixed Criticality: Trading Criticality with Computational Resource.« 2018 IEEE 23rd International Conference on Emerging Technologies and Factory Automation (ETFA). Vol. 1. IEEE, 2018.

- Ballabriga, Clement, et al. «Static Analysis Of Binary Code With Memory Indirections Using Polyhedra.« 2019 20th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI).

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.