[Thèse de doctorat] Vérification des Stratégies de Conduite pour des Véhicules Autonomes

Contexte de la thèse

Au sein de l’Institut de Recherche Technologique SystemX, situé au cœur du campus scientifique d’excellence mondiale de Paris-Saclay, vous prendrez une part active au développement d’un centre de recherche technologique de niveau international dans le domaine de l’ingénierie numérique des systèmes. Adossé aux meilleurs organismes de recherche français du domaine et constitué par des équipes mixtes d’industriels et d’académiques, cet institut a pour mission de générer de nouvelles connaissances et solutions technologiques en s’appuyant sur les percées de l’ingénierie numérique et de diffuser ses compétences dans tous les secteurs économiques.

Plus particulièrement au sein de l’IRT SystemX, le doctorant sera rattaché au domaine « Sûreté de Fonctionnement ». Le sujet de thèse a été défini par le consortium réuni dans le cadre du projet « Chaîne outillée pour la Validation et l’Homologation du véhicule automatisé connecté » (CVH). La direction de la thèse sera assurée par Burkhart Wolff du Laboratoire Méthodes Formelles (LMF) de l’Université Paris-Saclay et la thèse sera inscrite à l’école doctorale STIC (ED STIC). Le doctorant bénéficiera d’un encadrement scientifique à l’IRT par Paolo Crisafulli, ingénieur-chercheur de l’institut.

Le poste est basé à l’IRT SystemX – Palaiseau avec des déplacements réguliers au laboratoire LMF. Hormis les déplacements en conférences internationales, un séjour long à l’étranger dans un laboratoire partenaire pourra être envisagé. La date souhaitée de démarrage de la thèse est le 01/10/2023. La rémunération de la thèse est de 2700€ brut mensuel sur 3 ans, portée par l’IRT SystemX.

Sujet de thèse

Résumé

La modélisation et l’analyse des véhicules autonomes (VA), cas particulier de systèmes cyber-physiques, est un défi pour les méthodes formelles et un domaine de recherche actif. À l’heure actuelle, la validation des propriétés de sécurité des VA sont généralement établies par des simulations. L’objectif de cette thèse est d’étendre cette approche et d’adapter un cadre existant basé sur la preuve formelle. Ce cadre permet la conception et la validation d’un VA avec une dynamique plus complexe, des topologies routières variées, et des occlusions partielles des systèmes de perception. Les preuves formelles des propriétés de sécurité dans l’environnement Isabelle/HOL simplifieront considérablement le cycle d’ingénierie en fournissant des critères de sécurité mesurables et atteignables ainsi qu’une méthode d’optimisation des plans de test.

Description

Les systèmes cyber-physiques tels que les robots ou les VA étant en fort développement dans le milieu industriel, le besoin de certification de sécurité s’étend. Les méthodes formelles sont naturellement candidats pour adresser ces besoins et relever les défis scientifiques correspondants. Les systèmes cyber-physiques se caractérisent par des interactions concurrentes, des observables continus obéissant aux lois de la physique, et par le fait que les acteurs ne possèdent qu’une version discrétisée de ces observables. L’analyse de ces systèmes nécessite donc l’établissement des propriétés du système au moyen de tests formels systématiques et de preuves mécanisées. Cette thèse s’appuiera sur un environnement développé dans [5] pour la modélisation et l’analyse formelle des systèmes cyber-physiques en général et des cas concrets sous forme d’études de cas du domaine des VA. À grands traits, notre environnement est fondé sur une intégration conservative de la théorie des processus séquentiels communicants (CSP) [12] dans Isabelle/HOL qui sert à la fois d’environnement de modélisation et d’analyse. Les notions de raffinement standards de CSP peuvent être adaptées à la communication et à l’interaction ainsi qu’à une représentation particulière discrétisée/échantillonnée des variables continues des CPS. Le plongement de HOL-CSP [11] dans Isabelle/HOL donne accès à des théories sophistiquées sur l’analyse fonctionnelle et les espaces vectoriels, qui se prêtent à des langages d’ontologie spécifiques à un domaine, tels que le référentiel de scénarios MOSAR [14], bien connu dans le domaine des VA. L’environnement proposé suppose que les VA sont des processus HOL-CSP appelés acteurs qui s’accordent à des instants temporels spécifiques sur un état physique global. Sur la base de cet état physique global, une fonction particulière à l’intérieur d’un acteur (la stratégie de conduite), calcule un ensemble d’accélérations possibles. Des choix non déterministes à chaque début d’intervalle de temps se traduiront par des trajectoires possibles des VA dans le scénario, et les états des acteurs évolueront dans cet intervalle de temps en fonction de leur cinématique continue.

Objectifs

Étude de stratégies de conduite des VA prenant en compte :

• des dynamiques complexes (ex. accélérations et forces externes, …) ;
• des approximations de topologies (par exemple courbes et voies, …) ;
• des perceptions partielles de la scène globale (par exemple, occlusions d’obstacles et d’acteurs) ;
• vivacité des trajectoires dans des topologies complexes.

Plan de travail 

• Étendre les théories Isabelle/CyberPhi existantes fondées sur Isabelle/HOL-CSP ;
• Modélisation formelle de nouvelles stratégies de conduite impliquant des topologies nécessitant des méthodes de preuve automatisées à l’aide de zonotopes ;
• Modélisation formelle de nouvelles stratégies de conduite impliquant des dynamiques plus complexes et le développement de certaines automatisations de preuve ;
• Étude de la vivacité des trajectoires dans des topologies complexes.

Profil recherché

De formation bac +5 (Master Recherche ou Ingénieur avec un intérêt avéré pour la recherche) en Informatique,  Mathématiques appliquées, Science des données, Apprentissage Automatique, ou équivalent.

Connaissances essentielles :

Bonne formation en informatique, analyse et programmation fonctionnelle ainsi qu’un intérêt pour les outils de preuve formelle.

Qualités professionnelles :

Goût pour la prise en compte de problématiques industrielles et de leurs traductions en questions scientifiques. Travail en équipe. Un bon niveau d’anglais est indispensable

Pour postuler, merci de renvoyer les éléments suivants : un CV, une lettre de motivation, les relevés de note de Master 2, des lettres de recommandations