Soutenance de thèse de Yann Duplouy

Informations pratiques

Date et heure

Lundi 26 novembre 2018, 14h00 heure de Paris.

Lieu

Amphithéâtre Marie Curie
École Normale Supérieure Paris-Saclay
61, avenue du Président Wilson
94 230 Cachan

Comment s'y rendre

Depuis la station de RER B Bagneux (ou ses alentours), suivez la carte de cette page pour aller à l'ENS Paris-Saclay puis cette carte une fois arrivé sur le campus. L'Amphithéâtre Marie Curie est dans le bâtiment principal: entrez dans le Bâtiment d'Alembert par son entrée principale supérieure (en haut du «Fer à Cheval»), puis suivez le couloir à gauche, jusqu'au bout.

Matériel

Les slides utilisées pour la présentation sont disponibles par ce lien. L'exemple illustré au cours de la soutenance peut être rejoué avec les éléments fournis dans ce dossier compressé.

Thèse

Titre

Applying Formal Methods to Autonomous Vehicle Control (Application des méthodes formelles au contrôle du véhicule autonome)

Mots clés

Model-checking statistique, véhicule autonome, Simulink

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 contrôleurs 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.

Manuscrit

Le manuscrit est disponible via ce lien

Jury

DANG ThaoRapporteure
DEMONGODIN IsabelRapporteure
HÉLOUET LoïcExaminateur
KLOUL LeïlaExaminatrice
PEKERGIN NihalExaminatrice
BERARD BéatriceCo-encadrante de thèse
HADDAD SergeDirecteur et co-encadrant de thèse

À propos du LSV