 |
Journal articles
[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
Béatrice Bérard 1
Author
Pierre Courtieu 2, 3
Author IdHAL : pierre-courtieu ORCID : https://orcid.org/0000-0001-8789-9781
Laure Millet 1
Author IdHAL : lmillet
Maria Potop-Butucaru 4
Author
Lionel Rieg 5
Author IdHAL : lionel-rieg
Nathalie Sznajder 1
Author IdHAL : sznajder-nathalie
Sébastien Tixeuil 6, 4, 7
Author IdHAL : tixeuil ORCID : https://orcid.org/0000-0002-0948-7172
Xavier Urbain 8, 9
Author IdHAL : xavier-urbain
1
MoVe - Modélisation et Vérification (France)
- LIP6 - Laboratoire d'Informatique de Paris 6 (4 Place JUSSIEU 75252 PARIS CEDEX 05 - France)
- UPMC - Université Pierre et Marie Curie - Paris 6 (4 place Jussieu - 75005 Paris - France)
- CNRS - Centre National de la Recherche Scientifique : UMR7606 (France)
2
GALLIUM - Programming languages, types, compilation and proofs (France)
- Inria Paris-Rocquencourt (INRIA Rocquencourt : Domaine de Voluceau, Rocquencourt B.P. 105 78153 le Chesnay Cedex - France)
- Inria - Institut National de Recherche en Informatique et en Automatique (Domaine de Voluceau Rocquencourt - BP 105 78153 Le Chesnay Cedex - France)
3
CEDRIC - Centre d'études et de recherche en informatique et communications (292 rue Saint-Martin
75141 PARIS Cedex 03
Case courrier 2D4P30 - France)
- ENSIIE - Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise : EA4629 (France)
- CNAM - Conservatoire National des Arts et Métiers [CNAM] : EA4629 (France)
4
NPA - Networks and Performance Analysis (France)
- LIP6 - Laboratoire d'Informatique de Paris 6 (4 Place JUSSIEU 75252 PARIS CEDEX 05 - France)
- UPMC - Université Pierre et Marie Curie - Paris 6 (4 place Jussieu - 75005 Paris - France)
- CNRS - Centre National de la Recherche Scientifique : UMR7606 (France)
5
CdF (institution) - Collège de France (France)
6
LINCS - Laboratory of Information, Network and Communication Sciences (23 avenue d'Italie 75013 Paris - France)
- UPMC - Université Pierre et Marie Curie - Paris 6 (4 place Jussieu - 75005 Paris - France)
- Inria - Institut National de Recherche en Informatique et en Automatique (Domaine de Voluceau Rocquencourt - BP 105 78153 Le Chesnay Cedex - France)
- IMT - Institut Mines-Télécom [Paris] (37-39 Rue Dareau, 75014 Paris - France)
7
IUF - Institut Universitaire de France (Maison des Universités 103 Boulevard Saint-Michel 75005 Paris - France)
- M.E.N.E.S.R. - Ministère de l'Education nationale, de l’Enseignement supérieur et de la Recherche (1 rue Descartes - 75231 Paris cedex 05 - France)
9
LRI - Laboratoire de Recherche en Informatique (LRI - Bâtiments 650-660 Université Paris-Sud 91405 Orsay Cedex - France)
- UP11 - Université Paris-Sud - Paris 11 (Bâtiment 300 - 91405 Orsay cedex - France)
- CentraleSupélec (3, rue Joliot Curie, Plateau de Moulon, 91192 GIF-SUR-YVETTE Cedex - France)
- CNRS - Centre National de la Recherche Scientifique : UMR8623 (France)
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 :
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 : Friday, January 8, 2021 - 5:38:07 PM
Contributor : Sébastien Tixeuil <>
Submitted on : Monday, December 7, 2015 - 10:29:54 AM
Last modification on : Friday, January 8, 2021 - 5:38:07 PM
Identifiers
- HAL Id : hal-01238784, version 1
Collections
UPMC | CNRS | CNAM | INSTITUT-TELECOM | CDF | UMR8623 | LIP6 | INRIA | LRI-VALS | CENTRALESUPELEC | UNIV-HESAM | SORBONNE-UNIVERSITE | CEDRIC-CNAM | SU-SCIENCES | PSL
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⟩
Metrics
Record views