License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.OPODIS.2017.12
URN: urn:nbn:de:0030-drops-86324
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/8632/
Go to the corresponding LIPIcs Volume Portal

Doan, Ha Thi Thu ; Bonnet, François ; Ogata, Kazuhiro

Model Checking of Robot Gathering

pdf-format:
LIPIcs-OPODIS-2017-12.pdf (0.6 MB)

Abstract

Recent advances in distributed computing highlight models and algorithms for autonomous mo- bile robots that self-organize and cooperate together in order to solve a global objective. As results, a large number of algorithms have been proposed. These algorithms are given together with proofs to assess their correctness. However, those proofs are informal, which are error prone. This paper presents our study on formal verification of mobile robot algorithms. We first propose a formal model for mobile robot algorithms on anonymous ring shape network under multiplicity and asynchrony assumptions. We specify this formal model in Maude, a specification and pro- gramming language based on rewriting logic. We then use its model checker to formally verify an algorithm for robot gathering problem on ring enjoys some desired properties. As the result of the model checking, counterexamples have been found. We detect the sources of some unforeseen design errors. We, furthermore, give our interpretations of these errors.

BibTeX - Entry

@InProceedings{doan_et_al:LIPIcs:2018:8632,
  author =	{Ha Thi Thu Doan and Fran{\c{c}}ois Bonnet and Kazuhiro Ogata},
  title =	{{Model Checking of Robot Gathering}},
  booktitle =	{21st International Conference on Principles of Distributed Systems (OPODIS 2017)},
  pages =	{12:1--12:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-061-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{95},
  editor =	{James Aspnes and Alysson Bessani and Pascal Felber and Jo{\~a}o Leit{\~a}o},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/8632},
  URN =		{urn:nbn:de:0030-drops-86324},
  doi =		{10.4230/LIPIcs.OPODIS.2017.12},
  annote =	{Keywords: Mobile Robot, Robot Gathering, Formal Verification, Model Checking, Maude}
}

Keywords: Mobile Robot, Robot Gathering, Formal Verification, Model Checking, Maude
Collection: 21st International Conference on Principles of Distributed Systems (OPODIS 2017)
Issue Date: 2018
Date of publication: 28.03.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI