SpringerLink
Log in

TeSSLa-ROS-Bridge – Runtime Verification of Robotic Systems

  • Conference paper
  • First Online:
Theoretical Aspects of Computing – ICTAC 2023 (ICTAC 2023)

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

Included in the following conference series:

  • 365 Accesses

Abstract

Runtime Verification is a formal method to check a run of a system against a specification. To this end, a monitor is generated from the specification checking the system under scrutiny. Typically, runtime verification is used for checking executions of programs. However, it may equally be well suited for runs of robotic systems, most of which are built and controlled on top of the Robot Operating System (ROS). In stream runtime verification the specifications are given as stream transformations and this approach has become popular recently with several stream runtime verification systems starting from LOLA having emerged. This paper introduces the TeSSLa-ROS-Bridge, which allows to interact with ROS-based robotic systems via the temporal stream-based specification language TeSSLa.

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
EUR 32.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
EUR 29.95
Price includes VAT (Germany)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 60.98
Price includes VAT (Germany)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 79.17
Price includes VAT (Germany)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** 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.

    See http://ros.org.

  2. 2.

    See https://github.com/carla-simulator/ros-bridge.

  3. 3.

    See https://de.mathworks.com/products/ros.html.

  4. 4.

    https://www.tessla.io.

  5. 5.

    https://github.com/ros2/rclpy.

  6. 6.

    https://github.com/PyO3/pyo3.

  7. 7.

    See http://wiki.ros.org/Security.

References

  1. OMG Data Distribution Service (DDS), Version 1.4. Standard, Object Management Group (2015)

    Google Scholar 

  2. DDS Security, Version 1.1. Standard, Object Management Group (2018)

    Google Scholar 

  3. Baheti, R., Gill, H.: Cyber-physical systems. .Impact Control Technol. 12(1), 161–166 (2011)

    Google Scholar 

  4. Bartocci, E., Falcone, Y. (eds.): Lectures on Runtime Verification - Introductory and Advanced Topics. Lecture Notes in Computer Science, vol. 10457. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75632-5

    Book  Google Scholar 

  5. Baumeister, J., Finkbeiner, B., Schirmer, S., Schwenger, M., Torens, C.: RTLola cleared for take-off: monitoring autonomous aircraft. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 28–39. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53291-8_3

    Chapter  Google Scholar 

  6. Convent, L., Hungerecker, S., Leucker, M., Scheffel, T., Schmitz, M., Thoma, D.: TeSSLa: temporal stream-based specification language. In: Massoni, T., Mousavi, M.R. (eds.) SBMF 2018. LNCS, vol. 11254, pp. 144–162. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03044-5_10

    Chapter  Google Scholar 

  7. D’Angelo, B., et al.: LOLA: runtime monitoring of synchronous systems. In: 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), 23–25 June 2005, Burlington, Vermont, USA, pp. 166–174. IEEE Computer Society (2005). https://doi.org/10.1109/TIME.2005.26

  8. Dosovitskiy, A., Ros, G., Codevilla, F., López, A.M., Koltun, V.: CARLA: an open urban driving simulator. In: CoRL. Proceedings of Machine Learning Research, vol. 78, pp. 1–16. PMLR (2017)

    Google Scholar 

  9. Faymonville, P., et al.: StreamLAB: stream-based monitoring of cyber-physical systems. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 421–431. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-25540-4_24

    Chapter  Google Scholar 

  10. Fazzari, K.: ROS 2 DDS-security integration (2020). https://design.ros2.org/articles/ros2_dds_security.html. Accessed 16 Sept 2023

  11. Ferrando, A., Cardoso, R.C., Fisher, M., Ancona, D., Franceschini, L., Mascardi, V.: ROSMonitoring: a runtime verification framework for ROS. In: Mohammad, A., Dong, X., Russo, M. (eds.) TAROS 2020. LNCS (LNAI), vol. 12228, pp. 387–399. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-63486-5_40

    Chapter  Google Scholar 

  12. Friese, M.J., Kallwies, H., Leucker, M., Sachenbacher, M., Streichhahn, H., Thoma, D.: Runtime verification of AUTOSAR timing extensions. In: Abdeddaïm, Y., Cucu-Grosjean, L., Nelissen, G., Pautet, L. (eds.) RTNS 2022: The 30th International Conference on Real-Time Networks and Systems, Paris, France, 7–8 June 2022, pp. 173–183. ACM (2022). https://doi.org/10.1145/3534879.3534898

  13. Gorostiaga, F., Sánchez, C.: Stream runtime verification of real-time event streams with the Striver language. Int. J. Softw. Tools Technol. Transfer 23, 157–183 (2021). https://doi.org/10.1007/s10009-021-00605-3

    Article  Google Scholar 

  14. Jaksic, S., Bartocci, E., Grosu, R., Nguyen, T., Nickovic, D.: Quantitative monitoring of STL with edit distance. Formal Methods Syst. Des. 53(1), 83–112 (2018). https://doi.org/10.1007/s10703-018-0319-x

    Article  MATH  Google Scholar 

  15. Kallwies, H., Leucker, M., Sánchez, C.: Symbolic runtime verification for monitoring under uncertainties and assumptions. In: Bouajjani, A., Holík, L., Wu, Z. (eds.) ATVA 2022. LNCS, vol. 13505, pp. 117–134. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-19992-9_8

    Chapter  MATH  Google Scholar 

  16. Kallwies, H., Leucker, M., Schmitz, M., Schulz, A., Thoma, D., Weiss, A.: TeSSLa - an ecosystem for runtime verification. In: Dang, T., Stolz, V. (eds.) RV 2022. LNCS, vol. 13498, pp. 314–324. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-17196-3_20

    Chapter  Google Scholar 

  17. Kharraz, K.Y., Leucker, M., Schneider, G.: Timed dyadic deontic logic. In: Erich, S. (ed.) Legal Knowledge and Information Systems - JURIX 2021: The Thirty-fourth Annual Conference, Vilnius, Lithuania, 8–10 December 2021. Frontiers in Artificial Intelligence and Applications, vol. 346, pp. 197–204. IOS Press (2021). https://doi.org/10.3233/FAIA210336

  18. Lee, E.A.: The past, present and future of cyber-physical systems: a focus on models. Sensors 15(3), 4837–4869 (2015)

    Article  Google Scholar 

  19. Leucker, M., Sánchez, C., Scheffel, T., Schmitz, M., Thoma, D.: Runtime verification for timed event streams with partial information. In: Finkbeiner, B., Mariani, L. (eds.) RV 2019. LNCS, vol. 11757, pp. 273–291. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-32079-9_16

    Chapter  Google Scholar 

  20. Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Logic Algebr. Progr. 78(5), 293–303 (2009)

    Article  MATH  Google Scholar 

  21. Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT -2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30206-3_12

    Chapter  MATH  Google Scholar 

  22. Nguyen, T., Nickovic, D.: Assertion-based monitoring in practice - checking correctness of an automotive sensor interface. Sci. Comput. Program. 118, 40–59 (2016). https://doi.org/10.1016/j.scico.2015.11.002

    Article  Google Scholar 

  23. Ničković, D., Yamaguchi, T.: RTAMT: online robustness monitors from STL. In: Hung, D.V., Sokolsky, O. (eds.) ATVA 2020. LNCS, vol. 12302, pp. 564–571. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-59152-6_34

    Chapter  Google Scholar 

  24. Painter, R.R.: Software plans: multi-dimensional fine-grained separation of concerns. A Dissertation Proposal (2006)

    Google Scholar 

  25. AUTOSAR, Development, Partnership: Specification of Timing Extensions, Version 1.0.0, Release 4.0.1 (2009)

    Google Scholar 

  26. Perez, I., Dedden, F., Goodloe, A.: Copilot 3. Technical report NASA/TM-2020-220587, NASA Langley Research Center (2020)

    Google Scholar 

  27. Perez, I., Mavridou, A., Pressburger, T., Will, A., Martin, P.J.: Monitoring ROS2: from requirements to autonomous robots. In: FMAS/ASYDE@SEFM. EPTCS, vol. 371, pp. 208–216 (2022)

    Google Scholar 

  28. Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on the Foundations of Computer Science (FOCS-77), pp. 46–57. IEEE Computer Society Press, Providence (1977)

    Google Scholar 

  29. Quigley, M., et al.: ROS: an open-source robot operating system. In: ICRA Workshop on Open Source Software, Kobe, Japan, vol. 3, p. 5 (2009)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Lübeck, Lübeck, Germany

    Marian Johannes Begemann, Hannes Kallwies, Martin Leucker & Malte Schmitz

Authors
  1. Marian Johannes Begemann
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hannes Kallwies
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Martin Leucker
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Malte Schmitz
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Hannes Kallwies .

Editor information

Editors and Affiliations

  1. RWTH Aachen University, Aachen, Germany

    Erika Ábrahám

  2. Eindhoven University of Technology, Eindhoven, The Netherlands

    Clemens Dubslaff

  3. University of Oslo, Oslo, Norway

    Silvia Lizeth Tapia Tarifa

Rights and permissions

Reprints and permissions

Copyright information

© 2023 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

Begemann, M.J., Kallwies, H., Leucker, M., Schmitz, M. (2023). TeSSLa-ROS-Bridge – Runtime Verification of Robotic Systems. In: Ábrahám, E., Dubslaff, C., Tarifa, S.L.T. (eds) Theoretical Aspects of Computing – ICTAC 2023. ICTAC 2023. Lecture Notes in Computer Science, vol 14446. Springer, Cham. https://doi.org/10.1007/978-3-031-47963-2_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-47963-2_23

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-47962-5

  • Online ISBN: 978-3-031-47963-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation