https://www.mdu.se/

Formal verification of robotic applications, particularly those based on ROS 2, is desirable for ensuring correctness and safety. However, the complexity of formal methods and the manual effort required for model creation and parameter extraction often hinder their adoption. This paper addresses these challenges by proposing a model-based methodology that automates the formal verification process using model-driven engineering techniques. We introduce a methodology which can be applied as a toolchain that automates the initialization of formal model templates in UPPAAL using system parameters derived from ROS 2 execution traces generated by the ROS2_tracing tool. The toolchain employs four model representations based on custom Eclipse Ecore metamodels to capture both structural and verification aspects of ROS 2 systems. The methodology supports both implemented and conceptual systems and enables iterative verification of timing and scheduling parameters through model-to-model and model-to-text transformations. A proof-of-concept implementation demonstrates the feasibility of the proposed approach. The designed toolchain supports verification using two types of UPPAAL models: one for individual node verification (e.g., callback latency and buffer overflow) and another for end-to-end latency analysis of ROS 2 processing chains. Experiments conducted on two implemented and one conceptual ROS 2 systems validate the correctness and adaptability of the toolchain. The results show that the toolchain can automate parameter extraction and model generation. The proposed methodology modularizes the verification process, allowing domain experts to focus on their areas of expertise. It targets to enhances traceability and reusability across different verification scenarios and formal models. The approach aims to make formal verification more accessible and practical to robotics developers.

This paper proposes an approach to pattern-based modeling and Uppaal-based verification for ROS 2 applications. The proposed verification focuses on callback execution latencies and buffer overflow. We propose formal model templates to model the execution of ROS 2 system components, created using a pattern-based approach. The model templates simplify the formal modeling of an ROS 2 application. Using Uppaal, we model in Uppaal timed automata, allowing the description of computation chains of ROS 2-based applications. Our focus is on execution behavior, including two versions of the mainline single-threaded executor of ROS 2. System traces generated using the formal models are validated in multiple experiments. Furthermore, we compare two approaches to modeling the execution of nodes that are typically the core units of computation of ROS 2. The first approach is a holistic approach to model ROS 2 applications, including communication and execution in computation chains. The second is an approach for individual nodes only, at a higher abstraction level. Additionally, we show the application of the verification by model checking in two ROS 2 system scenarios where we compare generated model traces to actual system executions. Overall, through formal modeling and verification, we showcase the potential for uncovering errors in the execution of distributed robotic systems.

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. 

Multi-UAV mission control requires a software solution that helps the operator to supervise individual UAVs and coordinate groups of units. This paper explores the experience and methodology of a User Interface for multi-UAVs systems developed for supporting a European project to aggregate heterogeneous UAVs in farming domain. The aim of the proposed system is to support the operator with the extra workload required for supervision of several UAVs while keeping their Situational Awareness (SA) high. The solution is evaluated with respect to workload and SA. A text-to-speech (TTS) approach is also evaluated to assess its effect on these metrics. The results show that while a TTS solution reduces the operator's workload, over-reliance on the system can cause loss of SA for properties which are not directly presented by TTS.

Human hands and fingers have been widely studied in different fields, such as animation, biomechanics, ergonomics, rehabilitation, medicine, and robotics. However, since the hands are a highly complex part of the human body capable of developing precise tasks, replicating human hand mechanisms remains challenging and, thus, continues to be an active area. This study focuses on a bioinspired mechanically equivalent finger model. A parametric model was proposed based on the typical architecture of a human finger, allowing adaptation to different anthropometries. A forward kinematic model assesses each phalanx's range of motion (ROM) during flexion-extension and abduction-adduction. A CAD modeling technique based on fused filament fabrication (FFF) is used for easy fabrication, requiring no assembly. The resulting model achieves the desired ROM, offering a simple solution for hand modeling. This bioinspired model aids in training hand exoskeleton robots, accurately mimicking human finger mechanics for various applications, including rehabilitation and prosthetics. This model helps understand complex hand mechanisms and holds potential for robotics and related fields.

Exoskeletons with active joints arouse great interest for human power augmentation and assistive applications. In this article we present an innovative prototype of a portable shoulder and elbow exoskeleton, for assistance in agricultural tasks and heavy lifting in general. This exoskeleton provides controlled torque for the flexion/extension movements of shoulders and elbows and passive actuation of the movement of abduction and adduction of the shoulder. The remaining degrees of freedom of the shoulder system have been left unrestricted for comfort and little discrepancy with arm and shoulder movement. For this purpose, a serial mechanism has also been incorporated to facilitate scapular movement. On the other hand, the design incorporates a parallelogram beam mechanism to reduce the actuation torques and improve the controllability of the device. Moreover, the mechanical design of this mechanism was improved to ensure alignment between user elbow average flexion/extension rotation axis and that of the mechanism during the complete range of motion.

The advent of powerful control units and the widespread availability of cheap computers have significantly increased the role of artificial intelligence (AI) in various sectors. In the field of maritime applications, this progress has led to the emergence of Edge AI as an important technology. This research focuses on the application of Edge AI to maritime vessels, addressing key aspects of maritime operations. Using Edge AI, we aim to improve the situation awareness and operational efficiency of marine vessels. This study explores Edge AI integration into marine environments and emphasizes its potential to improve on-board safety, navigation and decision-making processes. Our approach shows how smart units decentralized in large central systems can lead to more efficient and adaptive maritime operations and paving the way for a new era of technologically advanced and environmentally conscious maritime practices.

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.

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.

With the rapidly growing use of Multi-Agent Systems (MASs), which can exponentially increase the system complexity, the problem of planning a mission for MASs became more intricate. In some MASs, human operators are still involved in various decision-making processes, including manual mission planning, which can be an ineffective approach for any non-trivial problem. Mission planning and re-planning can be represented as a combinatorial optimization problem. Computing a solution to these types of problems is notoriously difficult and not scalable, posing a challenge even to cutting-edge solvers. As time is usually considered an essential resource in MASs, automated solvers have a limited time to provide a solution. The downside of this approach is that it can take a substantial amount of time for the automated solver to provide a sub-optimal solution. In this work, we are interested in the interplay between a human operator and an automated solver and whether it is more efficient to let a human or an automated solver handle the planning and re-planning problems, or if the combination of the two is a better approach. We thus propose an experimental setup to evaluate the effect of having a human operator included in the mission planning and re-planning process. Our tests are performed on a series of instances with gradually increasing complexity and involve a group of human operators and a metaheuristic solver based on a genetic algorithm. We measure the effect of the interplay on both the quality and structure of the output solutions. Our results show that the best setup is to let the operator come up with a few solutions, before letting the solver improve them.