[Invited Paper] Formal Methods for Mobile Robots: Current Results and Open Problems

Béatrice Bérard 1 Pierre Courtieu 2, 3 Laure Millet 1 Maria Potop-Butucaru 4 Lionel Rieg 5 Nathalie Sznajder 1 Sébastien Tixeuil 6, 4, 7 Xavier Urbain 8, 9
1 MoVe - Modélisation et Vérification
LIP6 - Laboratoire d'Informatique de Paris 6
2 GALLIUM - Programming languages, types, compilation and proofs
Inria Paris-Rocquencourt
3 CEDRIC - Centre d'études et de recherche en informatique et communications
4 NPA - Networks and Performance Analysis
LIP6 - Laboratoire d'Informatique de Paris 6
5 CdF - Collège de France
6 LINCS - Laboratory of Information, Network and Communication Sciences
7 IUF - Institut Universitaire de France
8 ENSIIE - Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise
9 LRI - Laboratoire de Recherche en Informatique
Abstract : Mobile robot networks emerged in the past few years as a promising distributed computing model. Existing work in the literature typically ensures the correctness of mobile robot protocols via ad hoc handwritten proofs, which are both cumbersome and error-prone. This paper surveys state-of-the-art results about applying formal methods approaches (namely, model-checking, program synthesis, and proof assistants) to the context of mobile robot networks. Those methods already proved useful for bug-hunting in published literature, designing correct-by-design optimal protocols, and certifying impossibility results. We also present related open questions to further develop this path of research.
Document type :
Journal articles
Complete list of metadatas
https://hal.sorbonne-universite.fr/hal-01238784
Contributor : Sébastien Tixeuil <>
Submitted on : Monday, December 7, 2015 - 10:29:54 AM
Last modification on : Thursday, December 19, 2019 - 1:32:04 AM

Identifiers

  • HAL Id : hal-01238784, version 1

Collections

UPMC | CNRS | CNAM | INSTITUT-TELECOM | UMR8623 | LIP6 | INRIA | LRI-VALS | PSL | UNIV-PARIS-SACLAY | CENTRALESUPELEC | UNIV-HESAM | SORBONNE-UNIVERSITE | CEDRIC-CNAM | SU-SCIENCES

Citation

Béatrice Bérard, Pierre Courtieu, Laure Millet, Maria Potop-Butucaru, Lionel Rieg, et al.. [Invited Paper] Formal Methods for Mobile Robots: Current Results and Open Problems. International Journal of Informatics Society, Japan Informatics Society, 2015, 7 (3), pp.101-114. ⟨hal-01238784⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

798

Contact

Informations

CCSD