https://www.mdu.se/

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. 

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.

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.

This paper is focused on multiple supervised machine learning algorithms' performance evaluation in terms of classification accuracy and speed for the blind frequency bands classification into three occupancy classes: white, gray, and black spaces for potential implementation in cognitive radio application. Training and validation data sets consisting of 180 000 samples, including 60 000 samples per class, have been collected in the controlled experiment. Data samples have been generated using a hardware signal generator and recorded on the receiver's front end as the time-domain complex signals. Gray space data samples contain one, two, or three signals modulated into 2FSK, BPSK, or QPSK with symbol rates 10, 100, or 1000 kSymbol/s. White space data samples contain no own generated signals. Black space data samples contain two signals with the symbol rate of 22.5 MSymbol/s and offset +14 MHz and -14 MHz from the central frequency occupying the entire observation band. Training and validation of twenty supervised machine learning algorithms have been performed offline in the Matlab Classification Learner application using the collected data set. Fine decision trees have demonstrated the highest classification accuracy of 87.8 %, the observed classification speed of 630000 Objects/s is also higher than the required 2000 Objects/s. Medium decision trees and ensemble boosted trees have demonstrated 87.5 % and 87.7 % accuracy and classification speeds of 950000 and 230000 Objects/s respectively. Therefore, ensemble boosted trees, and fine and medium decision trees have been selected for the deployment on the target radio application in the scope of future work.

Path planning is an important part of navigation for mobile robots. Several approaches have been proposed in the literature based on a discretisation of the map, including A*, Theta*, and RRT*. While these approaches have been widely adopted also in real applications, they tend to generate non-smooth paths, which can be difficult to follow, based on the kinematic and dynamic constraints of the robot. Time-Elastic-Bands (TEB) have also been used in the literature, to deform an original path in real-time to produce a smoother path, and to handle potential local changes in the environment, such as the detection of an unknown obstacle. This work analyses the effects on the overall path for different choices of initial paths fed to TEB. In particular, the produced paths are compared in terms of total distance, curvature, and variation in the desired heading. The optimised version of the solution produced by Theta* shows the highest performance among the considered methods and metrics, and we show that it can be successfully followed by an autonomous bicycle. 

Multi-agent systems have received a tremendous amount of attention in many areas of research and industry, especially in robotics and computer science. With the increased number of agents in missions, the problem of allocation of tasks to agents arose, and it is one of the most fundamental classes of problems in robotics, formally known as the Multi-Robot Task Allocation (MRTA) problem. MRTA encapsulates numerous problem dimensions, and it aims at providing formulations and solutions to various problem configurations, i.e., complex multi-agent missions. One dimension of the MRTA problem has not caught much of the research attention. In particular, problem configurations including Multi-Task (MT) robots have been neglected. However, the increase in computational power, in robotic systems, has allowed the utilization of parallel task execution. This in turn had the benefit of allowing the creation of more complex robotic missions; however, it came at the cost of increased problem complexity. Our contribution to the aforementioned domain can be grouped into three categories. First, we model the problem using two different approaches, Integer Linear Programming and Constraint Programming. With these models, we aim at filling the gap in the literature related to the formal definition of MT robot problem configuration. Second, we introduce the distinction between physical and virtual tasks and their mutual relationship in terms of parallel task execution. This distinction allows the modeling of a wider range of missions while exploiting possible parallel task execution. Finally, we provide a comprehensive performance analysis of both models, by implementing and validating them in CPLEX and CP Optimizer on the set of problems. Each problem consists of the same set of test instances gradually increasing in complexity, while the percentage of virtual tasks in each problem is different. The analysis of the results includes exploration of the scalability of both models and solvers, the effect of virtual tasks on the solvers' performance, and overall solution quality.

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.