article

Formal verification of mobile robot protocols

Authors:

Béatrice Bérard,

Pascal Lafourcade,

Maria Potop-Butucaru,

Yann Thierry-Mieg,

Sébastien TixeuilAuthors Info & Claims

Distributed Computing, Volume 29, Issue 6

Pages 459 - 487

https://doi.org/10.1007/s00446-016-0271-1

Published: 01 November 2016 Publication History

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.

References

[1]

Flocchini, P., Prencipe, G., Santoro, N.: Distributed Computing by Oblivious Mobile Robots. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, San Rafael, California (2012)

Digital Library

[2]

Almeida, A., Ramalho, G., Santana, H., Azevedo Tedesco, P., Menezes, T., Corruble, V., Chevaleyre, Y.: Recent advances on multi-agent patrolling. In: 17th Brazilian Symposium on Artificial Intelligence Advances in Artificial Intelligence--SBIA 2004, São Luis, Maranhão, Brazil, 29 Sept---1 Oct 2004, Proceedings, pp. 474---483 (2004)

[3]

Flocchini, P., Ilcinkas, D., Pelc, A., Santoro, N.: Computing without communicating: ring exploration by asynchronous oblivious robots. Algorithmica 65(3), 562---583 (2013)

Digital Library

[4]

Blin, L., Milani, A., Potop-Butucaru, M., Tixeuil, S.: Exclusive perpetual ring exploration without chirality. In: Proceedings of 24th International Symposium in Distributed Computing (DISC'10), vol. 6343 of LNCS, pp. 312---327. Springer (2010)

Digital Library

[5]

Suzuki, I., Yamashita, M.: Distributed anonymous mobile robots: formation of geometric patterns. SIAM J. Comput. 28(4), 1347---1363 (1999)

Digital Library

[6]

Clerentin, A., Delafosse, M., Delahoche, L., Marhic, B., Jolly-Desodt, A.: Uncertainty and imprecision modeling for the mobile robot localization problem. Auton. Robots 24(3), 267---283 (2008)

Digital Library

[7]

D'Angelo, G., Di Stefano, G., Navarra, A.: Gathering of six robots on anonymous symmetric rings. In: Proceedings of 18th International Colloquium on Structural Information and Communication Complexity (SIROCCO'11), volume 6796 of LNCS, pp. 174---185. Springer (2011)

Digital Library

[8]

Kamei, S., Lamani, A., Ooshita, F., Tixeuil, S.: Asynchronous mobile robot gathering from symmetric configurations without global multiplicity detection. In: Proceedings of 18th International Colloquium on Structural Information and Communication Complexity (SIROCCO'11), vol. 6796 of LNCS, pp. 150---161. Springer (2011)

Digital Library

[9]

Lamani, A., Kamei, S., Ooshita, F., Tixeuil, S.: Gathering an even number of robots in an odd ring without global multiplicity detection. In: Proceedings of International Conference on Mathematical Foundations of Computer Science (MFCS'12), vol. 7464 of LNCS, pp. 542---553. Springer (2012)

Digital Library

[10]

Flocchini, P., Prencipe, G., Santoro, N., Widmayer, P.: Gathering of asynchronous robots with limited visibility. Theor. Comput. Sci. 337(1---3), 147---168 (2005)

Digital Library

[11]

Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2001)

[12]

Baier, C., Katoen, J .P.: Principles of Model Checking. MIT Press, Cambridge (2008)

Digital Library

[13]

Lamport, L., Merz, S.: Specifying and verifying fault-tolerant systems. In: Proceedings of Third International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'94), organized jointly with the Working Group Provably Correct Systems--ProCoS, vol. 863 of LNCS, pp. 41---76. Springer (1994)

Digital Library

[14]

Kulkarni, S.S., Bonakdarpour, B., Ebnenasir, A.: Mechanical verification of automatic synthesis of fault-tolerant programs. In: Proceedings of 14th International Symposium on Logic Based Program Synthesis and Transformation (LOPSTR' 04), vol. 3573 of LNCS, pp. 36---52. Springer (2004)

Digital Library

[15]

Guerraoui, R., Henzinger, T.A., Singh, V.: Model checking transactional memories. Distrib. Comput. 22(3), 129---145 (2010)

Digital Library

[16]

Chatzigiannakis, I., Michail, O., Spirakis, P.G.: Algorithmic verification of population protocols. In: Proceedings of 12th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS'10), vol. 6366 of LNCS, pp. 221---235. Springer (2010)

Digital Library

[17]

Clément, J., Delporte-Gallet, C., Fauconnier, H., Sighireanu, M.: Guidelines for the verification of population protocols. In: Proceedings of 31st International Conference on Distributed Computing Systems (ICDCS'11), pp. 215---224. IEEE (2011)

Digital Library

[18]

Charron-Bost, B., Debrat, H., Merz, S.: Formal verification of consensus algorithms tolerating malicious faults. In: Proceedings of 13th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS'11), vol. 6976 of LNCS, pp. 120---134. Springer (2011)

Digital Library

[19]

Lu, T., Merz, S., Weidenbach, C.: Towards verification of the pastry protocol using TLA$$^{{+}}$$+. In: Proceedings of Joint 13t International Conference (FMOODS'11) 2011, and 31st International Conference (FORTE'11) on Formal Techniques for Distributed Systems, volume 6722 of LNCS, pp. 244---258. Springer (2011)

Digital Library

[20]

Tsuchiya, T., Schiper, A.: Verification of consensus algorithms using satisfiability solving. Distrib. Comput. 23, 341---358 (2011)

Digital Library

[21]

Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307---309 (1986)

Digital Library

[22]

Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: 14th Annual Symposium on Logic in Computer Science, pp. 352---359. IEEE (1999)

Digital Library

[23]

Suzuki, I.: Proving properties of a ring of finite-state machines. Inf. Process. Lett. 28(4), 213---214 (1988)

Digital Library

[24]

Aminof, B., Kotek, T., Rubin, S., Spegni, F., Veith, H.: Parameterized model checking of rendezvous systems. In: Paolo, B., Daniele, G. (eds.) CONCUR 2014 Concurrency Theory, vol. 8704 of Lecture Notes in Computer Science, pp. 109---124. Springer, Berlin (2014)

[25]

Allen Emerson, E., Namjoshi, K.S.: Reasoning about rings. In: Proceedings of the 22Nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '95, pp. 85---94. ACM, New York (1995)

Digital Library

[26]

Manna, Z., Pnueli, A.: Temporal verification diagrams. In: Proceedings of International Conference on Theoretical Aspects of Computer Software (TACS'94), vol. 789 of LNCS, pp. 726---765. Springer (1994)

Digital Library

[27]

Clarke, E.M., Grumberg, O., Jha, S.: Veryfying parameterized networks using abstraction and regular languages. In: Proceedings of 6th International Conference on Concurrency Theory (CONCUR'95), vol. 962 of LNCS, pp. 395---407. Springer (1995)

Digital Library

[28]

BjØrner, N., Browne, A., Chang, E.Y., Colón, M., Kapur, A., Manna, Z., Sipma, H., Uribe, T.E.: Step: deductive-algorithmic verification of reactive and real-time systems. In: Proceedings of 8th International Conference on Computer Aided Verification (CAV'96), vol. 1102 of LNCS, pp. 415---418. Springer (1996)

Digital Library

[29]

de Alfaro, L., Manna, Z., Sipma, H.B., Uribe, T.E.: Visual verification of reactive systems. In: Proceedings of 3rd International Workshop on Tools and Algorithms for Construction and Analysis of Systems (TACAS'97), vol. 1217 of LNCS, pp. 334---350. Springer (1997)

Digital Library

[30]

Cansell, D., Méry, D., Merz, S.: Diagram refinements for the design of reactive systems. J. Univ. Comput. Sci. 7(2), 159---174 (2001)

[31]

Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.D.: Parameterized verification with automatically computed inductive assertions. In: Proceedings of 13th International Conference on Computer Aided Verification (CAV'01), vol. 2102 of LNCS, pp. 221---234. Springer (2001)

Digital Library

[32]

Gmeiner, A., Konnov, I., Schmid, U., Veith, H., Widder J.: Tutorial on parameterized model checking of fault-tolerant distributed algorithms. In Marco, B., Ferruccio, D., Reiner, H., EinarBroch, J., Ina S. (eds.) Formal Methods for Executable Software Models, vol. 8483 of Lecture Notes in Computer Science, pp. 122---171. Springer International Publishing (2014)

Digital Library

[33]

Devismes, S., Lamani, A., Petit, F., Raymond, P., Tixeuil, S.: Optimal grid exploration by asynchronous oblivious robots. In: Proceedings of 14th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS'12), vol. 7596 of LNCS, pp. 64---76. Springer (2012)

Digital Library

[34]

Bonnet, F., Défago, X., Petit, F., Potop-Butucaru, M., Tixeuil, S.: Brief announcement: discovering and assessing fine-grained metrics in robot networks protocols. In: Proceedings of 14th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS'12), vol. 7596 of LNCS, pp. 282---284. Springer (2012)

Digital Library

[35]

Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous dataflow programming language Lustre. Proc. IEEE 79(9), 1305---1320 (1991)

[36]

Barnat, J., Brim, L., Havel, V., Havlícek, J., Kriho, J., Lenco, M., Rockai, P., Still, V., Weiser, J.: Divine 3.0--an explicit-state model checker for multithreaded C & C$$++$$++ programs. In: Proceedings of 25th International Conference on Computer Aided Verification (CAV'13), vol. 8044 of LNCS, pp. 863---868. Springer (2013)

[37]

Colange, M., Baarir, S., Kordon, F., Thierry-Mieg, Y.: Towards distributed software model-checking using decision diagrams. In: Proceedings of 25th International Conference on Computer Aided Verification (CAV'13), vol. 8044 of LNCS, pp. 830---845. Springer (2013)

[38]

Behrmann, G., Cougnard, A., David, A., Fleury, E., Guldstrand Larsen, K., Lime, D.: Uppaal-tiga: time for playing games! In: 19th International Conference on Computer Aided Verification, CAV'07, vol. 4590 of Lecture Notes in Computer Science, pp. 121---125. Springer (2007)

Digital Library

[39]

Barnat, J., Brim, L., Češka, M., Roă¿kai, P.: DiVinE: parallel distributed model checker (tool paper). In: Sharygina, N., Veith, H. (eds.) Parallel and Distributed Methods in Verification and High Performance Computational Systems Biology, pp. 4---7. IEEE (2010)

Digital Library

[40]

Holzmann, G .J.: The SPIN Model Checker--Primer and Reference Manual, 1st edn. Addison-Wesley, Reading (2004)

Digital Library

[41]

Blom, S., van de Pol, J., Weber, M.: Ltsmin: Distributed andsymbolic reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) Computer Aided Verification, vol. 6174 of Lecture Notes in Computer Science, pp. 354---359. Springer, Berlin (2010)

Digital Library

[42]

Bérard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P.: Systems and Software Verification: Model-Checking Techniques and Tools, 1st edn. Springer Publishing Company Incorporated, Berlin (2010)

Digital Library

[43]

Harrison, M.A.: Introduction to Formal Language Theory, 1st edn. Addison-Wesley Longman Publishing Co. Inc, Boston (1978)

Digital Library

[44]

Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Uppaal--a tool suite for automatic verification of real-time systems. In: Proceedings of Workshop on Verification and Control of Hybrid Systems III, Number 1066 in Lecture Notes in Computer Science, pp. 232---243. Springer (1995)

Digital Library

[45]

Millet, L., Potop-Butucaru, M., Sznajder, N., Tixeuil, S.: On the synthesis of mobile robots algorithms: the case of ring gathering. In: Proceedings of 16th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS'14), vol. 8756 of Lecture Notes in Computer Science, pp. 237---251. Springer (2014)

[46]

Ramadge, W.M., Wonham, P.J.: Supervisory control of a class of discrete event processes. In: Proceedings of 6th International Conference on Analysis and Optimization of Systems, vol. 63 of LNCS. Springer (1984)

Cited By

Raju DBakirtzis GTopcu UAgmon NAn BRicci AYeoh W(2023)Memoryless Adversaries in Imperfect Information GamesProceedings of the 2023 International Conference on Autonomous Agents and Multiagent Systems10.5555/3545946.3598940(2379-2381)Online publication date: 30-May-2023
https://dl.acm.org/doi/10.5555/3545946.3598940
Défago XHeriban ATixeuil SWada K(2023)Using model checking to formally verify rendezvous algorithms for robots with lights in Euclidean spaceRobotics and Autonomous Systems10.1016/j.robot.2023.104378163:COnline publication date: 1-May-2023
https://dl.acm.org/doi/10.1016/j.robot.2023.104378
Balabonski TCourtieu PPelle RRieg LTixeuil SUrbain X(2021)Computer Aided Formal Design of Swarm Robotics AlgorithmsStabilization, Safety, and Security of Distributed Systems10.1007/978-3-030-91081-5_31(469-473)Online publication date: 17-Nov-2021
https://dl.acm.org/doi/10.1007/978-3-030-91081-5_31
Show More Cited By

Index Terms

Formal verification of mobile robot protocols
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking

Recommendations

Formal verification of ASMs using MDGs

We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Coverage metrics for formal verification

In formal verification, we verify that a system is correct with respect to a specification. Even when the system is proven to be correct, there is still a question of how complete the specification is and whether it really covers all the behaviors of ...
Formal Verification for C Program

Iterative abstraction refinement has emerged in the last few years as the leading approach to software model checking. We present an approach for automatically verifying C programs against safety specifications based on finite state machine. The ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Distributed Computing

Distributed Computing Volume 29, Issue 6

November 2016

78 pages

ISSN:0178-2770

Issue’s Table of Contents

Copyright © Copyright © 2016 Springer-Verlag Berlin Heidelberg.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 November 2016

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

14
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Raju DBakirtzis GTopcu UAgmon NAn BRicci AYeoh W(2023)Memoryless Adversaries in Imperfect Information GamesProceedings of the 2023 International Conference on Autonomous Agents and Multiagent Systems10.5555/3545946.3598940(2379-2381)Online publication date: 30-May-2023
https://dl.acm.org/doi/10.5555/3545946.3598940
Défago XHeriban ATixeuil SWada K(2023)Using model checking to formally verify rendezvous algorithms for robots with lights in Euclidean spaceRobotics and Autonomous Systems10.1016/j.robot.2023.104378163:COnline publication date: 1-May-2023
https://dl.acm.org/doi/10.1016/j.robot.2023.104378
Balabonski TCourtieu PPelle RRieg LTixeuil SUrbain X(2021)Computer Aided Formal Design of Swarm Robotics AlgorithmsStabilization, Safety, and Security of Distributed Systems10.1007/978-3-030-91081-5_31(469-473)Online publication date: 17-Nov-2021
https://dl.acm.org/doi/10.1007/978-3-030-91081-5_31
Amoussou-Guenou YBaarir SPotop-Butucaru MSznajder NTible LTixeuil S(2020)On the Encoding and Solving of Partial Information GamesNetworked Systems10.1007/978-3-030-67087-0_5(60-76)Online publication date: 3-Jun-2020
https://dl.acm.org/doi/10.1007/978-3-030-67087-0_5
Sangnier ASznajder NPotop-Butucaru MTixeuil S(2019)Parameterized verification of algorithms for oblivious robots on a ringFormal Methods in System Design10.1007/s10703-019-00335-y56:1-3(55-89)Online publication date: 30-Jul-2019
https://dl.acm.org/doi/10.1007/s10703-019-00335-y
Cicerone SDi Stefano GNavarra A(2019)Embedded pattern formation by asynchronous robots without chiralityDistributed Computing10.1007/s00446-018-0333-732:4(291-315)Online publication date: 2-Aug-2019
https://dl.acm.org/doi/10.1007/s00446-018-0333-7
Cicerone SDi Stefano GNavarra A(2019)Asynchronous Arbitrary Pattern FormationDistributed Computing10.1007/s00446-018-0325-732:2(91-132)Online publication date: 15-May-2019
https://dl.acm.org/doi/10.1007/s00446-018-0325-7
Balabonski TDelga ARieg LTixeuil SUrbain X(2019)Synchronous Gathering without Multiplicity DetectionTheory of Computing Systems10.1007/s00224-017-9828-z63:2(200-218)Online publication date: 15-May-2019
https://dl.acm.org/doi/10.1007/s00224-017-9828-z
Balabonski TCourtieu PPelle RRieg LTixeuil SUrbain X(2019)Continuous vs. Discrete Asynchronous Moves: A Certified Approach for Mobile RobotsNetworked Systems10.1007/978-3-030-31277-0_7(93-109)Online publication date: 19-Jun-2019
https://dl.acm.org/doi/10.1007/978-3-030-31277-0_7
Altisen KCorbineau PDevismes S(2019)Squeezing Streams and Composition of Self-stabilizing AlgorithmsFormal Techniques for Distributed Objects, Components, and Systems10.1007/978-3-030-21759-4_2(21-38)Online publication date: 17-Jun-2019
https://dl.acm.org/doi/10.1007/978-3-030-21759-4_2
Show More Cited By

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents