Chercheur Postdoctoral (F/H) Cadre d’ingénierie pour la sûreté de fonctionnement du véhicule autonome fondée sur la preuve formelle

Rejoignez l’IRT SystemX afin d’imaginer et concevoir un monde numérique plus sûr, plus performant et plus durable. Aux côtés de nos partenaires industriels et académiques, nous adressons de nouveaux usages qui répondent aux grands enjeux de notre temps, sociétaux et technologiques. Ensemble, nous accélérons la transformation numérique des industries, des services et des territoires.

Vous désirez rejoindre un institut enthousiaste à l’expertise reconnue ? Avec nos 140 collaborateurs et collaboratrices, prenez une part active au développement d’un institut de recherche technologique (IRT) de niveau international, dans le domaine de l’ingénierie numérique des systèmes. Vous découvrirez l’intérêt stimulant de nos projets collaboratifs au sein d’un campus scientifique d’excellence mondiale, le cluster Paris-Saclay.

Ce postdoc sera réalisé dans le cadre du projet « Chaîne Outillée pour la Validation et l’Homologation des véhicules autonomes » (CVH). Ce projet s’articule autour d’une chaîne outillée générique et interopérable permettant, à partir de la définition d’un système de conduite automatisé, de générer des plans de tests afin de valider et/ou homologuer ce système, notamment par la simulation.

Vous renforcerez l’institut sur un projet qui s’insère dans la thématique « mobilité et véhicule autonome », en développant des travaux de recherche dans le domaine de la sûreté de fonctionnement.

Un partenaire académique co-encadrera ce travail de postdoc, en l’occurrence le Pr. Burkhart Wolff du Laboratoire Méthodes Formelles (LMF) de l’Université Paris-Saclay (https://lmf.cnrs.fr/).

Sujet de thèse

• Cette recherche postdoctorale s’inscrit dans le cadre du projet CVH et de sa tâche « Cadre d’ingénierie pour la safety du véhicule autonome, fondé sur la preuve formelle ».

  Le problème de la couverture de tests de validation des systèmes de transport autonome reste complexe, quelle que soit la méthode utilisée : roulages simulés ou réels, collections de scénarios, recherche de l’inconnu (SOTIF https ://www.iso.org/fr/standard/77490.html).

  L’approche Responsability-Sensitive Safety (RSS) proposée par l’entreprise Mobileye [1] [2] se démarque : l’ambition est de proposer d’emblée un niveau d’abstraction permettant de prendre en compte tous les scénarios possibles, vis-à-vis du danger de collision. Par son approche de conception « correcte par construction », elle ouvre la voie à la simplification de l’ensemble du cycle d’ingénierie du point de vue de la safety, en fournissant des critères de safety mesurables et atteignables, et en particulier une méthode d’optimisation des plans de test. Utilisée dans plusieurs projets antérieurs de l’institut avec de très bons résultats [3], cette approche permet de compléter les activités du projet CVH avec des garanties mathématiques d’exhaustivité. Cependant la preuve mathématique publiée par Mobileye reste faible : des travaux précédemment réalisés avec le LMF [4] en ont montré la fragilité sur certains cas. Notre modélisation fondée sur l’algèbre de processus Communicating Sequential Processes (CSP) a permis d’obtenir de meilleurs résultats via une approche algébrique : une formule CSP représente un ensemble abstrait de scénarios de roulage (traces), défini de manière intensive. Cependant, la limite de cette approche est du côté de la représentation extensive des scénarios. Autrement dit, il est difficile de constituer de manière systématique un ensemble d’exemples représentatifs des scénarios décrits par une formule du modèle, afin de se les représenter de manière pratique et tangible.

  Une telle représentation serait pourtant d’une grande aide pour se convaincre que les scénarios en question correspondent aux intentions initiales de la modélisation choisie, puis en convaincre les partenaires industriels, éventuellement par une représentation sous forme de simulations visuellement réalistes.

  Une première étape vers ces objectifs est de convertir la sémantique algébrique CSP vers une sémantique opérationnelle judicieusement choisie. Deux possibilités ont été identifiées :

  • encodage d’un fragment de CSP en «interaction trees » [5]
  • utiliser les Labelled Transition System (LTS) générés par la sémantique opérationnelle de CSP [6]

  Cette étape doit aboutir à la représentation sous forme de scénarios symboliques (ou scénarios logiques dans le vocabulaire métier du projet Pegasus [7]) et si possible, à une concrétisation sous forme d’exemples représentatifs (traces d’un processus), obtenus par un choix judicieux des valeurs des symboles, et illustrables sous forme de simulation automobile visuellement réaliste et intelligible.

  Les principales missions de poste sont :

  • Étudier les sémantiques opérationnelles proposées et les possibilités qu’elles offrent pour la génération de traces symboliques ou concrètes.
  • Implémenter un environnement de génération de traces à partir de formules CSP, fondé sur Isabelle/HOL en tant que plateforme de développement.

  Bibliographie

  [1] Shai Shalev-Shwartz, Shaked Shammah, Amnon Shashua. 2017. “On a Formal Model of Safe and Scalable Self-driving Cars”. https://arxiv.org/pdf/1708.06374.pdf

  [2] Philip Koopman, Beth Osyk, Jack Weast 2019. « Autonomous Vehicles Meet the Physical World: RSS, Variability, Uncertainty, and Proving Safety (Expanded Version) ».  https://arxiv.org/abs/1911.01207

  [3] Paolo Crisafulli, Safouan Taha, Burkhart Wolff 2021. « Modelling and Proving Safety in Autonomous Cars Scenarios in HOL-CSP ». https://hal.science/IRT-SYSTEMX/hal-03429597v2

  [4] Paolo Crisafulli, Safouan Taha, Burkhart Wolff2023. Modeling and analysing Cyber–Physical Systems in HOL-CSP. Robotics and Autonomous Systems. 170. 104549. DOI 10.1016/j.robot.2023.104549.

  [5] Simon Foster, Chung-Kil Hur, Jim Woodcock 2021. Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL. https://arxiv.org/abs/2105.05133

  [6] Benoît Ballenghien, Burkhart Wolff 2023. Operational Semantics formally proven in HOL-CSP. https://www.isa-afp.org/entries/HOL-CSP_OpSem.html

  [7] Till Menzel, Gerrit Bagschik, Markus Maurer 2018. Scenarios for Development, Test and Validation of Automated Vehicles. https://arxiv.org/abs/1801.08598 –

Offre de poste

Cette offre décrit un poste de Chercheur Postdoctoral en CDD de 13 mois qui est rattaché à l’équipe « Ingénierie Système et Sûreté de Fonctionnement » de l’institut SystemX.

Vos missions principales consisteront à :

• Approfondir et analyser l’état de l’art des verrous scientifiques sur le sujet identifié ;
• Élaborer des propositions méthodologiques, technologiques et architecturales en cohérence avec les attentes du projet et les propositions du partenaire académique ;
• Analyser les cas d’usages des partenaires industriels et aider à la réalisation des preuves de concept et démonstrateurs ;
• Documenter les travaux réalisés ;
• Être engagé fortement pour la réalisation de publications associées aux travaux de recherche.

Mots-clés : Preuve assistée par ordinateur, Isabelle-HOL, Communicating Sequential Processes (CSP), Modélisation de Systèmes Cyber-Physiques, Calcul de propriétés, Sûreté de fonctionnement, Liveness/Performance.

Profil recherché

Le candidat(e) devra être titulaire d’une thèse en informatique avec une spécialité méthodes formelles.

Compétences techniques

• Programmation fonctionnelle,
• Méthodes formelles pour l’informatique (théorie des langages de programmation, etc.),
• Bases en modélisation de processus concurrents en CSP ou autre algèbre de processus,
• Bases en modélisation de systèmes hybrides et cyber-physiques.
• Une expérience d’utilisation d’Isabelle/HOL serait un plus ainsi que la connaissance d’Isabelle en tant que plateforme de développement (par exemple, développement de Domain Specific Languages ou génération de code).

Qualités professionnelles et relationnelles

• Curiosité, esprit d’initiative, capacité d’analyse et rigueur
• Adaptabilité et autonomie
• Capacité à travailler en mode projet : suivi et avancement des travaux, valorisation et communication des résultats
• Aisance relationnelle, capacité à travailler en équipe, très bonne communication orale et écrite (en français et anglais)

Rédaction scientifique

L’IRT SystemX est engagé en faveur de l’égalité des chances. À ce titre, tous nos postes sont ouverts aux candidats en situation de handicap.

Pour ce poste basé au sein du cluster Paris-Saclay (91), des déplacements occasionnels sont à prévoir en région parisienne. Vous travaillerez sur des projets attractifs et vous bénéficierez d’avantages tels que : le télétravail à raison de 10 jours par mois, une protection mutuelle performante, une subvention de l’employeur pour la restauration, 3 semaines de congés en plus du légal, des congés supplémentaires en fonction de l’ancienneté, 1% logement, un comité social et économique, un partenariat avec Science Accueil permettant aux collaborateurs étrangers d’obtenir notamment un accompagnement dans les démarches administratives.

Pour en savoir plus sur l’IRT SystemX

Pour découvrir les témoignages de nos collaborateurs