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

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

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  », International Journal of Informatics Society, 2015, pp. 101-114. ISSN 1883-4566. 〈http://www.infsoc.org/journal/vol07/IJIS_07_3_101-114.pdf〉

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.

Voir la notice complète sur HAL

Actualités