Robotic systems are widely used to interact with humans or to perform critical tasks. As a result, it is imperative to provide guarantees about their behavior. Due to the modularity and complexity of robotic systems, their design and verification are often divided into several layers. However, some system properties can only be investigated by considering multiple layers simultaneously. We propose a cross-layer verification method to verify the expected properties of concrete robotic systems. Our method verifies one layer using abstractions of other layers. We propose two approaches: refining the models of the abstract layers and refining the property under verification. A combination of these two approaches seems to be the most promising to ensure model genericity and to avoid the state-space explosion problem.

In response to the increasing complexity of real-time embedded software, driven by the need for intelligent computation in constrained environments, multicore architectures have emerged as a promising solution. The challenge lies in to choose an effective mapping of the real-time tasks to the various computational resources of these embedded boards, while ensuring real-time constraint satisfaction. To address this problem, our approach rests on two pillars. The first is a domain-specific language designed to capture hardware and software characteristics, constraints, and criteria in a clear and unambiguous manner. The second is a solver method based on Satisfiability Modulo Theories solver augmented with a lazy theory to handle real-time aspects. This method allows us to synthesize mappings that respect temporal constraints and optimize specific criteria, such as the power consumption of the embedded board.

There exist different semantics for Linear Temporal Logic (LTL) in terms of finiteness of the considered traces. Although several ones can be useful depending on the verification context, no verification framework handle their diversity in a simple way. Another limitation of current LTL verification tools is the treatment of concrete domains (bounded and infinite integers, real numbers, etc.). We present an approach to LTL model checking on both finite and infinite traces with concrete domains. Our method is based on an SMT solver and on Bounded Model Checking (BMC). We also present some experiments and compare our tool with NuSMV and nuXmv.

This work presents a novel approach for the online supervision of robotic systems assembled from multiple complex components with skillset-based architectures, using Petri nets (PN). Predictive runtime verification is performed, which warns the system user about actions that would lead to the violation of safety specifications, using online model-checking tools on the system PNs.

Software architectures for autonomous systems are generally structured with 3 layers: a decisional layer managing autonomous reasoning, a functional layer managing reactive tasks and processing, and an executive layer bridging the gap between both. The executive layer plays a central role, as it links high-level tasks with low-level processing, and is generally responsible for the robustness or the fault-tolerance of the overall system. In this paper, we propose a development process for such an executive layer that emphasizes on the dependability of this layer. To do so, we structure the executive layer using skills, that are formally defined using a specific language, and we then provide some tools to verify these models, generate some code, and a methodology to assess the fault-tolerance of the resulting architecture.

The demand of parallel execution in real-time embedded applications has motivated the integration of GPUs as processing accelerators on SoCs (System-on-Chip) embedded architectures, often leading to CPU-iGPU architectures. In the safety-critical domain, it is paramount to ensure that the execution deadlines of critical tasks are not exceeded. To ease the analysis of this kind of tasks, we can make their worst-case execution time more predictable. One way to achieve this is by mitigating or controlling the memory interference generated by the concurrent execution of tasks through the application of a series of techniques (e.g., cache partitioning, bank partitioning, cache locking, bandwidth regulation). Originally, these were applied to CPUs, and more recently, to GPUs as well. In this work, we focus on the hardware-based L2 cache locking on iGPUs as memory interference mitigation mechanism. We are interested in evaluating its capacity for reducing the worst-case and the average-case execution time in different scenarios. Our measurement-based analysis has been carried out on the NVIDIA’s Jetson AGX Orin 64 GB MPSoC, making use of four representative benchmarks (data resetting, 2D convolution, 3D convolution and matrix upsampling).

Usually, robotic systems must be designed as reactive systems because they must be able to react and adapt to their environment and also communicate with some other systems. However, the reactive behavior, because of its non-deterministic nature, is difficult to analyze and prevents designers to perform a proper real-time analysis which is usually needed for critical robotic systems. In this paper, we propose a deterministic task model to handle the reactive behavior as well as the necessary tools to analyze it and verify the respect of real-time constraints. An implementation of this model, which is used in a ROS2 patch, is also presented.

The need for high-level autonomy and robustness of autonomous systems for missions in dynamic and remote environment has pushed developers to come up with new software architectures.A common architecture style is to summarize the capabilities of the robotic system into elementary actions, called skills, on top of which a skill management layer is implemented to structure, test and control the functional layer.However, current available verification tools only provide either mission-specific verification or verification on a model that does not replicate the actual execution of the system, which makes it difficult to ensure its robustness to unexpected events.To that end, a tool, SkiNet, has been developed to transform the skill-based architecture of a system into a Petri net modeling the state-machine behaviors of the skills and the resources they handle.The Petri net allows the use of model-checking, such as Linear Temporal Logic (LTL) or Computational Tree Logic (CTL), for the user to analyze and verify the model of the system.

Safety-critical real-time embedded systems are becoming difficult to model and analyze as they accommodate more and more functionalities, and they rely on more and more complex HW and SW implementations. One of the main difficulty with such systems is to find the right coupling between the task model and the analysis method. Indeed, if the task model is too simple it may add pessimism to the result of the analysis, and it may not be possible to prove the correctness of the systems. If the model is too complex, the analysis may be not efficient enough to be usable; or worst the model may have an incomplete method only or no method at all, so the system cannot be analyzed. Finding, the right couple task model analysis method is a balance between expressiveness and analysis efficiency. In this article, we introduce a new graph real-time task model (noted GGTM) which has been used for several years for the deployment and the analysis of different embedded systems. We discuss its expressiveness compared to the literature and demonstrate its advantages. We also, present a decidable and efficient, exact schedulability analysis.

This paper introduces a conditional planning and execution system for an Earth monitoring satellite. This system builds plans containing optional acquisitions that are activated or not at execution time depending on the amount of energy actually available. One originality is that the energy activation thresholds computed on the ground take into account the capacity of the satellite to use an heliocentric pointing or switch off the payload when acquisitions are canceled. Another originality is that the conditional planner proposed uses several energy propagation models, from conservative models containing margins on power production to optimistic models that allow opportunistic acquisitions to be planned.

The development of software architectures that ensure both a high-level of autonomy in the mission, and the robustness to possible failures, is a challenging task. In this paper, we propose to structure the software architecture around a skill management layer, based on formal skill models. This skill management layer helps to structure and test the underlying functional layer, while it provides a...

The objective of AGLIMMS project, whose acronym stands for Acoustic GLIders Mission Management System, was to coordinate a fleet of underwater gliders whose missions are to obtain physical, chemical, biological and/or acoustic measurements on a large 3D sea area. This paper introduces components and tests of the developed planning and supervision system that was integrated in a global centralised architecture and describes the result of sea experimentation conducted in November 2019 in the Mediterranean Sea with three SeaExplorer gliders from Alseamar.

In this paper, we propose a formal language to specify robot skills, i.e. the elementary behaviours or functions provided by the robot platform in order to perform an autonomous mission. The advantage of the language we propose is that it integrates a wide range of elements that allows to define and provide automatic translation both to operational models, used online to control the skill execution, and descriptive models, allowing to reason about the expected skill execution, and then apply automated planning or model-checking taking skill models into account.

In this paper we approach the problem of Mixed Criticality (MC) for probabilistic real-time systems where tasks execution times are described with probabilistic distributions. In our analysis, the task enters high criticality mode if its response time exceeds a certain threshold, which is a slight deviation from a more classical approach in MC. We do this to obtain an application oriented MC system in which criticality mode changes depend on actual scheduled execution. This is in contrast to classical approaches which use task execution time to make criticality mode decisions, because execution time is not affected by scheduling while the response time is. We use a graph-based approach to seek for an optimal MC schedule by exploring every possible MC schedule the task set can have. The schedule we obtain minimizes the probability of the system entering high criticality mode. In turn, this aims at maximizing the resource efficiency by the means of scheduling without compromising the execution of the high criticality tasks and minimizing the loss of lower criticality functionality. The proposed approach is applied to test cases for validation purposes.

The objective of AGLIMMS project, whose acronym stands for Acoustic GLIders Mission Management System, is to efficiently coordinate a fleet of underwater gliders whose missions are to obtain physical, chemical, biological and/or acoustic measurements on a large 3D sea area. This paper describes planning and supervision functions under development and their integration in a global centralised architecture. A demonstration with three SeaExplorer from Alseamar is planned late 2019.

Gliders constitute a new generation of autonomous underwater platforms. The SeaExplorer glider, developed and commercialized by Alseamar, is a buoyancy-controlled vehicle that profiles from the surface to 1000 m-depth along reprogrammable routes. In the framework of AGLIMMS (Acoustic GLIders Mission Management System) project, a centralized web-based platform for the SeaExplorer gliders has been developed and is presented here. The development of such a tool aimed to bring together very different stakes such as piloting assistance, help for mission planning or interpretation of glider data in a 4-D context. In this short article, a focus is made on satellite products and concrete examples are given to highlight the platforms capabilities.

Fault-tolerant architectures are mandatory to ensure the robustness of autonomous robots performing missions in complex and uncertain environments. The first step of a fault-tolerant mechanism is the detection of a faulty behavior of the system. It is then important to provide tools to help robot developers specify relevant observers. It is moreover crucial to guarantee a correct implementation of the observers, i.e. that the observers do not miss data and do not trigger unsuitable recovery actions in case of false detection. In this paper, we propose a specification language for observers that uses Past-Time LTL to express complex formulas on data produced by software components, and timed constraints on the evaluations of these formulas. We moreover provide an implementation of this specification that guarantees a real-time evaluation of the observers. We briefly describe the observers we have specified for a patrolling mission, and we evaluate the performance of our approach compared to state of the art on a benchmark in which we detect errors on a laser range sensor.

The integration of autonomous robots in real applications is a challenge. It needs that the behaviour of these robots is proved to be safe. In this paper, we focus on the real-time software embedded on the robot, and that supports the execution of safe and autonomous behaviours. We propose a methodology that goes from the design of component-based software architectures using a Domain Specific Language, to the analysis of the real-time constraints that arise when considering the safety of software applications. This methodology is supported by a code generation toolchain that ensures that the code eventually executed on the robot is consistent with the analysis performed. This methodology is applied on a ground robot exploring an area. Categories (2), (3)

Mixed criticality systems combine applications with different levels of safety within the same platform. Those applications execute under different modes, each representing an execution condition that can be required at runtime. This work proposes a mixed criticality schedulability analysis which is a modified version of the earliest deadline first scheduling paradigm. The analysis covers every possible execution condition by providing schedulability that is parametrized by the safety level. Besides, sensitivity analysis is developed for evaluating the impact of mixing criticality to schedulability and defining trade-offs between resource usage and schedulability. Test cases of real-time cyber physical systems are investigated to validate the mixed criticality analysis framework presented.