Français Anglais
Accueil Annuaire Plan du site
Home > Research results > Dissertations & habilitations
Research results
Thesis in progress de

Thesis in progress
Group :

Contribution to the formal modelling of mobile robot swarms

Starts on 01/10/2016
Advisor : CONTEJEAN, Evelyne

Funding : Contrat doctoral uniquement recherche
Affiliation : Université Paris-Saclay
Laboratory : LRI - VALS

Defended on 18/12/2020, committee :
Rapporteurs :
- David Ilcinkas, Chargé de recherche, Université de Bordeaux
- Micaela Mayero, Maître de conférences, Université Paris 13

Examinateurs :
- Quentin Bramas, Maître de conférences, Université de Strasbourg
- Isabelle Guérin Lassous, Professeure, Université Claude Bernard Lyon 1
- Pascale LeGall, Professeure, Université Paris Saclay
- Xavier Urbain, Professeur, Université Claude Bernard Lyon 1

Directrice :
- Évelyne Contejean, Directrice de recherche, CNRS

Co-Encadrant :
- Thibaut Balabonski, Maître de conférences, Université Paris Saclay

Invités :
- Lionel Rieg, Maître de conférences, ENSIMAG
- Sébastien Tixeuil, Professeur, Sorbonne Université

Research activities :

Abstract :
Distributed Algorithm is among domains where informal reasoning is not an option, especially when Byzantine errors may occur. It is also characterized by a large variety of models whose subtle modulations imply radically different properties. We are interested in "robotic network": clouds of autonomous entities performing a cooperative task. The applications that these swarms of agents offer are extremely promising: exploration and search for survivors in devasted areas, patrols and drone flights in formation, etc. These few potentially critical exemples underline the high dynamicity of the model; they also indicate how failures of robots or errors in the distributed protocols that equip them can have distastrous consequences.

To ensure the safety of the protocols and the security of tasks, we aim to optain, with the help of the Coq proof assistant, foraml mechanical validations of properties of certain distributed protocols. A prototype of Coq's formal model for robot network, Pactole, has recently shown the feasibility of an proof assistant verification in this framework. It captures quite naturally many variants of these networks, especially with regard to topology or the properties of demons. This model is of course in the higher order, and is based on coinductive types. It makes it possible to demonstrate in Coq both positive properties: the embedded program makes it possible to carry out the task regardless of the initial configuration, as negative properties: there is no embedded program to complete the task.

In the emerging framework of robot networks, the models are distinguished by the characteristics and capabilities of the robots, the topology of the space in which they evolve, the degree of synchronism (modelled by the properties of the activation demon), the error that can occure, etc. The prototype Pactole expresses only some of these variants. Thought in a theoretical framework (point robots, instantaneous movement, etc.), hypotheses remain out of reach, in particular realistic hypothesis such as totally asynchronous executions, or risk of collision. The absence of collision is fundamental in all applications relates to formation flights (drones) and critical safety condition as soon as one is interested in air transport. Formal validation of this property is therefore of great importance.

The work consits of extending the formal model to take into account asynchronous evolutions of large robots. This modelling should allow easy formulation of protocols and the task they are supposed to perform. Particular attention will be given to ensuring the absence of collisions during potentially complex movements.

Ph.D. dissertations & Faculty habilitations
The topic of this habilitation is the study of very small data visualizations, micro visualizations, in display contexts that can only dedicate minimal rendering space for data representations. For several years, together with my collaborators, I have been studying human perception, interaction, and analysis with micro visualizations in multiple contexts. In this document I bring together three of my research streams related to micro visualizations: data glyphs, where my joint research focused on studying the perception of small-multiple micro visualizations, word-scale visualizations, where my joint research focused on small visualizations embedded in text-documents, and small mobile data visualizations for smartwatches or fitness trackers. I consider these types of small visualizations together under the umbrella term ``micro visualizations.'' Micro visualizations are useful in multiple visualization contexts and I have been working towards a better understanding of the complexities involved in designing and using micro visualizations. Here, I define the term micro visualization, summarize my own and other past research and design guidelines and outline several design spaces for different types of micro visualizations based on some of the work I was involved in since my PhD.