More Web Proxy on the site http://driver.im/

Article

Computer Aided Formal Design of Swarm Robotics Algorithms

Authors:

Thibaut Balabonski,

Pierre Courtieu,

Sébastien Tixeuil,

Xavier UrbainAuthors Info & Claims

Stabilization, Safety, and Security of Distributed Systems: 23rd International Symposium, SSS 2021, Virtual Event, November 17–20, 2021, Proceedings

Pages 469 - 473

https://doi.org/10.1007/978-3-030-91081-5_31

Published: 17 November 2021 Publication History

Abstract

Previous works on formally studying mobile robotic swarms consider necessary and sufficient system hypotheses enabling to solve theoretical benchmark problems (geometric pattern formation, gathering, scattering, etc.). We argue that formal methods can also help in the early design stage of mobile robotic swarms correct-by-design protocols, even for tasks closer to real-world use cases and not previously studied theoretically. Our position is supported by a concrete case study. Starting from a real-world case scenario, we jointly design the formal problem specification, a family of protocols that are able to solve the problem, and their corresponding proof of correctness, all expressed with the same formal framework. The concrete framework we use for our development is the Pactole library based on the Coq proof assistant.

References

[1]

Altisen K, Corbineau P, and Devismes S Albert E and Lanese I A framework for certified self-stabilization Formal Techniques for Distributed Objects, Components, and Systems 2016 Cham Springer 36-51

Digital Library

[2]

Auger C, Bouzid Z, Courtieu P, Tixeuil S, and Urbain X Higashino T, Katayama Y, Masuzawa T, Potop-Butucaru M, and Yamashita M Certified impossibility results for Byzantine-tolerant mobile robots Stabilization, Safety, and Security of Distributed Systems 2013 Cham Springer 178-190

Digital Library

[3]

Balabonski T, Courtieu P, Pelle R, Rieg L, Tixeuil S, and Urbain X Atig MF and Schwarzmann AA Continuous vs. discrete asynchronous moves: a certified approach for mobile robots Networked Systems 2019 Cham Springer 93-109

Digital Library

[4]

Balabonski, T., Courtieu, P., Pelle, R., Rieg, L., Tixeuil, S., Urbain, X.: Computer aided formal design of swarm robotics algorithms. CoRR abs/2101.06966 (2021). https://arxiv.org/abs/2101.06966

[5]

Balabonski T, Delga A, Rieg L, Tixeuil S, and Urbain X Synchronous gathering without multiplicity detection: a certified algorithm Theory Comput. Syst. 2017 63 2 200-218

Digital Library

[6]

Balabonski, T., Pelle, R., Rieg, L., Tixeuil, S.: A foundational framework for certified impossibility results with mobile robots on graphs. In: Bellavista, P., Garg, V.K. (eds.) Proceedings of the 19th International Conference on Distributed Computing and Networking, ICDCN 2018, Varanasi, India, 4–7 January 2018, pp. 5:1–5:10. ACM (2018).

Digital Library

[7]

Bérard B, Lafourcade P, Millet L, Potop-Butucaru M, Thierry-Mieg Y, and Tixeuil S Formal verification of mobile robot protocols Distrib. Comput. 2016 29 6 459-487

Digital Library

[8]

Bezem M, Bol R, and Groote JF Formalizing process algebraic verifications in the calculus of constructions Formal Aspects Comput. 1997 9 1-48

Digital Library

[9]

Bonnet, F., Défago, X., Petit, F., Potop-Butucaru, M., Tixeuil, S.: Discovering and assessing fine-grained metrics in robot networks protocols. In: 33rd IEEE International Symposium on Reliable Distributed Systems Workshops, SRDS Workshops 2014, Nara, Japan, 6–9 October 2014, pp. 50–59. IEEE (2014).

Digital Library

[10]

Courtieu P, Rieg L, Tixeuil S, and Urbain X Impossibility of gathering, a certification Inf. Process. Lett. 2015 115 447-452

[11]

Courtieu P, Rieg L, Tixeuil S, and Urbain X Gavoille C and Ilcinkas D Certified universal gathering in

R^{2}

for oblivious mobile robots Distributed Computing 2016 Heidelberg Springer 187-200

[12]

Cousineau D, Doligez D, Lamport L, Merz S, Ricketts D, and Vanzetto H Giannakopoulou D and Méry D TLA

^{+}

Proofs FM 2012: Formal Methods 2012 Heidelberg Springer 147-154

[13]

Défago, X., Heriban, A., Tixeuil, S., Wada, K.: Using model checking to formally verify rendezvous algorithms for robots with lights in Euclidean space. In: International Symposium on Reliable Distributed Systems, SRDS 2020, Shanghai, China, 21–24 September 2020, pp. 113–122. IEEE (2020).

[14]

Deng, Y., Monin, J.F.: Verifying self-stabilizing population protocols with coq. In: Chin, W.N., Qin, S. (eds.) Third IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2009), Tianjin, China, pp. 201–208. IEEE Computer Society, July 2009

[15]

Devismes S, Lamani A, Petit F, Raymond P, and Tixeuil S Richa AW and Scheideler C Optimal grid exploration by asynchronous oblivious robots Stabilization, Safety, and Security of Distributed Systems 2012 Heidelberg Springer 64-76

Digital Library

[16]

Doan HTT, Bonnet F, and Ogata K Liu S, Duan Z, Tian C, and Nagoya F Model checking of a mobile robots perpetual exploration algorithm Structured Object-Oriented Formal Language and Method 2017 Cham Springer 201-219

Digital Library

[17]

Doan, H.T.T., Bonnet, F., Ogata, K.: Model checking of robot gathering. In: Aspnes, J., Bessani, A., Felber, P., Leitão, J. (eds.) 21st International Conference on Principles of Distributed Systems, OPODIS 2017, Lisbon, Portugal, 18–20 December 2017. LIPIcs, vol. 95, pp. 12:1–12:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017).

[18]

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

Digital Library

[19]

Fokkink W Modelling Distributed Systems 2007 Heidelberg Springer

[20]

Gaspar, N., Henrio, L., Madelaine, E.: Bringing coq into the world of GCM distributed applications, pp. 643–662 (2014)

[21]

Küfner P, Nestmann U, and Rickmann C Baeten JCM, Ball T, and de Boer FS Formal verification of distributed algorithms Theoretical Computer Science 2012 Heidelberg Springer 209-224

Digital Library

[22]

Lamport L The temporal logic of actions ACM Trans. Program. Lang. Syst. 1994 16 3 872-923

Digital Library

[23]

Millet L, Potop-Butucaru M, Sznajder N, and Tixeuil S Felber P and Garg V On the synthesis of mobile robots algorithms: the case of ring gathering Stabilization, Safety, and Security of Distributed Systems 2014 Cham Springer 237-251

[24]

Sangnier, A., Sznajder, N., Potop-Butucaru, M., Tixeuil, S.: Parameterized verification of algorithms for oblivious robots on a ring. Formal Methods Syst. Des. (6), 55–89 (2019).

Digital Library

[25]

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

Digital Library

Cited By

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

Recommendations

Formal Specification and Design Time Testing

It is shown how design time testing can be used in conjunction with formal specification. Emphasis is placed on the benefits of using an executable specification language OBJ, of having a design controlled by requirements specification, and of adherence ...
Formal Object-Oriented User-Interface Design
ASWEC '00: Proceedings of the 2000 Australian Software Engineering Conference

A notation is presented for formally describing the design of a user-interface. A specification of a system is given using the Object-Z formal specification language and then extended to describe presentation (user-interface design) using the User ...
A Formal Framework for ASTRAL Intralevel Proof Obligations

ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development, and therefore has been formally defined. This paper focuses on how to formally prove the mathematical correctness of ASTRAL ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

Stabilization, Safety, and Security of Distributed Systems: 23rd International Symposium, SSS 2021, Virtual Event, November 17–20, 2021, Proceedings

Nov 2021

536 pages

ISBN:978-3-030-91080-8

DOI:10.1007/978-3-030-91081-5

Editors:
Colette Johnen
University of Bordeaux, Bordeaux, France
,
Elad Michael Schiller
Chalmers University of Technology, Gothenburg, Sweden
,
Stefan Schmid
University of Vienna, Vienna, Austria

© Springer Nature Switzerland AG 2021.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 17 November 2021

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 03 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

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

View Options

View options

Figures

Tables

Media

View Table of Conten