Contribution à un langage de modélisation automobile formellement vérifié pour les logiciels embarqués critiques

Référence interne : C26-RGE-AMS/ST4

I – Contexte
A. Thème et problématique de recherche
L'introduction du Software Defined Vehicle (SDV) et l'augmentation des données et des calculs a nécessité l'introduction d'un nouveau paradigme dans la communication des données entre les capteurs, les unités de calcul et les actuateurs. Contrairement à l'architecture AUTOSAR utilisée dans le monde automobile où toutes les données sont communiquées de manière périodique et très rapide sur un bus Ethernet automobile, dans ce nouveau paradigme seuls les modifications des données et les évènements sont communiqués et ce de manière asynchrone. La communication concurrente et l'utilisation d'un bus Ethernet peut induire une congestion et un déni de service, mais aussi des comportements non déterministes et des effets de bords non maîtrisés en cas de suréchantillonnage. La sûreté peut être compromise.
Lors de sa thèse CIFRE réalisée à Ampere (Groupe Renault) et encadrée au Département d'Ingénierie des Systèmes Complexes de l'ISAE-SUPAERO et au laboratoire LIP6 de Sorbonne Université, Émilie Thomé a introduit GRust, un langage dédié pour modéliser des services en SDV. Le compilateur de GRust est écrit en Rust et produit du code Rust, automatisant ainsi la génération de code à partir d'un modèle du service. Émilie Thomé a également montré que le code produit vérifie des propriétés de sureté : déterminisme, sans allocation dynamique, mémoire bornée. Elle a également démontré et testé le théorème de suréchantillonnage qui montre que le code produit est insensible au changement de paradigme de périodique à on-change.
Cependant, si GRust apporte une preuve de concept prometteuse, il reste de nombreuses limitations. Tout d'abord pour que l'outil puisse être qualifié par une agence, il faut l'outiller pour automatiser la traçabilité. Ensuite, la preuve du théorème de suréchantillonnage est complexe, longue et manuelle. L'automatiser à l'aide d'un assistant de preuve permettrait d'augmenter la confiance dans le code généré et est un atout pour la qualification ISO26262.

GRust permet actuellement de concevoir et de générer du code pour chaque service indépendamment. L'interface des services doit être écrite à la main. La prochaine étape est de générer cette interface automatiquement en analysant globalement le système et en guidant l'ordonnanceur pour qu'il respecte les propriétés de sûreté (déterminisme et préservation par suréchantillonnage), mais aussi qu'il s'adapte aux contraintes temporelles et de répartition de charge de calcul.
Les services sont interfacés à l'aide d'un ordonnanceur asynchrone qui repose sur un algorithme de work stealing. Actuellement, il repose sur l'utilisation de la bibliothèque Rust Tokio dont les propriétés de sureté ne sont pas vérifiées. La qualification de l'outil reposera sur l'implémentation d'un ordonnanceur et d'un runtime dont les propriétés seront prouvées formellement en s'appuyant sur l'effort de la communauté distribuée pour proposer des alternatives pour lesquelles les contraintes temporelles et l'absence d'interblocage sont assurées.

B. État de l’art scientifique & Vérification formelle
1. Compilation
CompCert (Leroy, 2016) est le premier compilateur dont la préservation de la sémantique a été vérifiée formellement à l'aide de l'assistant de preuve Rocq. Ce travail réalisé par Xavier Leroy (Professeur au Collège de France) et son équipe a ensuite été utilisé dans plusieurs projets logiciels, par exemple chez Airbus. Le compilateur certifié Velus (Bourke, 2019) est lui aussi vérifié formellement en Rocq. Il prend en entrée du code Lustre (similaire à du code SCADE) et produit du code C compatible avec CompCert. Baptiste Pollien a écrit dans sa thèse de doctorat (Pollien, 2023) effectué à l'ISAE-SUPAERO et à l'ENAC un compilateur de plans de vol pour un drone décrits dans un langage de haut niveau vers du code C compatible avec CompCert et embarquable directement dans l'autopilote Paparazzi.
Il existe plusieurs alternatives pour prouver l'invariance sémantique lors de la compilation. Par exemple, le compilateur LustreC (Brun, 2023) permet d'équiper les programmes écrits en Lustre avec des contrats spécifiant leur comportement. Ces contrats sont transportés vers le code C généré via le langage de spécification ACSL et sont ensuite prouvé de façon automatique. Dans sa thèse, Son Ho a posé les bases théoriques et conçu les outils pour la vérification formelle de programmes Rust via des transformations fonctionnelles, en définissant une sémantique purement fonctionnelle pour la partie sûre du langage, intégrant son modèle d’emprunts. Une traduction fonctionnelle vers un λ-calcul pur permet ensuite l’utilisation d’outils de preuve matures tels que Lean ou Rocq pour raisonner sur des programmes Rust.

2. Systèmes multipériodiques
La prise en compte globale de services ayant des périodicités différentes a été étudiées dans plusieurs travaux. Dans leur travail Bourke & al (Bourke T. a., 2023) ont étendu Lustre pour équilibrer la charge de calcul et respecter les contraintes en termes de ressources limitées et de latences de bout en bout. Dans leur travail sur le langage Prelude, Forget & al (Wyss, 2015) étudient également les latences de bout en bout dans des systèmes multipériodiques.
3. Ordonnanceur asynchrone
Un effort important est déployé par la communauté de l'informatique distribuée pour concevoir des ordonnanceurs qui ont des bonnes propriétés. Par exemple, dans Scheduling Parallel Programs by Work Stealing with Private Deques (Acar, 2013), Arthur Chargueraud prouve les propriétés théoriques d'un algorithme de workstealing avec queue privée qui communiquent par message. Certains travaux utilisent des algorithmes de model checking pour prouver qu'il n'existe pas de trace d'exécution qui viole les contraintes temporelles et de mémoire (cf. Formally Verified Block-based Work Stealing for Parallel Processing (Chen, 2023)).
II – Objectifs de la thèse
L'objectif de la thèse est d'apporter des garanties formelles sur la sûreté du code modélisé et généré à travers le langage GRust et les outils associés en vue de leur utilisation dans un contexte industriel automobile sous la norme ISO26262.

1.
Traçabilité des spécifications (génération du graphe de dépendance, liste des variables etc).
2.
Preuve formelle des propriétés du code généré (déterminisme, productivité, stabilité par sur-échantillonnage).
3.
Génération automatique de l'interface des services.
4.
Conception d'un runtime asynchrone sûr dont les propriétés de contraintes temporelles et d'utilisation des ressources sont formellement garanties.
5.
Études de cas industriels pour l'évaluation des performances du code généré.
A. Objectifs et contribution aux axes R&AE (Research & Advanced Engineering) de Ampere

Il est essentiel pour Ampere de se doter de techniques de modélisation et de vérification performantes qui traitent les problématiques et de sureté et de flexibilité pour adresser la complexité croissante des systèmes logiciels et de leur environnement. Le gain en flexibilité et en performance résultant de l’association d’un langage réactif à la génération de code vers différents langages industriels permettrait d’élargir le champ d’application de méthodes MBD – généralement limitées au domaine du logiciel temps réel embarqué et des modules de commande électronique (ECU) simples – à des applications ADAS ou IHM complexes.
L’utilisation d’un langage certifié et de sa chaine d’analyse statique contribue quant à elle directement à l’objectif principal : la sécurité, la sûreté et la fiabilité des applications.

B. Etat de l’art chez Ampere
Historiquement, l’outil principal utilisé chez Ampere est Simulink/Stateflow pour la modélisation, et associé avec les générateurs de code de MathWorks. L’environnement Simulink permet de modéliser et d'autogénérer le code pour les ECU du power-train et du Body Control Module (BCM). Mais les algorithmes ADAS ou IHM n'étaient pas modélisés, par la complexité de modélisation des flux évènementiels avec les outils actuels.
Aujourd'hui, de nouveaux travaux se concentrent sur l'étude de la sûreté de fonctionnement, notamment dans les systèmes ADAS et le contrôle châssis/moteur. Un axe majeur est la preuve formelle de l'intégralité de la chaîne de code généré par Matlab/Simulink en utilisant par exemple les outils directement intégrés. Également, une collaboration a été établie avec l'entreprise SERMA qui fournit les outils SafeProver, un outil de model checking, et IFFREE, un outil d'analyse statique, visant à déduire la preuve de sûreté d'un système complet à partir des preuves de sûreté de ses composants individuels.
Dans le contexte du tableau de bord du véhicule, les fonctions critiques contribuent directement à garantir la sûreté de fonctionnement, notamment pour l’affichage d’informations réglementaires ou d’alertes sur l’état du véhicule. Par exemple, il est essentiel de garantir l’affichage ou le déclenchement d’une alerte sonore pour signaler une défaillance critique à l’utilisateur. Le développement de ces fonctions safety-capable, développée selon l’ISO 26262, n’est pas réalisé en interne ce qui limite la capacité de Ampere à les faire évoluer rapidement. Dans cette optique, créer un générateur de code vérifié comme Grust est une première étape importante, afin de maitriser le développement de ces fonctions critiques. La seconde étape est de pouvoir exécuter le code asynchrone généré par un runtime sûr. Les runtimes asynchrones classiques comme Tokio, ne fournisse aucune garantie de sûreté et ne sont généralement pas compatible avec les environnements d’exécution ASIL utilisés par Ampere. C’est pourquoi il serait intéressant de développer un runtime asynchrone vérifié, adapté aux besoins du code généré par Grust et conçu pour les environnements d’exécution sûrs.

III – Méthodologie et Programme de Travail
A. Programme
Année 1 : Etat de l’art et prototypage

Etude bibliographique

Apprentissage de l’environnement Automobile et méthodes formelles,

Refonte du langage avec intégration de l’interfaçage et prototypage d’une chaine de compilation

Rédaction d’un document de synthèse.

Préparation d’une première publication de conférence.
Année 2 : Développement et vérification

Développement et vérification de la chaine de compilation complète.

Rédaction d’une publication pour une conférence internationale et nationale, et préparation d’une publication de journal.
Année 3 : Validation et rédaction

Simulation sur étude de cas fournit par Ampere,

Rédaction du manuscrit de thèse

Valorisation scientifique : publication en revue et en conférences internationales.
B. Principaux livrables

Langage de spécification sous la forme d’une grammaire ANTLR ou BNF

Prototype de la chaine de compilation

Preuve formelle de la sûreté du code généré

Exemples de conception fonctionnelle et caractérisation de l'efficacité de la programmation fonctionnelle dans le développement d'applications accessibles, sûre et efficace pour l'automobile.

Publications dans des revues internationales à comité de lecture (JACM, TCS, ...)

Présentation des travaux dans des conférences internationales de rang A (POPL, ICFP, LICS, EMSOFT)
C. Liste des activités de recherche

Développement d'un langage de programmation appliqué à la spécification fonctionnelle.

Publication d'articles de recherche dans des revues et conférences internationales en langages de programmation. Participation à des conférences

de recherche (Langage de programmation POPL, Informatique Théorique LICS, Langage de programmation réactifs et synchrones SYNCHRONES).

Le doctorant ou la doctorante devra aussi participer à un projet de développement logiciel chez Ampere afin de maîtriser les outils et les besoins et de définir les contours d'un langage de programmation adapté aux besoins de l'entreprise tant en termes de sécurité que de performance du logiciel.
D. Articulations des activités entre Ampere et le laboratoire
Cette thèse sera réalisée en collaboration entre le laboratoire de recherche de l’ISAE-SUPAERO et l'entreprise Ampere, entité du groupe Ampere spécialisée dans les véhicules électriques et le software.

Les activités de recherche bibliographique, la définition d’algorithmes d’analyse statique et la recherche de preuve formelle seront principalement encadrées par le labo.

Pour la définition des objectifs de sureté (ISO-26262) et les activités de modélisation MID/HID le doctorant aura accès aux outils de conception logiciel et aux experts Ampere.

La spécification de la sémantique et de la grammaire du langage sera encadrée par un expert Ampere et se fera en étroite collaboration avec l’enseignant-chercheur. Le doctorant et l’enseignant-chercheur auront accès l’infrastructure Devops de Ampere.

Méthodes utilisées :
o
Ingénierie logicielle : Model-Based-Design, Programmation Évènementielle, Programmation Réactive, programmation concurrente
o
Théorie des Langages de Programmation : Compilation, Certification, Vérification formelle, Sémantique, Programmation Fonctionnelle
ISAE-SUPAERO, département DISC
Au sein de l’ISAE-SUPAERO, le Département d’ingénierie des systèmes complexes (DISC) développe des compétences en mathématiques et informatique pour l’ingénierie aéronautique et spatiale.
En enseignement comme en recherche, il s’intéresse aux modèles, méthodes et outils nécessaires pour maîtriser le comportement et les performances de systèmes complexes. Cette complexité peut être induite par le caractère multi-physiques ou multi-échelles des systèmes étudiés, leur comportement dynamique, leur structure distribuée et communicante.

Le Département d’Ingénierie des Systèmes complexes de l’ISAE possède les forces suivantes :

une équipe « méthodes formelles » qui vient d’être renforcée avec pour ambition l’innovation dans la vérification de systèmes embarqués

une équipe technique avec une longue expérience de la robotique terrestre et des drones aériens, avec en particulier une flotte de drones et une volière pour des expérimentations grandeur nature

des équipements de simulation à travers le projet PRISE (Plateforme de Recherche et d’Ingénierie en Systèmes Embarqués), financés par un contrat CPER

une tradition de collaboration avec les agences liées à la Défense et les industriels de l’aéronautique
Bibliographie
Acar, U. A. (2013). Scheduling parallel programs by work stealing with private deques. Association for Computing Machinery.
Bourke, T. a. (2019). Mechanized semantics and verified compilation for a dataflow synchronous language with reset. POPL.
Bourke, T. a. (2023). Scheduling and Compiling Rate-Synchronous Programs with End-To-End Latency Constraints. 35th Euromicro Conference on Real-Time Systems (ECRTS 2023).
Brun, L. a.-L. (2023). Equation-Directed Axiomatization of Lustre Semantics to Enable Optimized Code Validation. ACM Trans. Embed. Comput. Syst.
Chen, J. W. (2023). BWoS: Formally Verified Block-based Work Stealing for Parallel Processing. 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI 23).
Leroy, X. a. (2016). CompCert - A Formally Verified Optimizing Compiler. ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress.
Pollien, B. (2023). Formal Verification of an UAV autopilot: Static analysis and Verified Code Generation.

Wyss, R. a. (2015). Calcul de propriétés temps réel de bout-en-bout dans un programme synchrone multi-périodique. Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques.