Formal verification of mobile robot protocols

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, in the case of asynchronous execution models, are both cumbersome and error-prone. Our contribution is twofold. We first propose a formal model to describe mobile robot protocols operating in a discrete space i.e., with a finite set of possible robot positions, under synchrony and asynchrony assumptions. We translate this formal model into the DVE language, which is the input format of the model-checkers DiVinE and ITS tools, and formally prove the equivalence of the two models. We then verify several instances of two existing protocols for variants of the ring exploration in an asynchronous setting: exploration with stop and perpetual exclusive exploration. For the first protocol we refine the correctness bounds and for the second one, we exhibit a counter-example. This protocol is then modified and we establish the correctness of the new version with an inductive proof.
Type de document :
Article dans une revue
Distributed Computing, Springer Verlag, 2016, 29 (6), pp.459-487. 〈http://link.springer.com/article/10.1007/s00446-016-0271-1〉. 〈10.1007/s00446-016-0271-1〉
Liste complète des métadonnées

Littérature citée [47 références]  Voir  Masquer  Télécharger

https://hal.sorbonne-universite.fr/hal-01344903
Contributeur : Yann Thierry-Mieg <>
Soumis le : mercredi 13 décembre 2017 - 14:35:09
Dernière modification le : jeudi 13 décembre 2018 - 01:33:04

Fichier

TCS16.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Beatrice Bérard, Pascal Lafourcade, Laure Millet, Maria Potop-Butucaru, Yann Thierry-Mieg, et al.. Formal verification of mobile robot protocols. Distributed Computing, Springer Verlag, 2016, 29 (6), pp.459-487. 〈http://link.springer.com/article/10.1007/s00446-016-0271-1〉. 〈10.1007/s00446-016-0271-1〉. 〈hal-01344903〉

Partager

Métriques

Consultations de la notice

395

Téléchargements de fichiers

63