Contribution à un langage de modélisation automobile formellement vérifié pour les logiciels em[...]

Overview

Contribution à un langage de modélisation automobile formellement vérifié pour les logiciels embarqués critiques, en collaboration avec Ampère Software Technology et l’ISAE‑Supaero. L’objectif est de fournir des garanties formelles pour la sûreté du code généré en fonction de la norme ISO26262.

Responsibilities

• Développer et valider un compilateur et une chaîne de compilation pour le langage GRust.
• Automatiser la traçabilité des spécifications (graphes de dépendance, liste des variables, etc.).
• Élaborer et présenter des preuves formelles des propriétés du code généré (déterminisme, stabilités par sur‑échantillonnage).
• Concevoir et implémenter une interface automatique des services à partir des modèles.
• Développer un runtime asynchrone sûr, avec démonstration formelle des contraintes temporelles et de l’utilisation des ressources.
• Conduire des études de cas industriels pour évaluer les performances du code produit.

Deliverables

• Spécification de langage sous forme de grammaire ANTLR ou BNF.
• Prototype de la chaîne de compilation complète.
• 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.
• Publications scientifiques (revues et conférences internationales).

Contract Details

Job Family: TransverseDuration: 36 months