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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

This paper is focused on the blind vacant frequency channels detection in 56 MHz observation band divided into 56 channels (1 MHz each) implemented on in-house developed hardware based on the AD9364 transceiver operating in automatic gain control (AGC) mode. Vacant channel detection has been modeled as a binary hypothesis testing problem. Three signal detection algorithms widely used in the literature including energy detection, wavelets, and cyclostationary have been tested and evaluated for potential use in our target application. Primary, offline testing has been performed in the Matlab environment using the data samples captured on the target receiver's front end as a time-domain complex signal. Data samples containing one, two, or three signals generated by hardware signal generator and modulated into 2FSK, BPSK, or QPSK with symbol rate 10, 100, or 1000 kSymbol/s. The highest accuracy of 91.0 % has been observed in the offline detection for continuous wavelet transform, while energy detection has demonstrated 86.4 % accuracy. Cyclostationary detection has shown no distinguishable difference in the spectrum correlation values calculated for the AWGN noise sample and the sample containing BPSK and 2FSK modulated signals. Energy detection and discrete wavelet transform have been implemented on our target hardware and tested in the office environment in conditions that could be approximated by AWGN channel. Test sequences containing one or two signals have been generated by the signal generator and received and processed by our target radio node. Discrete wavelet transform has demonstrated 85.73 % and energy detection 85.25 % accuracy in real-time testing.

The use of multiagent systems (MASs) in real-world applications keeps increasing, and diffuses into new domains, thanks to technological advances, increased acceptance, and demanding productivity requirements. Being able to automate the generation of mission plans for MASs is critical for managing complex missions in realistic settings. In addition, finding the right level of abstraction to represent any generic MAS mission is important for being able to provide general solution to the automated planning problem. In this article, we show how a mission for heterogeneous MASs can be cast as an extension of the traveling salesperson problem (TSP), and we propose a mixed-integer linear programming formulation. In order to solve this problem, a genetic mission planner (GMP), with a local plan refinement algorithm, is proposed. In addition, the comparative evaluation of CPLEX and GMP is presented in terms of timing and optimality of the obtained solutions. The algorithms are benchmarked on a proposed set of different problem instances. The results show that, in the presence of timing constraints, GMP outperforms CPLEX in the majority of test instances.

This paper is focused on the blind symbol rate estimation for the digital FSK modulated signals, based on the classification between three symbol rate classes: 10, 100, and 1000 KSymbol/second using the scalogram images obtained from continuous wavelet transform with Morse wavelet. Pretrained deep learning AlexNet has been transfer learned to classify between symbol rate classes. Training, testing, and validation data sets have been composed of the artificial data generated using Bernoulli binary random signal generator modulated into FSK signal corrupted by additive white Gaussian noise (AWGN) noise with SNR ranging from 1 to 30 dB. Training and validation data sets have been augmented to obtain twice more extensive data set i.e 1800 scalogram images, compared to the original size of 900 samples. The average classification accuracy during validation has reached 99.7 % and during testing 100 % and 96.3 % for the data sets with SNR 25–30 dB and 20–25 dB respectively. The proposed algorithm has been compared with cyclostationary and has shown improved classification accuracy, especially in conditions of low SNR.

A superpixel segment is a group of pixels that carry similar information. The Simple Linear Iterative Clustering (SLIC) is a well-known algorithm for generating superpixels that offers a good balance between accuracy and efficiency. Nevertheless, due to its high computational requirements, the algorithm does not meet the demands of real-time embedded applications in terms of speed and resources. This paper proposes a fully-pipelined FPGA architecture based on SLIC, dubbed FP-SLIC, that exhibits 1) a simplified and efficient algorithm of reduced computational complexity that facilitates algorithm development for FPGAs, 2) a fully pipelined FPGA design operating at 40MHz with a throughput of one pixel per cycle, and 3) a memory-efficient architecture that eliminates the requirement for external memory. FP-SLIC shows promising BSDS500 benchmark results, especially considering boundary recall for less than 1000 superpixels, where it performs better than related works, while, at the same time, accomplishing a throughput of 259 frames per second (fps).

In this paper, a novel path planning algorithm for multiple robots using congestion analysis and control is presented. The algorithm ensures a safe path planning solution by avoiding collisions among robots as well as among robots and humans. For each robot, alternative paths to the goal are realised. By analysing the travelling time of robots on different paths using Petri Nets, the optimal configuration of paths is selected. The prime objective is to avoid congestion when routing many robots into a narrow area. The movements of robots are controlled at every intersection by organising a one-by-one passing of the robots. Controls are available for the robots which are able to communicate and share information with each other. To avoid collision with humans and other moving objects (i.e. robots), a dipole field integrated with a dynamic window approach is developed. By considering the velocity and direction of the dynamic obstacles as sources of a virtual magnetic dipole moment, the dipole-dipole interaction between different moving objects will generate repulsive forces proportional to the velocity to prevent collisions. The whole system is presented on the widely used platform Robot Operating System (ROS) so that its implementation is extendable to real robots. Analysis and experiments are demonstrated with extensive simulations to evaluate the effectiveness of the proposed approach.

This paper is focused on the performance evaluation of nine supervised machine learning algorithms in terms of classification accuracy applied to perform two radio scene analysis tasks: 1. blind binary frequency band occupancy classification: vacant or occupied; 2. interference type classification: sine wave interference, or modulated signal or additive white Gaussian noise (AWGN) for the frequency hopping spread spectrum cognitive radio application. Twenty-nine features derived from the time-, frequency-domain and RSSI, have been used as classification inputs to the evaluated machine learning classifiers. Classifiers training and validation have been performed offline in Matlab Classification Learner and Neural Networks applications using four data sets, generated in the controlled experiment, covering both classification tasks in AWGN and mixed channel propagation conditions (AWGN and Rician fading). Data samples have been generated using a hardware signal generator and recorded on the target application receivers' front end as the time-domain complex signals. The highest classification accuracy of 98.71 % has been demonstrated by Feed Forward Neural Network (FFNN) for the binary occupancy classification in Kfold validation for the mixed data set containing both AWGN and Rician fading channel samples. For the interference type classification, FFNN has demonstrated classification accuracy of 99.82 % for K-fold validation and 99.71 % for hold-out validation. FFNN has been concluded as an acceptable algorithm for further adaptation and embedded deployment on our target radio application for both binary classification between occupied or vacant frequency bands and interference type classification.

Hand rehabilitation has been widely studied since it affects the life quality and independence of those affected. Hand impairment can be caused by several conditions, among them strokes and other cerebrovascular accidents, affecting the capabilities of those who survive them in performing the activities of daily living (ADL). Rehabilitation seeks to restore the ability of a person to perform these crucial ADL. There is a current trend in using robotic rehabilitation and other industry 4.0 tools since it can provide a safe, intensive, and task-oriented at a relatively low cost, which can be combined with other technologies such as virtual and augmented reality, BCI, haptics, and others. Moreover, it can provide accessibility in the face of current panoramas such as COVID-19. Hand exoskeleton robots are one of the most extended robotic devices for rehabilitation. However, a design adapted to the patient's needs is necessary to achieve their capability fully and succeed in rehabilitation. One of the main challenges is that several considerations and parameters affect these devices' design and the broad approaches that can be followed. This brief review aims to understand and empathize as a source of inspiration during the design process of hand exoskeleton robots for rehabilitation.

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.