Yann DUPLOUY

Doctorant, IRT SystemX

À propos

Courte présentation

Je suis désormais chercheur post-doctoral dans l'équipe VeriDis au Loria, sous la direction de Stephan Merz et Marie Duflot-Kremer.

J'ai été en thèse à l'IRT SystemX et au LSV sous la direction de Serge Haddad et de Béatrice Bérard depuis octobre 2015.

Pour en savoir plus

Je dispose aussi d'un site professionnel général où vous pourrez trouver mon CV.

Recherche (Thèse)

Publications

Voir ma liste de publications

Développement logiciel

Je participe activement au développement du model-checker Cosmos.

Sujet de thèse

Soutenance

Je soutiens le 26 novembre 2018; les informations pratiques sont disponibles sur la page de la soutenance.

Titre

Application des méthodes formelles au contrôle du véhicule autonome

Résumé

Cette thèse s'inscrit dans le cadre de la conception de véhicules autonomes et plus spécifiquement de la vérification de controleurs de tels véhicules. Nos contributions à la résolution de ce problème sont les suivantes : (1) fournir une syntaxe et une sémantique pour un modèle de systèmes hybrides, (2) étendre les fonctionnalités du model checker statistique Cosmos à ce modèle et (3) valider empiriquement la pertinence de notre approche sur des cas d'étude typiques du véhicule autonome.

Nous avons choisi de combiner le modèle des réseaux de Petri stochastiques de haut niveau (qui était le formalisme d'entrée de Cosmos) avec le formalisme d'entrée de Simulink afin d'atteindre un pouvoir d'expression suffisant. En effet Simulink est très largement utilisé dans le domaine automobile et de nombreux contrôleurs sont spécifiés avec cet outil. Or Simulink n'a pas de sémantique formellement définie. Ceci nous a conduit à concevoir une telle sémantique en deux temps : tout d'abord en introduisant une sémantique dite exacte mais qui n'est pas opérationnelle puis en la complétant par une sémantique approchée intégrant le facteur d'approximation recherché.

Afin de combiner le modèle à événements discrets des réseaux de Petri et le modèle continu spécifié en Simulink, nous avons proposé au niveau syntaxique une interface reposant sur de nouveaux types de transitions et au niveau sémantique une extension de la boucle de simulation. L'évaluation de ce nouveau formalisme a été entièrement implémentée dans Cosmos.

Grace à ce nouveau formalisme, nous avons développé et étudié les deux cas d'étude suivants : d'une part une circulation dense sur une section d'autoroute et d'autre part l'insertion du véhicule dans une voie rapide. L'analyse des modélisations correspondantes a démontré la pertinence de notre approche.

Quelques éléments pour comprendre

La création de systèmes permettant aux véhicules d'être autonomes dans certaines situations est un défi essentiel pour l'ensemble des acteurs de l'industrie automobile. La modélisation des véhicules et de leur environnement est complexe, et nécessite souvent un temps de calcul long.

Au lieu d'utiliser une simulation physique complète (ou de faire rouler directement des véhicules), techniques exactes mais bien trop coûteuses en temps pour produire les résultats attendus (des probabilités de collision de l'ordre de 10-9 par 100km), certains acteurs ont décidé de découper le problème en plus petits morceaux, testant par exemple d'un côté l'usure d'un amortisseur ou l'aérodynamisme de la carosserie.

Parmi ces problèmes se pose la question centrale des décisions prises par le contrôleur embarqués dans ces véhicules. L'objectif de ma thèse est d'élaborer une méthode permettant de tester directement le contrôleur décisionnel embarqué, et de le faire de manière suffisamment optimale pour répondre aux normes fixées.

À propos du LSV

Contact

Yann DUPLOUY
Adresse
LSV, CNRS & ENS de Cachan
61, avenue du Président Wilson
94235 CACHAN Cedex, France
Fax
+33 (0)1 47 40 75 21
Secr.
+33 (0)1 47 40 75 20
E-Mail
yann (dot) duplouy (at) lsv.fr