Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Programming Multi-robot Systems with X-KLAIM

  • Conference paper
  • First Online:
Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning (ISoLA 2022)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 13703))

Included in the following conference series:

Abstract

Software development for robotics applications is still a major challenge that becomes even more complex when considering a Multi-Robot System (MRS). Such a distributed software has to perform multiple cooperating tasks in a well-coordinated manner to avoid unsatisfactory emerging behavior. This paper provides an approach for programming MRSs at a high abstraction level using the programming language X-Klaim. The computation and communication model of X-Klaim, based on multiple distributed tuple spaces, permits to coordinate with the same abstractions and mechanisms both intra- and inter-robot interactions of an MRS. This allows developers to focus on MRS behavior, achieving readable and maintainable code. The proposed approach can be used in practice through the integration of X-Klaim and the popular robotics framework ROS. We show the proposal’s feasibility and effectiveness by implementing an MRS scenario.

This work was partially supported by the PRIN projects “SEDUCE” n. 2017TWRCNB and “T-LADIES” n. 2020TL3X8X, and the INdAM - GNCS Project “Proprietà qualitative e quantitative di sistemi reversibili” n. CUP_E55F2200027001.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 59.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 79.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    https://github.com/LorenzoBettini/xklaim.

  2. 2.

    https://www.ros.org/.

  3. 3.

    https://github.com/h2r/java_rosbridge.

  4. 4.

    Jetty 9: https://www.eclipse.org/jetty/.

  5. 5.

    https://gazebosim.org/.

  6. 6.

    The complete source code of the scenario implementation, and a screencast showing its execution on Gazebo, can be found at https://github.com/LorenzoBettini/xklaim-ros-multi-robot-warehouse-example.

References

  1. Adam, S., Larsen, M., Jensen, K., Schultz, U.P.: Rule-based dynamic safety monitoring for mobile robots. J. Softw. Eng. Rob. 7(1), 121–141 (2016)

    Google Scholar 

  2. Adam, S., Schultz, U.P.: Towards interactive, incremental programming of ROS nodes. In: Workshop on Domain-Specific Languages and models for Robotic systems (2014)

    Google Scholar 

  3. Alonso, D., et al.: V\(^3\)CMM: a 3-view component meta-model for model-driven robotic software development. J. Softw. Eng. Rob. 1, 3–17 (2010)

    Google Scholar 

  4. Bettini, L., De Nicola, R., Pugliese, R.: Klava: a Java package for distributed and mobile applications. Softw. Pract. Exp. 32(14), 1365–1394 (2002)

    Article  Google Scholar 

  5. Bettini, L., Bourr, K., Pugliese, R., Tiezzi, F.: Writing robotics applications with X-Klaim. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12477, pp. 361–379. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-61470-6_22

    Chapter  Google Scholar 

  6. Bettini, L., Loreti, M., Pugliese, R.: An infrastructure language for open nets. In: SAC, pp. 373–377. ACM (2002)

    Google Scholar 

  7. Bettini, L., Merelli, E., Tiezzi, F.: X-Klaim is back. In: Boreale, M., Corradini, F., Loreti, M., Pugliese, R. (eds.) Models, Languages, and Tools for Concurrent and Distributed Programming. LNCS, vol. 11665, pp. 115–135. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-21485-2_8

    Chapter  Google Scholar 

  8. Brugali, D., Gherardi, L.: HyperFlex: a model driven toolchain for designing and configuring software control systems for autonomous robots. In: Koubaa, A. (ed.) Robot Operating System (ROS). SCI, vol. 625, pp. 509–534. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-26054-9_20

    Chapter  Google Scholar 

  9. Bruyninckx, H., et al.: The BRICS component model: a model-based development paradigm for complex robotics software systems. In: SAC, pp. 1758–1764. ACM (2013)

    Google Scholar 

  10. Bubeck, A., et al.: BRIDE - a toolchain for framework-independent development of industrial service robot applications. In: ISR, pp. 137–142. VDE (2014)

    Google Scholar 

  11. Casalaro, G.L.: Model-driven engineering for mobile robotic systems: a systematic mapping study. Softw. Syst. Model. (2021). https://doi.org/10.1007/s10270-021-00908-8

  12. Ciccozzi, F., et al.: Adopting MDE for specifying and executing civilian missions of mobile multi-robot systems. IEEE Access 4, 6451–6466 (2016)

    Article  Google Scholar 

  13. de Araújo Silva, E., Valentin, E., Carvalho, J.R.H., da Silva Barreto, R.: A survey of model driven engineering in robotics. Comput. Lang. 62, 101021 (2021)

    Google Scholar 

  14. De Nicola, R., Di Stefano, L., Inverso, O.: Toward formal models and languages for verifiable multi-robot systems. Front. Rob. AI 5, 94 (2018)

    Article  Google Scholar 

  15. De Nicola, R., Ferrari, G.L., Pugliese, R.: KLAIM: a kernel language for agents interaction and mobility. IEEE Trans. Softw. Eng. 24(5), 315–330 (1998)

    Article  Google Scholar 

  16. De Nicola, R., Ferrari, G.L., Pugliese, R., Venneri, B.: Types for access control. Theor. Comput. Sci. 240(1), 215–254 (2000)

    Article  MathSciNet  Google Scholar 

  17. De Nicola, R., Gorla, D., Pugliese, R.: Confining data and processes in global computing applications. Sci. Comput. Program. 63(1), 57–87 (2006)

    Article  MathSciNet  Google Scholar 

  18. De Nicola, R., Gorla, D., Pugliese, R.: Basic observables for a calculus for global computing. Inf. Comput. 205(10), 1491–1525 (2007)

    Article  MathSciNet  Google Scholar 

  19. De Nicola, R., Katoen, J., Latella, D., Loreti, M., Massink, M.: Model checking mobile stochastic logic. Theor. Comput. Sci. 382(1), 42–70 (2007)

    Article  MathSciNet  Google Scholar 

  20. De Nicola, R., Loreti, M.: A modal logic for mobile agents. ACM Trans. Comput. Log. 5(1), 79–128 (2004)

    Article  MathSciNet  Google Scholar 

  21. De Nicola, R., Loreti, M., Pugliese, R., Tiezzi, F.: A formal approach to autonomic systems programming: the SCEL language. ACM Trans. Auton. Adapt. Syst. 9(2), 1–29 (2014)

    Article  Google Scholar 

  22. De Nicola, R., et al.: From flow logic to static type systems for coordination languages. Sci. Comput. Program. 75(6), 376–397 (2010)

    Article  MathSciNet  Google Scholar 

  23. Desai, A., Saha, I., Yang, J., Qadeer, S., Seshia, S.A.: Drona: a framework for safe distributed mobile robotics. In: 8th Internnational Conference on Cyber-Physical Systems, pp. 239–248 (2017)

    Google Scholar 

  24. Dhouib, S., Kchir, S., Stinckwich, S., Ziadi, T., Ziane, M.: RobotML, a domain-specific language to design, simulate and deploy robotic applications. In: Noda, I., Ando, N., Brugali, D., Kuffner, J.J. (eds.) SIMPAR 2012. LNCS (LNAI), vol. 7628, pp. 149–160. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-34327-8_16

    Chapter  Google Scholar 

  25. Doriya, R., Mishra, S., Gupta, S.: A brief survey and analysis of multi-robot communication and coordination. In: International Conference on Computing, Communication, Automation, pp. 1014–1021 (2015)

    Google Scholar 

  26. Dragule, S., Meyers, B., Pelliccione, P.: A generated property specification language for resilient multirobot missions. In: Romanovsky, A., Troubitsyna, E.A. (eds.) SERENE 2017. LNCS, vol. 10479, pp. 45–61. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-65948-0_4

    Chapter  Google Scholar 

  27. Eckhardt, J., Mühlbauer, T., Meseguer, J., Wirsing, M.: Semantics, distributed implementation, and formal analysis of KLAIM models in Maude. Sci. Comput. Program. 99, 24–74 (2015)

    Article  Google Scholar 

  28. Estévez, E., et al.: ART2ool: a model-driven framework to generate target code for robot handling tasks. Adv. Manuf. Technol. 97(1–4), 1195–1207 (2018)

    Article  Google Scholar 

  29. Farinelli, A., Iocchi, L., Nardi, D.: Multirobot systems: a classification focused on coordination. IEEE Trans. Syst. Man Cybern. Part B (Cybern.) 34(5), 2015–2028 (2004)

    Article  Google Scholar 

  30. Figat, M., Zieliński, C.: Robotic system specification methodology based on hierarchical Petri nets. IEEE Access 8, 71617–71627 (2020)

    Article  Google Scholar 

  31. Frigerio, M., Buchli, J., Caldwell, D.G.: A domain specific language for kinematic models and fast implementations of robot dynamics algorithms. In: Proceedings of DSLRob 2011. CoRR, vol. abs/1301.7190 (2013)

    Google Scholar 

  32. García, S., et al.: High-level mission specification for multiple robots. In: 12th ACM SIGPLAN International Conference on Software Language Engineering, p. 127–140 (2019)

    Google Scholar 

  33. Gelernter, D.: Generative communication in linda. ACM Trans. Program. Lang. Syst. 7(1), 80–112 (1985)

    Article  Google Scholar 

  34. Ghosh, R., et al.: Koord: a language for programming and verifying distributed robotics application. Proc. ACM Program. Lang. 4(OOPSLA), 1–30 (2020)

    Google Scholar 

  35. Gjondrekaj, E., Loreti, M., Pugliese, R., Tiezzi, F.: Modeling adaptation with a tuple-based coordination language. In: SAC 2012, pp. 1522–1527. ACM (2012)

    Google Scholar 

  36. Gjondrekaj, E., et al.: Towards a formal verification methodology for collective robotic systems. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 54–70. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-34281-3_7

    Chapter  Google Scholar 

  37. Gorla, D., Pugliese, R.: Enforcing security policies via types. In: Hutter, D., Müller, G., Stephan, W., Ullmann, M. (eds.) Security in Pervasive Computing. LNCS, vol. 2802, pp. 86–100. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-39881-3_10

    Chapter  Google Scholar 

  38. Gorla, D., Pugliese, R.: Resource access and mobility control with dynamic privileges acquisition. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 119–132. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-45061-0_11

    Chapter  MATH  Google Scholar 

  39. Harbin, J., et al.: Model-driven simulation-based analysis for multi-robot systems. In: 24th International Conference on Model Driven Engineering Languages and Systems (MODELS) (2021)

    Google Scholar 

  40. Hu, C., Dong, W., Yang, Y., Shi, H., Zhou, G.: Runtime verification on hierarchical properties of ROS-based robot swarms. IEEE Trans. Reliabil. 69(2), 674–689 (2019)

    Article  Google Scholar 

  41. Huang, J., Erdogan, C., Zhang, Y., Moore, B., Luo, Q., Sundaresan, A., Rosu, G.: ROSRV: runtime verification for robots. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 247–254. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11164-3_20

    Chapter  Google Scholar 

  42. Koenig, N.P., Howard, A.: Design and use paradigms for Gazebo, an open-source multi-robot simulator. In: IROS, pp. 2149–2154. IEEE (2004)

    Google Scholar 

  43. Kumar, P., et al.: Rosmod: a toolsuite for modeling, generating, deploying, and managing distributed real-time component-based software using ros. In: International Symposium on Rapid System Prototyping (RSP) (2015)

    Google Scholar 

  44. Lomuscio, A., Qu, H., Raimondi, F.: Mcmas: an open-source model checker for the verification of multi-agent systems. Softw. Tools Technol. Transfer 19(1), 9–30 (2017)

    Article  Google Scholar 

  45. Luckcuck, M., Farrell, M., Dennis, L.A., Dixon, C., Fisher, M.: Formal specification and verification of autonomous robotic systems. ACM Comput. Surv. 52, 1–41 (2020)

    Article  Google Scholar 

  46. Majumdar, R., Yoshida, N., Zufferey, D.: Multiparty motion coordination: from choreographies to robotics programs. Proc. ACM Program. Lang. 4(OOPSLA), 134:1–134:30 (2020)

    Google Scholar 

  47. Meng, W., Park, J., Sokolsky, O., Weirich, S., Lee, I.: Verified ROS-based deployment of platform-independent control systems. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 248–262. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-17524-9_18

    Chapter  Google Scholar 

  48. Miyazawa, A., et al.: RoboChart: modelling and verification of the functional behaviour of robotic applications. Softw. Syst. Model. 18(5), 3097–3149 (2019)

    Article  Google Scholar 

  49. Nordmann, A., Hochgeschwender, N., Wigand, D., Wrede, S.: A survey on domain-specific modeling and languages in robotics. Softw. Eng. Rob. 7, 75–99 (2016)

    Google Scholar 

  50. Nordmann, A., Hochgeschwender, N., Wrede, S.: A survey on domain-specific languages in robotics. In: Brugali, D., Broenink, J.F., Kroeger, T., MacDonald, B.A. (eds.) SIMPAR 2014. LNCS (LNAI), vol. 8810, pp. 195–206. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11900-7_17

    Chapter  Google Scholar 

  51. Pinciroli, C., Lee-Brown, A., Beltrame, G.: A tuple space for data sharing in robot swarms. EAI Endorsed Trans. Collab. Comput. 2(9), e2 (2016)

    Google Scholar 

  52. Quigley, M., et al.: Ros: an open-source robot operating system. In: ICRA Workshop on Open Source Software (2009)

    Google Scholar 

  53. Ramaswamy, A., Monsuez, B., Tapus, A.: SafeRobots: a model-driven approach for designing robotic software architectures. In: Proceedings of CTS, pp. 131–134. IEEE (2014)

    Google Scholar 

  54. Rutle, A., Backer, J., Foldøy, K., Bye, R.T.: CommonLang: a DSL for defining robot tasks. In: Proceedings of MODELS18 Workshops. CEUR Workshop Proceedings, vol. 2245, pp. 433–442 (2018)

    Google Scholar 

  55. St-Onge, D., Varadharajan, V.S., Li, G., Svogor, I., Beltrame, G.: ROS and Buzz: consensus-based behaviors for heterogeneous teams. CoRR abs/1710.08843 (2017)

    Google Scholar 

  56. Wang, R.: A formal model-based design method for robotic systems. IEEE Syst. J. 13(1), 1096–1107 (2018)

    Article  Google Scholar 

  57. Yan, Z., Jouandeau, N., Ali, A.: A survey and analysis of multi-robot coordination. Int. J. Adv. Rob. Syst. 10, 1 (2013)

    Google Scholar 

Download references

Acknowledgements

We thank the anonymous reviewers for their useful comments.

Author information

Authors and Affiliations

  1. Dipartimento di Statistica, Informatica, Applicazioni, Università degli Studi di Firenze, Firenze, Italy

    Lorenzo Bettini, Rosario Pugliese & Francesco Tiezzi

  2. School of Science and Technology, Università di Camerino, Camerino, Italy

    Khalid Bourr

Authors
  1. Lorenzo Bettini
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Khalid Bourr
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Rosario Pugliese
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Francesco Tiezzi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Francesco Tiezzi .

Editor information

Editors and Affiliations

  1. University of Limerick, CSIS and Lero, Limerick, Ireland

    Tiziana Margaria

  2. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Bettini, L., Bourr, K., Pugliese, R., Tiezzi, F. (2022). Programming Multi-robot Systems with X-KLAIM. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning. ISoLA 2022. Lecture Notes in Computer Science, vol 13703. Springer, Cham. https://doi.org/10.1007/978-3-031-19759-8_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-19759-8_18

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-19758-1

  • Online ISBN: 978-3-031-19759-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation