MILLET Laure

Docteur
Équipe : MoVe
Date de départ : 31/08/2016
Direction de recherche : Béatrice BÉRARD
Co-encadrement : POTOP-BUTUCARU Maria, SZNAJDER Nathalie

Vérification et synthèse d'algorithmes de robots

L'adaptation et l'application des méthodes formelles de vérification et de développement à des systèmes et algorithmes distribués est un domaine de recherche très actif. Un des défis principaux réside dans la variété des modèles calculatoires qui existent en algorithmique répartie : des encodages naïfs conduisent à des espaces d'états dont la taille dépasse les capacités des outils les plus puissants de vérification.
D'autre part, la complexité intrinsèque de ces algorithmes fait que leur correction n'est pas évidente même pour leurs concepteurs.
Dans cette thèse on s'intéresse à l'analyse formelle de protocoles de robots mobiles, un modèle de calcul particulièrement original car les agents ne disposent ni de mémoire (locale ou partagée) ni de la capacité de communiquer par échange de messages.
Un cadre général permettant d'exprimer les modèles robotiques est présenté dans cette thèse.
Ce modèle a permit d'utiliser à la fois la vérification par model checking d'algorithmes proposés dans la littérature et la synthèse formelle d'algorithmes (optimaux) pour un problème donné, quelque soit le niveau d'asynchronisme du modèle robotique étudié.
Soutenance : 01/12/2015 - 14h - Site Jussieu 25-26/105
Membres du jury :
Paola Flocchini, Professeur, Ottawa University, Canada [Rapporteur]
Stephan Merz, Professeur, INRIA Nancy & LORIA [Rapporteur]
Béatrice,Bérard, Professeur, LIP6,UPMC
Amal El Fallah Seghrouchni, Professeur, LIP6, UPMC
Laure Petrucci,Professeur, LIPN, Paris 13
Maria Potop-Butucaru, Professeur, LIP6, UPMC
Nathalie Sznajder, Maitre de Conférences LIP6, UPMC
Xavier Urbain, Maitre de Conférences, LRI
Josef Widder, Professeur, TU, Wien, Austria
Situation professionnelle : - Critical System Labs

Publications 2012-2016

 Mentions légales
Carte du site |