Une méthodologie correcte par construction pour supporter la variabilité du temps d'exécution dans les systèmes temps réel – Corteva

Les idées principales du projet peuvent se résumer comme suit :
1. Nous utilisons l'analyse de Pire Temps d'Exécution (WCET) paramétrique pour calculer une formule de WCET hors ligne. La formule est paramétrée par des éléments tels que les valeurs d'entrée d'un bloc de code, ou l'état du cache d'un processeur ;
2. Nous prévoyons d'utiliser la formule durant l'exécution pour estimer une valeur plus précise du WCET ;
3. Sur la base de cette estimation, nous adaptons le comportement de l'application pour éviter de rater des échéances ;
4. Le concepteur spécifie les adaptations possibles du système à l'aide d'un langage synchrone, de manière à garantir formellement la correction fonctionnalle et temporelle ;
5. Nous proposons une méthodologie de conception afin d'assister le concepteur lors de la configuration du système.

Corteva repose sur l'expertise de ses partenaires et réutilise leurs travaux précédents, en particuliers :
- CPAL : un langage pour modéliser, simuler, vérifier et programmer des Systèmes Cyber-Physiques ;
- Prelude : un langage synchrone pour la programmation de systèmes de contrôle embarqués ;
- Analyse de WCET symbolique : une technique pour le calcul de formule de WCET paramétriques.

Le projet est actuellement dans sa deuxième année. Nous avons terminé l'analyse des besoins et le cas d'étude. Les autres workpackages sont en cours.

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).

Dans le domaine de la programmation des systèmes temps-réel critiques, il est capital de pouvoir garantir que les calculs seront réalisés dans
les délais impartis, afin d'éviter une panne catastrophique du système. Les systèmes avioniques et aérospatiaux, les systèmes électroniques dans le domaine automobile, les systèmes de contrôle de trains, etc, sont des exemples de systèmes temps-réel critiques. Pour garantir leur correction, le concepteur doit calculer une borne supérieure au temps d'exécution de chaque bloc de code de l'application, puis garantir que, dans le pire cas, chaque bloc sera ordonnancé par le système d'exploitation de manière à ce qu'il se termine avant son échéance.

De nos jours, il est difficile de construire un système temps-réel à la fois prévisible et performant sur des processeurs modernes, car la vitesse d'exécution d'un programme est très variable. Le pire cas peut être des centaines de fois plus long que le meilleur cas, en raison de paramètres variant d'une exécution à l'autre, tels que, par exemple, l'état de la mémoire cache. C'est pourquoi le concepteur sur-dimensionne généralement la puissance des processeurs, ce qui mène à un coût plus élevé du système. En raison de la volonté constante d'intégrer de nouvelles fonctionnalités, cette situation n'est pas gérable à long
terme. Bien que des méthodes aient été proposées pour prendre en compte ces importantes variations, elles ne sont pas immédiatement applicables
car elles se concentrent sur l'ordonnancement sans prendre en compte les aspects fonctionnels de l'application.

Ce projet a pour objectif général de contribuer à la conception et au développement d'une nouvelle génération de systèmes embarqués temps-réel critiques. En particulier, nous tenterons de résoudre le problème de l'importante variabilité du temps d'exécution en utilisant des modèles de programmation fiables et prouvés qui combinent aspects temporels et fonctionnels.

L'idée principale de ce projet peut être résumée comme suit. D'abord, nous utiliserons des techniques de calcul de pire temps d'exécution (Worst Case Execution Time - WCET) paramétriques, pour calculer statiquement un WCET sous la forme d'une formule. Cette formule dépend de paramètres, qui correspondent aux valeurs d'entrée du bloc de code executé et à des informations sur l'état de la mémoire cache. Ensuite, nous instancierons cette formule dynamiquement à l'exécution pour estimer un temps d'exécution plus précis. Cette estimation permettra, à l'exécution, de détecter l'occurence d'un temps d'exécution exceptionnellement élevé afin d'adapter le comportement de l'application de manière à garantir le respect des échéances. Le concepteur spécifiera le comportement de l'application à l'aide d'un langage synchrone pour garantir formellement à la fois la sûreté fonctionnelle et la sûreté
temporelle. Enfin, nous proposons l'utilisation d'une méthodologie pour aider le concepteur à configurer son système de la meilleure façon possible.