Computer Aided Formal Design of Swarm Robotics Algorithms
In: https://hal.sorbonne-universite.fr/hal-03111541 ; 2021, 2021
Online
report
Zugriff:
Previous works on formally studying mobile robotic swarms consider necessary and sufficient system hypotheses enabling to solve theoretical benchmark problems (geometric pattern formation, gathering, scattering, etc.). We argue that formal methods can also help in the early stage of mobile robotic swarms protocol design, to obtain protocols that are correct-by-design, even for problems arising from real-world use cases, not previously studied theoretically. Our position is supported by a concrete case study. Starting from a real-world case scenario, we jointly design the formal problem specification, a family of protocols that are able to solve the problem, and their corresponding proof of correctness, all expressed with the same formal framework. The concrete framework we use for our development is the PACTOLE library based on the COQ proof assistant.
| Titel: |
Computer Aided Formal Design of Swarm Robotics Algorithms
|
|---|---|
| Autor/in / Beteiligte Person: | Balabonski, Thibaut ; Courtieu, Pierre ; Pelle, Robin ; Rieg, Lionel ; Tixeuil, Sébastien ; Urbain, Xavier ; Laboratoire Méthodes Formelles (LMF) ; Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay) ; CEDRIC. Systèmes sûrs (CEDRIC - SYS) ; Centre d'études et de recherche en informatique et communications (CEDRIC) ; Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)-Conservatoire National des Arts et Métiers CNAM (CNAM) ; HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)-HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)-Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)-Conservatoire National des Arts et Métiers CNAM (CNAM) ; HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)-HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM) ; VERIMAG (VERIMAG - IMAG) ; Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ) ; Université Grenoble Alpes (UGA) ; Networks and Performance Analysis (NPA) ; LIP6 ; Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS) ; Laboratory of Information, Network and Communication Sciences (LINCS) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut Mines-Télécom Paris (IMT)-Sorbonne Université (SU) ; Distribution, Recherche d'Information et Mobilité (DRIM) ; Laboratoire d'InfoRmatique en Image et Systèmes d'information (LIRIS) ; Université Lumière - Lyon 2 (UL2)-École Centrale de Lyon (ECL) ; Université de Lyon-Université de Lyon-Université Claude Bernard Lyon 1 (UCBL) ; Université de Lyon-Institut National des Sciences Appliquées de Lyon (INSA Lyon) ; Université de Lyon-Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Centre National de la Recherche Scientifique (CNRS)-Université Lumière - Lyon 2 (UL2)-École Centrale de Lyon (ECL) ; Université de Lyon-Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Centre National de la Recherche Scientifique (CNRS) |
| Link: | |
| Zeitschrift: | https://hal.sorbonne-universite.fr/hal-03111541 ; 2021, 2021 |
| Veröffentlichung: | HAL CCSD, 2021 |
| Medientyp: | report |
| Schlagwort: |
|
| Sonstiges: |
|