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.


    Access

    Download


    Export, share and cite



    Title :

    Model Checking of Robot Gathering


    Contributors:

    Publication date :

    2018-01-01



    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English



    Classification :

    DDC:    004 / 629




    Dirt cleaning robot with intelligent material gathering manipulator

    HONG SHENGRONG / CHEN QICHUN / CHEN RENLIANG et al. | European Patent Office | 2022

    Free access

    CNut Gathering Robot. Design, Implementation and Mathematical Characterization

    Villalpando-Hernandez, Rafaela / Vargas-Rosales, Cesar / Diaz-M., Rene et al. | TIBKAT | 2020


    CNut Gathering Robot. Design, Implementation and Mathematical Characterization

    Villalpando-Hernandez, Rafaela / Vargas-Rosales, Cesar / Diaz-M., Rene et al. | Springer Verlag | 2020


    Requirement Gathering Problems: Environmental Issues in Robot Development

    Arif, Muhammad / Ali, Zunaira Shafqat / Arooj, Samman | BASE | 2019

    Free access

    Wireless vehicle-to-infrastructure data gathering for robot platooning

    Caruntu, Constantin F. / Copot, Cosmin / Lazar, Corneliu | BASE | 2017

    Free access