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

Béatrice Bérard; Pierre Courtieu; Laure Millet; Maria Potop-Butucaru; Lionel Rieg; Nathalie Sznajder; Sébastien Tixeuil; Xavier Urbain

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

Béatrice Bérard ¹ Pierre Courtieu ^{2, 3} Laure Millet ¹ Maria Potop-Butucaru ⁴ Lionel Rieg ⁵ Nathalie Sznajder ¹ 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

Domain :

Computer Science [cs] / Distributed, Parallel, and Cluster Computing [cs.DC]

Computer Science [cs] / Data Structures and Algorithms [cs.DS]

Computer Science [cs] / Embedded Systems

Computer Science [cs] / Ubiquitous Computing

Computer Science [cs] / Mobile Computing

Computer Science [cs] / Networking and Internet Architecture [cs.NI]

Computer Science [cs] / Formal Languages and Automata Theory [cs.FL]

Computer Science [cs] / Robotics [cs.RO]

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 : Tuesday, May 14, 2019 - 10:16:49 AM

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

Identifiers

Collections

Citation

Export

Metrics

764

Contact

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

Identifiers

Collections

Citation

Export

Share

Metrics

764

Contact