Safe, Adaptive, and Provable Protocols for Oblivious Robots Operation – SAPPORO
Safe, Adaptive, and Provable Protocols for Oblivious Robots Operation
Networks of mobile sensors are able to execute collectively various complex tasks. A characteristic feature is the extreme dynamism of their structure, content, load, and even execution environment. Obtaining certified guarantees on they behaviour is a crucial issue, as informal reasoning in that context possibly leads to disastrous errors when arguments are not perfectly clear.
SAPPORO aims to propose a formal provable framework to assess the correctness of localised distributed protocols.
«The ambition of Project SAPPORO is to lay the foundations of a formal framework and methodology aimed at mobile robot designers, to enable the certification of tentative robot protocols for any property related to their spatio-temporal behaviour that is useful in practise, or to demonstrate the impossibility of such designs. In order to provide strong guarantees on mobile robots protocols and properties we aim to propose a framework based on a formal model that can help both specialists and non specialists of formal proof in establishing and certifying their developments regarding swarms of robots. Designing such a framework amounts to defining the best-suited formal model, developing libraries and proof techniques to manage the developments, and providing an integrated development environment for designing and proving protocols for robotic swarms. These are the three fundamental challenges of SAPPORO :<br />1. What can we express formally? <br />2. What is the most convenient way to express it?<br />3. How can we put it in practice?<br />The formal model is at the core of the proposal, as all fundamental properties, algorithms, proofs, and developed tools are to use it. This model must permit to express hypotheses that are typically made by algorithm designer, regarding in particular the space in which robots move and act, the environment and various execution schemes, and the paradigms at work in protocols.<br />The thrustworthiness of autonomous robots is a major societal challenge, and mainstream media consider mobile robotic swarms as one of the “five key game-changing Technologies”. Designed to assist for both formal proof and clear specifications of behaviours, SAPPORO will help both research and industry in the crucial issue of providing trusted distributed systems. In particular, the formal framework to derive certified proofs is to be made freely available to the scientific community.«
«SAPPORO’s approach is to combine and extend current means to specify, means to design, and means to prove in a single easy to understand package. On the one hand, it provides means to specify both distributed protocols and their properties in a relatively easy way, especially for a non specialist of formal proof. On the other hand, it eases the actual proof development with its libraries of theorems and proof techniques. The model described above and the proofs of its main properties will be performed in COQ . Since all other tools will refer to this model, this ensures our methodology is built on a solid, consistent base.
A first component is the building of the fundamental formalisations to tackle mobile robot protocols that are extremely dy-
namic in their structure, content, and load, in order to encompass the main characteristics of the application
scenarios we consider, namely: multidimensional spatial environments, asynchrony in robots operations, and probabilistic behaviours.
A second component is to ensure that notions in protocols and proof steps identified as fundamental are easily manageable
and shared as much as possible, so as to ease both the specification and proving processes. It involves development of libraries, and a focus on automation.
The overall goal is an integrated development environment for developing and proving protocols for robotic swarms. This environment will gather several crucial elements together: a specification language, its associated verification conditions generator and a framework aiming at bringing all the facilities into a useful set of features through a integrated IDE.«
-
-
«- Stand Up Indulgent Rendez-vous. Quentin Bramas, Anissa Lamani, Sébastien Tixeuil. In Proceedings of SSS 2020, Austin, Texas, November 2020.
- Partial Gathering of Mobile Robots from Multiplicity-Allowed Configurations in Rings. Masahiro Shibata, Sébastien Tixeuil. In Proceedings of SSS 2020, Austin, Texas, November 2020.
- Using Model Checking to Formally Verify Rendezvous Algorithms for Robots with Lights in Euclidean Space. Xavier Défago, Adam Heriban, Sébastien Tixeuil, Koichi Wada. In Proceedings of IEEE SRDS 2020, Shanghai, China, October 2020.
- Du discrètement continu au continûment discret. Thibaut Balabonski, Pierre Courtieu, Robin Pelle, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain. In Algotel 2020, Lyon, France, October 2020.
- On the Encoding and Solving of Partial Information Games. Yackolley Amoussou-Guenou, Souheib Baarir, Maria Potop-Butucaru, Nathalie Sznajder, Léo Tible and Sébastien Tixeuil. In Proceedings of NETYS 2020, Marrackech, Morocco, June 2020.«
An emergent trend has recently received significant attention: networks of passively and/or actively mobile sensors (that is, swarms of robots). These robots are able to execute collectively various complex tasks; one application being for example to optimise the coverage of interest zones under natural or human disaster, and help in search and rescue tasks. A characteristic feature is the extreme dynamism of their structure, content, load, and even execution environment. Possibly the subjects to Byzantine failures, obtaining certified guarantees on their behaviour is a crucial issue, as they belong to an area of computer science well-known for being remarkably harsh on informal reasoning, possibly leading to disastrous errors when arguments are not perfectly clear. Project SAPPORO aims to propose a formal provable framework (mechanised in the (awarded) Coq proof assistant) to assess the correctness of localised distributed protocols at the core of dynamic mobile sensor networks.
Project coordination
Xavier Urbain (UMR 5205 - LABORATOIRE D'INFORMATIQUE EN IMAGE ET SYSTEMES D'INFORMATION)
The author of this summary is the project coordinator, who is responsible for the content of this summary. The ANR declines any responsibility as for its contents.
Partner
LIP6 Laboratoire d'informatique de Paris 6
Tokyo Institute of Technology / DDS
CEDRIC CENTRE D'ETUDES ET DE RECHERCHE EN INFORMATIQUE ET COMMUNICATIONS
LIRIS UMR 5205 - LABORATOIRE D'INFORMATIQUE EN IMAGE ET SYSTEMES D'INFORMATION
Help of the ANR 358,959 euros
Beginning and duration of the scientific project:
December 2019
- 48 Months
