| 1. |
- Dust, Lukas, et al.
(författare)
-
A Model-Based Methodology for Automated Verification of ROS 2 Systems
- 2024
-
Ingår i: Proceedings - 2024 IEEE/ACM 6th International Workshop on Robotics Software Engineering, RoSE 2024. - 9798400705663 ; , s. 35-42
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
| 2. |
- Dust, Lukas, et al.
(författare)
-
Dynamic Priority Scheduling for Periodic Systems Using ROS 2
- 2024
-
Ingår i: Lecture Notes in Computer Science. - : Springer Science and Business Media Deutschland GmbH. - 9783031492518 ; , s. 239-243
-
Konferensbidrag (refereegranskat)abstract
- In this paper, a novel dynamic priority scheduling algorithm for ROS 2 systems is proposed. The algorithm is based on determining deadlines of callbacks by taking the buffer size and update rates of channels into account. The efficacy of the scheduling algorithm is demonstrated on an illustrative example, where the needed buffer size is reduced in comparison to the conventional single-threaded executor in ROS 2.
|
|
| 3. |
- Dust, Lukas, et al.
(författare)
-
Experimental Evaluation of Callback Behavior in ROS 2 Executors
- 2023
-
Ingår i: IEEE Int. Conf. Emerging Technol. Factory Autom., ETFA. - : Institute of Electrical and Electronics Engineers Inc.. - 9798350339918
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
| 4. |
- Dust, Lukas, et al.
(författare)
-
Federated Fuzzy Learning with Imbalanced Data
- 2021
-
Ingår i: Proceedings - 20th IEEE International Conference on Machine Learning and Applications, ICMLA 2021. - : Institute of Electrical and Electronics Engineers Inc.. - 9781665443371 ; , s. 1130-1137
-
Konferensbidrag (refereegranskat)abstract
- Federated learning (FL) is an emerging and privacy-preserving machine learning technique that is shown to be increasingly important in the digital age. The two challenging issues for FL are: (1) communication overhead between clients and the server, and (2) volatile distribution of training data such as class imbalance. The paper aims to tackle these two challenges with the proposal of a federated fuzzy learning algorithm (FFLA) that can be used for data-based construction of fuzzy classification models in a distributed setting. The proposed learning algorithm is fast and highly cheap in communication by requiring only two rounds of interplay between the server and clients. Moreover, FFLA is empowered with an an imbalance adaptation mechanism so that it remains robust against heterogeneous distributions of data and class imbalance. The efficacy of the proposed learning method has been verified by the simulation tests made on a set of balanced and imbalanced benchmark data sets.
|
|
| 5. |
- Dust, Lukas, et al.
(författare)
-
Pattern-Based Verification of ROS 2 Nodes Using UPPAAL
- 2023
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - : Springer Science and Business Media Deutschland GmbH. - 9783031436802 ; , s. 57-75
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
| 6. |
- Dust, Lukas, et al.
(författare)
-
Quantitative analysis of communication handling for centralized multi-agent robot systems using ROS2
- 2022
-
Ingår i: IEEE International Conference on Industrial Informatics (INDIN). - : Institute of Electrical and Electronics Engineers Inc.. - 1935-4576 .- 2378-363X. ; 2022-July, s. 624-629
-
Konferensbidrag (refereegranskat)abstract
- Multi-agent robot systems, specifically mobile robots in dynamic environments interacting with humans, e.g., assisting in production environments, have seen an increased interest over the past years. To better understand the ROS2 communication in a network with a high load of nodes, this paper investigates the communication handling of multiple robots to a single tracking node for centralized multi-agent robot systems using ROS2. Thereore, a quantitative analysis of two publisher-subscriber communication architectures and a comparative study between DDS vendors (CycloneDDS, FastDDS and GurumDDS) using ROS2 Galactic is performed. The architectures of consideration are a many-to-one approach, where multiple robots communicate to a central node over one topic, and the one-to-one communication approach, where multiple robots communicate over particular topics to a central node. Throughout this work, the increase in the number of robots at different publishing rates is simulated on a single computer for the different DDS vendors. A further simulation is done using a distributed setup with CycloneDDS. The simulations show that with an increase in the number of nodes, the average data age and the data miss ratio in the one-to-one approach were significantly lower than in the many-to-one approach. CycloneDDS was shown as the most robust regarding crashes and response time under system launch, while FastDDS showed better results regarding the data ageing.
|
|
| 7. |
- Dust, Lukas, et al.
(författare)
-
UPPAAL-based Modeling and Verification of ROS 2 Multi-Threaded Execution and Operating System Reservations
-
Annan publikation (övrigt vetenskapligt/konstnärligt)abstract
- 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.
|
|
| 8. |
- Dust, Lukas, et al.
(författare)
-
UPPAAL-Based Modeling and Verification of ROS 2 Multi-threaded Execution and Operating System Reservations
- 2024
-
Ingår i: Lect. Notes Comput. Sci.. - : Springer Science and Business Media Deutschland GmbH. - 9783031681493 ; , s. 40-59
-
Konferensbidrag (refereegranskat)abstract
- 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 use 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 usefulness of model-based verification of distributed middleware applications, including internal scheduling and influences of underlying operating system actions.
|
|
| 9. |
- Dust, Lukas
(författare)
-
Verifying ROS 2 Based Distributed Robotic Systems
- 2024
-
Licentiatavhandling (övrigt vetenskapligt/konstnärligt)abstract
- 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.
|
|
