https://www.mdu.se/

mdu.sePublications
1232 of 3
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Verifying ROS 2 Based Distributed Robotic Systems
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0001-9663-5972
2024 (English)Licentiate thesis, comprehensive summary (Other academic)
Abstract [en]

Due to safety criticality, distributed robotic systems, such as Robot Operating System 2 (ROS 2) based applications, often have strict timing requirements. In this thesis, we attempt to simplify formal verification of the timing behaviour of ROS 2 based applications. Therefore, (i) we conduct experiments to determine and define patterns and semantics of ROS 2 task scheduling and execution, (ii) we propose a pattern-based formal approach of modeling and verifying ROS 2 applications via model checking in UPPAAL, and (iii) we propose a methodology for model-based development and verification of ROS 2 application designs. The thesis starts with a comprehensive evaluation of timing behavior, including the internal scheduling of ROS 2 applications, to define evaluation metrics and timing correctness. Based on the evaluation, buffer overflow and callback latency are defined as measures for timing errors. Furthermore, we identify application design patterns and parameters that can influence potential timing errors. To introduce and facilitate the use of formal methods, we propose pattern-based verification, using UPPAAL, creating reusable templates of important ROS 2 application components. Furthermore, we show how to apply the templates to model ROS 2 applications and verify potential buffer overflow and callback latencies. Finally, we propose a novel methodology for automation of verification in the context of ROS 2 that uses generated tracing information of ROS 2 executions to build structural models as class diagrams and, ultimately, formal models in the form of networks of UPPAAL timed automata for model checking. In our approach, one can apply the methodology as a framework that includes model checking as a back-end and, therefore, helping designers to bridge the gap between the ROS 2 code and formal analysis.

Place, publisher, year, edition, pages
Västerås: Mälardalens universitet, 2024.
Series
Mälardalen University Press Licentiate Theses, ISSN 1651-9256 ; 363
National Category
Computer Sciences Robotics Embedded Systems
Identifiers
URN: urn:nbn:se:mdh:diva-67510ISBN: 978-91-7485-670-5 (print)OAI: oai:DiVA.org:mdh-67510DiVA, id: diva2:1870159
Presentation
2024-09-17, U2-024 och via Zoom, Mälardalens universitet, Västerås, 13:30 (English)
Opponent
Supervisors
Available from: 2024-06-17 Created: 2024-06-14 Last updated: 2024-06-17Bibliographically approved
List of papers
1. Experimental Evaluation of Callback Behavior in ROS 2 Executors
Open this publication in new window or tab >>Experimental Evaluation of Callback Behavior in ROS 2 Executors
Show others...
2023 (English)In: IEEE Int. Conf. Emerging Technol. Factory Autom., ETFA, Institute of Electrical and Electronics Engineers Inc. , 2023Conference paper, Published paper (Refereed)
Abstract [en]

Robot operating system 2 (ROS 2) is increasingly popular both in research and commercial robotic systems. ROS 2 is designed to allow real-time execution and data communication, enabling rapid prototyping and deployment of robotic systems. In order to predict and calculate execution times in ROS 2, one needs to analyze its internal scheduler, called executor. The executor has been updated in various distributions of ROS 2, which is shown to impact significantly the periodic execution invoked by the underlying operating system's timers, potentially causing unexpected latencies. To expose the mentioned impact due to executor differences, in this paper, we present an experimental evaluation of the execution behavior of ROS 2's schedulable entities, namely callbacks, among the existing versions of the executor. We visualize the differences of callback execution order via simulation, and we create design-level scenarios that impact the execution of periodically scheduled callbacks, negatively. Moreover, we show how such negative impact can be mitigated by using multi-threaded executors. Finally, we illustrate the observed behavior on a real-world centralized multi-agent robot system. Our work aims to raise awareness within the ROS 2 developer community, regarding possible problems of timer blocking, and propose a mitigation solution of the latter.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers Inc., 2023
Keywords
Multi agent systems, Real time systems, Data-communication, Design levels, Experimental evaluation, Multithreaded, Rapid deployments, Rapid-prototyping, Real time execution, Real-time data, Real-world, Robotic systems, Robot Operating System
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:mdh:diva-64706 (URN)10.1109/ETFA54631.2023.10275668 (DOI)2-s2.0-85175439932 (Scopus ID)9798350339918 (ISBN)
Conference
IEEE International Conference on Emerging Technologies and Factory Automation, ETFA
Available from: 2023-11-09 Created: 2023-11-09 Last updated: 2024-06-14Bibliographically approved
2. Pattern-Based Verification of ROS 2 Nodes Using UPPAAL
Open this publication in new window or tab >>Pattern-Based Verification of ROS 2 Nodes Using UPPAAL
Show others...
2023 (English)In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Science and Business Media Deutschland GmbH , 2023, p. 57-75Conference paper, Published paper (Refereed)
Abstract [en]

This paper proposes a pattern-based modeling and Uppaal-based verification of latencies and buffer overflow in distributed robotic systems that use ROS 2. We apply pattern-based modeling to simplify the construction of formal models for ROS 2 systems. Specifically, we propose Timed Automata templates for modeling callbacks in Uppaal, including all versions of the single-threaded executor in ROS 2. Furthermore, we demonstrate the differences in callback scheduling and potential errors in various versions of ROS 2 through experiments and model checking. Our formal models of ROS 2 systems are validated in experiments, as the behavior of ROS 2 presented in the experiments is also exposed by the execution traces of our formal models. Moreover, model checking can reveal potential errors that are missed in the experiments. The paper demonstrates the application of pattern-based modeling and verification in distributed robotic systems, showcasing its potential in ensuring system correctness and uncovering potential errors.

Place, publisher, year, edition, pages
Springer Science and Business Media Deutschland GmbH, 2023
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 14290 LNCS
Keywords
Model Checking, Pattern-Based Modeling, Robot Operating System 2, Errors, Robot Operating System, Buffer overflows, Distributed robotic systems, Execution trace, Formal modeling, Models checking, Pattern-based models, Potential errors, Single-threaded, Timed Automata
National Category
Computer Sciences
Identifiers
urn:nbn:se:mdh:diva-64592 (URN)10.1007/978-3-031-43681-9_4 (DOI)001158872200004 ()2-s2.0-85174439033 (Scopus ID)9783031436802 (ISBN)
Conference
28th International Conference on Formal Methods in Industrial Critical Systems, FMICS 2023, Antwerp, Belgium, 20 September - 22 September 2023
Available from: 2023-10-30 Created: 2023-10-30 Last updated: 2024-06-14Bibliographically approved
3. UPPAAL-based Modeling and Verification of ROS 2 Multi-Threaded Execution and Operating System Reservations
Open this publication in new window or tab >>UPPAAL-based Modeling and Verification of ROS 2 Multi-Threaded Execution and Operating System Reservations
Show others...
(English)Manuscript (preprint) (Other academic)
Abstract [en]

In this paper, we propose a formal modeling approach in uppaal to simulate and verify multi-threaded robotics middleware execution based on ROS 2. In the modeling process, we consider middleware-specific scheduling by creating formal models that simulate the execution behavior of a ROS 2-based system. Furthermore, we show how to model potential underlying operating system's influences on execution by modeling reservation servers. We propose timed automata templates to model the multi-threaded execution of ROS 2 systems and the reservations of the underlying operating system in uppaal.We show how to utilize the created templates to simulate a ROS 2 application. We demonstrate the application of the formal models and model checking in various ROS 2 experiments. Furthermore, we validate the created models by comparing the observed execution traces in experiments on ROS 2 systems and the simulated traces of our models.Overall, this paper showcases the application and usability of model-based verification of distributed middleware applications, including internal scheduling and influences of underlying operating system actions.

National Category
Robotics Computer Sciences
Identifiers
urn:nbn:se:mdh:diva-67509 (URN)
Available from: 2024-06-14 Created: 2024-06-14 Last updated: 2024-06-14Bibliographically approved
4. A Model-Based Methodology for Automated Verification of ROS 2 Systems
Open this publication in new window or tab >>A Model-Based Methodology for Automated Verification of ROS 2 Systems
Show others...
2024 (English)Conference paper, Published paper (Refereed)
Abstract [en]

To simplify the formal verification of ROS 2-based applications, in this paper, we propose a novel approach to the automation of their model-based verification using model-driven engineering techniques. We propose a methodology starting with ROS 2 execution traces, generated by ROS2_tracing and using models and model transformations in Eclipse to automatically initialize pre-defined formal model templates in UPPAAL, with system parameters. While the methodology targets the simplification of formal verification for robotics developers as users, the implementation is at an early stage and the toolchain is not fully implemented and evaluated. Hence, this paper targets tool developers and researchers to give a first overview of the underlying idea of automating ROS 2 verification.

Hence, we propose a toolchain that supports verification of implemented and conceptual ROS 2 systems, as well as iterative verification of timing and scheduling parameters. We propose using four different model representations, based on the ROS2_tracing output and self-designed Eclipse Ecore metamodels to model the system from a structural and verification perspective. The different model representations allow traceability throughout the modeling and verification process.Last, an initial proof of concept is implemented containing the core elements of the proposed toolchain and validated given a small ROS 2 system. 

National Category
Robotics Embedded Systems Computer Sciences
Identifiers
urn:nbn:se:mdh:diva-67506 (URN)
Conference
2024 ACM/IEEE 6th International Workshop on Robotics Software Engineering (RoSE '24)
Available from: 2024-06-14 Created: 2024-06-14 Last updated: 2024-06-14Bibliographically approved

Open Access in DiVA

No full text in DiVA

Authority records

Dust, Lukas

Search in DiVA

By author/editor
Dust, Lukas
By organisation
Embedded Systems
Computer SciencesRoboticsEmbedded Systems

Search outside of DiVA

GoogleGoogle Scholar

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 89 hits
1232 of 3
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf