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.


    Zugriff

    Download


    Exportieren, teilen und zitieren



    Titel :

    Model Checking of Robot Gathering


    Beteiligte:

    Erscheinungsdatum :

    2018-01-01



    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    Klassifikation :

    DDC:    004 / 629




    Dirt cleaning robot with intelligent material gathering manipulator

    HONG SHENGRONG / CHEN QICHUN / CHEN RENLIANG et al. | Europäisches Patentamt | 2022

    Freier Zugriff

    CNut Gathering Robot. Design, Implementation and Mathematical Characterization

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


    CNut Gathering Robot. Design, Implementation and Mathematical Characterization

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


    Requirement Gathering Problems: Environmental Issues in Robot Development

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

    Freier Zugriff

    Wireless vehicle-to-infrastructure data gathering for robot platooning

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

    Freier Zugriff