Search

International audience; 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.

International audience; 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.

International audience; 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.

International audience; 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.

International audience; 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)

International audience; Formal methods and static analysis are widely used in software development, in particular in the context of safety-critical systems. They can be used to prove that the software behaviour complies to its specification: the software correctness. In this article, we address another usage of these methods: the verification of the quality of the source code, i.e., the compliance with guidelines, coding rules, design patterns. Such rules can refer to the structure of the source code through its Abstract Syntax Tree (AST) or to execution paths in the Control Flow Graph (CFG) of functions. AST and CFGs offer complementary information and current methods are not able to exploit both of them simultaneously. In this article, we propose an approach to automatically verifying the compliance of an application with specifications (coding rules) that reason about both the AST of the source code and the CFG of its functions. To formally express the specification, we introduce FO++, a logic defined as a temporal extension of many-sorted first-order logic. In our framework, verifying the compliance of the source code comes to the model-checking problem for FO++. We present a correct and complete model checking algorithm for FO++ and establish that the model checking problem of FO++ is PSPACE-complete. This approach is implemented into Pangolin, a tool for analyzing C++ programs. We use Pangolin to analyze two middle-sized open-source projects, looking for violations of six coding rules and report on several detected violations.

International audience; Real time systems must respect their temporal constraints both in nominal and degraded conditions. Environment disturbances cause faults which are revealed by errors during task execution. Therefore, schedulers must be fault tolerant to guarantee that no deadline will be missed. Phenomena like electromagnetic fields can disturb real-time systems on a extended period of time. During this period of time, it is difficult to forecast faults and their consequences to build efficient fault-tolerant systems. The classical fault models take into account the pseudo-periodic faults. A fault is described as a ponctual event which is separated from the next one by a minimum time interval. They are not made for phenomena extended in time. This paper intends to describe electromagnetic disturbances in a new fault model, named fault burst model. In adequation with the fault burst model, we provide error recovery strategies. These strategies are applied to a fixed-priority scheduler domain. Finally, we provide corresponding schedulability analysis to make the schedulers fault tolerant to fault bursts.

Nowadays embedded real-time systems are often large distributed communicating systems, and the need for bounds on worst-case execution times (WCET) now includes the need of bound on worst-case network traversal time (WCTT). Network calculus is one method used to compute such bounds, and has been successfully applied on Airbus A380 [13]. Nevertheless, the computed bounds could be pessimistic. On the other hand, the scheduling theory can often compute tight bounds, but with algorithms of complexity not able to deal with too large systems.In this paper, the scheduling theory is used to compute tight constraints on flows produced by computers, improving the inputs to the network calculus method and consequently compute better (i.e. lower) bounds.To do so, scheduling methods must be adapted to approach the best and worst date of message production, and some results on network calculus must be written to go from the scheduling method on a finite interval to a general long term constraint.

A robot is a complex system combining hardware and software parts. In order to simplify the robot design, the whole system is split in several separated modules. However, the complexity of the functional and temporal validation to improve the safety counterweights the robot design simplicity.We can find scheduling analysis tools for task-based software. These tools are used to check and validate the schedulability of the tasks involved in a software, run on a specific hardware.However, these methods considers the tasks as monolithic entities, without taking into account their internal structure. The resulting analyses may be too much pessimistic and therefore not applicable to robotic applications.In this work, we have modeled the internal structure of the tasks as state-machines and used these state-machines into the schedulability analysis in order to improve the analysis precision.Moreover, the tools developed during this work have been tested on real robotic use-cases.; Un système robotique est un système complexe, à la fois d’un point de vue matériel et logiciel. Afin de simplifier la conception de ces machines, le développement est découpé en modules qui sont ensuite assemblés pour constituer le système complet. Cependant, la facilité de conception de ces systèmes est bien souvent contrebalancée par la complexité de leur mise en sécurité, à la fois d’un point de vue fonctionnel et temporel.Il existe des ensembles d’outils et de méthodes permettant l’étude d’ordonnançabilité d’un système logiciel à base de tâches. Ces outils permettent de vérifier qu’un système de tâches respecte ses contraintes temporelles. Cependant ces méthodes d’analyse considèrent les tâches comme des entités monolithiques, sans prendre en compte la structure interne des tâches, ce qui peut les rendre trop pessimistes et non adaptées à des applications robotiques.Cette étude consiste à prendre en compte la structure interne des tâches dans des méthodesd’analyse d’ordonnançabilité. Cette thèse montre que le découpage de tâches monolithiques permet d’améliorer la précision des analyses d’ordonnancement. De plus, les outils issus de cestravaux ont été expérimentés sur un cas d’application de robotique mobile autonome.

A robot is a complex system combining hardware and software parts. In order to simplify the robot design, the whole system is split in several separated modules. However, the complexity of the functional and temporal validation to improve the safety counterweights the robot design simplicity.We can find scheduling analysis tools for task-based software. These tools are used to check and validate the schedulability of the tasks involved in a software, run on a specific hardware.However, these methods considers the tasks as monolithic entities, without taking into account their internal structure. The resulting analyses may be too much pessimistic and therefore not applicable to robotic applications.In this work, we have modeled the internal structure of the tasks as state-machines and used these state-machines into the schedulability analysis in order to improve the analysis precision.Moreover, the tools developed during this work have been tested on real robotic use-cases., Un système robotique est un système complexe, à la fois d’un point de vue matériel et logiciel. Afin de simplifier la conception de ces machines, le développement est découpé en modules qui sont ensuite assemblés pour constituer le système complet. Cependant, la facilité de conception de ces systèmes est bien souvent contrebalancée par la complexité de leur mise en sécurité, à la fois d’un point de vue fonctionnel et temporel.Il existe des ensembles d’outils et de méthodes permettant l’étude d’ordonnançabilité d’un système logiciel à base de tâches. Ces outils permettent de vérifier qu’un système de tâches respecte ses contraintes temporelles. Cependant ces méthodes d’analyse considèrent les tâches comme des entités monolithiques, sans prendre en compte la structure interne des tâches, ce qui peut les rendre trop pessimistes et non adaptées à des applications robotiques.Cette étude consiste à prendre en compte la structure interne des tâches dans des méthodesd’analyse d’ordonnançabilité. Cette thèse montre que le découpage de tâches monolithiques permet d’améliorer la précision des analyses d’ordonnancement. De plus, les outils issus de cestravaux ont été expérimentés sur un cas d’application de robotique mobile autonome.