Johan Arcile soutient sa thèse de doctorat le vendredi 13 décembre 2019 à 14h00 dans le Petit Amphithéâtre du site IBGBI
Titre: Conception, modélisation et vérification formelle d’un système temps-réel d’agents coopératifs : Application aux véhicules autonomes communicants
Résumé:
Cette thèse est motivée par la question de la validation de propriétés dans un système composé de plusieurs agents mobiles prenants individuellement des décisions en temps réel. Chaque agent a une perception de l’environnement qui lui est propre et peut communiquer avec les autres agents à proximité.
L’application qui a été choisie comme cas d’étude est celle des véhicules autonomes, qui du fait du large nombre de variables impliquées dans la représentation de tels systèmes, rend impossible des approches naïves. Les problématiques traitées concernent, d’une part, la modélisation d’un tel système, notamment le choix du formalisme et du niveau d’abstraction du modèle, et d’autre part, la mise en place d’un protocole d’évaluation de la prise de décision des véhicules. Ce dernier point inclut la question de l’efficacité de l’exploration de l’espace d’états du modèle. La thèse présente un ensemble de travaux, pouvant être complémentaires, visant à traiter ces problématiques. Tout d’abord, le système, composé des véhicules autonomes et de leur environnement, est défini avec précision. Il permet notamment d’observer l’impact des communications entre véhicules sur leur comportement. Le cadre logiciel VerifCar dédié à l’analyse de prise de décision de véhicules autonomes communicants est ensuite présenté. Il inclut un modèle paramétrique d’automates temporisés offrant la possibilité de vérifier des propriétés de logique temporelle. Une méthodologie d’analyse utilisant ces propriétés est présentée. On propose également une approche complémentaire permettant dans certains cas une meilleure efficacité et une plus grande expressivité. Elle est fondée sur le formalisme des MAPTs (Multi-Agent with timed Periodic Tasks), qui a été conçu pour la modélisation de systèmes temps réel d’agents coopératifs. Des algorithmes permettant une exploration dynamique des états de ce type de modèles (c’est à dire sans que l’espace d’états ne doive être préalablement construit) sont présentés.
Enfin, une méthode combinée alliant la simulation aux outils de vérification de modèle afin de contrôler le niveau de réalisme est décrite et appliquée au cas d’étude.
- Date: vendredi 13/12/2019, 14h00
- Lieu: IBISC site IBGBI, petit amphithéâtre
- Doctorant: Johan ARCILE, IBISC équipe COSMO
- Direction de thèse coté IBISC: Hanna KLAUDEL (PR Univ. Evry, IBISC équipe COSMO)
- Le document de thèse est sur HAL
