Soutenance de thèse de Ran BAO (équipe AELOS)

Ran Bao, doctorante au sein de l’équipe AELOS, soutiendra sa thèse intitulée « Modélisation formelle de systèmes de drones civils à l’aide de méthodes probabilistes paramétrées » / « Parametric Statistical model checking of UAV flight plan »

jeudi 7 mai 2020 à 10h, en visio.

Jury :
– Directeur thèse : Chirstian Attiogbé
– Co-encadrant : Benoit Delahaye
– Rapporteurs : Patricia Bouyer-Decitre (ENS Paris Saclay), Laure Petrucci (U. Paris 13)
– Autres membres : Olga Kouchnarenko (U. Franche Comté), Claude Jard
– Membre invité : Philippe Barranger (Pixiel)

Résumé : Les drones sont maintenant très répandus dans la société et sont souvent utilisés dans des situations dangereuses pour le public environnant. Il est alors nécessaire d’étudier leur fiabilité, en particulier dans le contexte de vols au-dessus d’un public. Dans cette thèse, nous étudions la modélisation et l’analyse de drones dans le contexte de leur plan de vol. Pour cela, nous construisons plusieurs modèles probabilistes du drone et les utilisons ainsi que le plan de vol pour modéliser la trajectoire du drone. Le modèle le plus détaillé obtenu prend en compte des paramètres comme la précision de l’estimation de la position par les différents capteurs, ainsi que la force et la direction du vent. Le modèle est analysé afin de mesurer la probabilité que le drone entre dans une zone dangereuse. Du fait de la nature et de la complexité des modèles successifs obtenus, leur vérification avec les outils classique, tels que PRISM ou PARAM, est impossible. Nous utilisons donc une nouvelle méthode d’approximation, appelée Model Checking Statistique Paramétrique. Cette méthode a été implémentée dans un prototype, que nous avons mis à
l’épreuve sur ce cas d’étude complexe. Nous avons pour finir utilisé les résultats fournis par ce prototype afin de proposer des pistes permettant d’améliorer la sécurité du public dans le contexte considéré.

Mots-clés : Drone, Modèle formel, Chaîne de Markov, Model checking statistique paramétrique

*********

Abstract: Unmanned Aerial Vehicles (UAV) are now widespread in our society and are often used in a context where they can put people at risk. Studying their reliability, in particular in the context of flight above a crowd, thus becomes a necessity. In this thesis, we study the modeling and analysis of UAV in the context of their flight plan. To this purpose, we build several parametrics probabilistic models of the UAV and use them, as well as a given flight plan, in order to model its trajectory. Our most advanced model takes into account the precision of position estimation by embedded sensors, as well as wind force and direction. The model is analyzed in order to measure the probability that the drone enters an unsafe zone. Because of the nature and complexity of the obtained models, their exact verification using classical tools such as PRISM or PARAM is impossible. We therefore develop a new approximation method, called Parametric Statistical Model Checking. This method has been implemented in a prototype tool, which we tested on this complex case study. Finally, we use the result to propose some ways to improve the safety of the public in our context.

Keywords: UAV, Formal Model, Markov Chain, Parametric statistical model checking