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.
