Réunion AID/CIEDS "Essaims de drones" et "FARO" des 11 et 12 octobre 2021
Salle Grace Hopper, LIX, Bâtiment Turing. Les
11 octobre à partir de midi, et 12 octobre jusqu'à 16h30.
Présentations
-
Monday 11th October
12am-1:30pm
Welcome, lunch
1:30pm-2pm
Morgan Louédec, "Interval Extended Kalman Filter – combining probabilistic and set membership filters"
The probabilistic and the set membership approaches in the localization problems are often seen as different and in competition. While in practice, the robots often rely on a probabilistic localization with a Kalman Filter for their online autonomous navigation, the set membership method is mainly used in post-process analysis. However, the Extended Kalman Filter (EKF), which has shown to be a precise method for nonlinear state estimation, may diverge if its linearization point is far from the true state. We propose a new filter, the Interval Extended Kalman Filter (IEKF) which benefits from the advantages of the EKF and the Interval Filter (IF). By linearizing the EKF in a feasible set generated by an IF, the IEKF is more likely to converge toward the state of the robot. This new filter has been applied for simulated underwater localization scenarios.
-
2pm-2:15pm
discussion, break
-
2:15pm-2:45pm
Luc Jaulin,
"Determining Ellipsoidal Outer and Inner Enclosures of Nonlinear Mappings of Ellipsoidal Domains", avec A. Rauh
A large variety of approaches for set-valued simulation, parameter identification, state estimation as well as reachability, observability and stability analysis for nonlinear discrete-time systems involve the propagation of ellipsoids via nonlinear functions. It is well known that the corresponding image sets usually possess a complex shape and may even be non-convex despite the convexity of the input data. For that reason, domain splitting procedures are often employed which help to reduce the phenomenon of overestimation that can be traced back to the well-known dependency and wrapping effects of interval analysis. In this talk, we propose a simple, yet efficient scheme for simultaneously determining outer and inner ellipsoidal range enclosures of the solution for the evaluation of multi-dimensional functions if the input domains are themselves described by ellipsoids. The Hausdorff distance between the computed enclosure and the exact solution set reduces at least linearly when reducing the size of the input domains.
-
2:45pm-3pm
discussion, break
-
3pm-3:30pm
Maria Luiza Costa Vianna, "Characterization of the area explored by an autonomous robot",
We are interested in the problem of a mobile robot exploring an unknown environment and we want to determine which part of the environment was explored and how many times. We present the relation of winding numbers with the explored area and a new method for computing it through a set theory approach.
-
3:30pm-3:45pm
discussion, break
-
3:45pm-4:15pm
Guruprerana Shabadi, "Accounting for sensor and communication delays in hybrid systems"
Cyber-physical systems use sensor devices and communication protocols to gather information on their environments in order to react to changes around them. However, in practice these sensors and protocols are far from perfect and can have non-negligible delays in relaying state information, i.e., there might be a delay in observing the current value of a state variable. To further motivate the study of these delays, we discuss the case study of a collision avoidance protocol with a group of robots navigating in space while avoiding collision. Here, we cannot ensure that each robot has exact information of the other robots in the system at every instant of time. To model these delays, we revisit the class of hybrid automata called lazy hybrid automata in the continuous, instead of discrete, semantic. Lazy hybrid automata model non-deterministic delays in observing the value of “input variables” used in invariants and guard conditions. We then discuss some results we have obtained on the expressiveness of some restricted classes of (continuous) lazy hybrid automata by providing their translations into classical hybrid automata.
-
4:15pm-4:30pm
discussion, break
-
7:30pm
Dinner, in Paris
Restaurant Zeyer, next to the Alesia metro station, 62 rue d’alesia
-
Tuesday 12th
9:30am-10:45 (guest presentation, in 2 parts)
Sergio Rajsbaum, "The topology of look-compute-move robot wait-free algorithms”, part I, part II
Look-Compute-Move models for a set of autonomous robots have been thoroughly studied. We consider one of the models that has been considered: Asynchronous Luminous Robots (ALR) model, where robots are located in a graph G. Each robot, repeatedly Looks at its surroundings and obtains a snapshot containing the vertices of G, where all robots are located; based on this snapshot, each robot Computes a vertex adjacent to its current position, and then Moves to it. Robots have visible lights, allowing them to communicate more information than only its actual position, and they move asynchronously, meaning that each one runs at its own arbitrary speed.
We describe several variants of the problem of bringing the robots close to each other. The main result is a direct the asynchronous wait-free multiprocess read/write shared memory model, and hence to a combinatorial topology characterization for the solvable robot tasks.
Based on joint work with Alcántara, Castañeda and Flores-Peñaloza that appeared in the journal Distributed Computing (2019)
-
10:45-11am
discussion, break
-
11am-11:30am
Constantin Enea, "Automated Testing of Distributed Systems Against Functional Specifications"
Large-scale, fault-tolerant, distributed systems are the backbone for many critical software services. Since they must execute correctly and efficiently in the presence of concurrent and asynchronous message exchanges as well as benign (message loss, process crash) or Byzantine failures (message corruption), the underlying algorithms are intricate. Moreover, even when the algorithms are proven correct, testing industrial strength implementations of these algorithms remains a significant challenge, precisely because of the enormous number of exceptional conditions that may arise in production. I will discuss several challenges and approaches for testing such distributed systems against functional specifications.
-
11:30am-11:45am
discussion, break
-
11:45am-12:15am
Lélio Brun, "Proof-carrying code de Lustre vers C"
Specifications based on block diagrams and state machines are used to design control software, especially in the certified development of safety-critical applications.
Tools like SCADE and Simulink/Stateflow are equipped with compilers that translate such specifications into executable code.
They provide programming languages for composing functions over streams as typified by dataflow synchronous languages like Lustre.
In this work, we turn an academic Lustre to C compiler, LustreC, into a certifying compiler.
Along with the produced C code, we generate contracts and predicates in the specification language of the Frama-C tool.
That way, we can give both an encoding of the transition system semantics of the Lustre nodes and a proof obligation that the executable code respects that semantics, to be automatically discharged by SMT solvers.
Moreover, we also translate contracts formulated on the Lustre specifications level into contracts on the C code, in order to ensure that properties shown at high level, eg. using model-checking techniques, still hold at low level.
-
12:15am-12:30pm
discussion, break
-
12:30am-1:30pm
Lunch
-
1:30pm-2pm
Laurent Pautet, "contributions of the mixed criticality approach to complex system design"
The design of safety-critical systems has been drifting from federated architectures, composed of isolate and independent components, to integrated architectures where programs of different criticality levels are sharing a single execution platform. Integrated Modular Avionics (IMA) and the AUTomotive Open System ARchitecture (AUTOSAR) are some prominent examples of industrial initiatives pushing towards integrated architectures for safety-critical systems. This trend in is in part explained by the ever-growing development of multi-core processors and the mixed-criticality (MC) execution model. While multi-core processors offer great processing capabilities and the possibility to execute programs in parallel, safety of most critical programs should not be compromised when sharing the same execution platform with less critical programs. From a timing perspective, MC scheduling techniques are capable of ensuring timeliness of high criticality programs but are also capable of mitigating the under-utilization of execution resources usually caused by over-estimation on Worst-Case Execution Time (WCET). This over-estimation is more notorious on multi-core architectures which are hardly predictable [4], making the MC execution model a promising lead to gain in resource usage (execution time, energy consumption, cost of robotic platform) while ensuring timeliness on critical applications. In this presentation, we give an overview of some contributions of the mixed criticality approach to complex system design.
-
2pm-2:15pm
discussion, break
-
2:15pm-2:45pm
Nan Li, "Case study of the cyber-physical system design: taking race car as an example"
Nowadays, cyber-physical systems (CPS) form an important category of computer systems. They take into consideration the system’s physical properties, such as system dynamic models, in the design of computational elements. Predictive control is one promising solution to provide a long-term perspective and safe (in the sense of the satisfaction of its constraints) control strategy in CPS. Together with other components (such as the perception part and the actuation part), they form a mixed-criticality system (MCS), in which the failure of different tasks causes a different level of consequence.
We focus on the research problem about how to ensure the functional and timing correctness in an MCS. We investigate the race car system as a case study. A model-based predictive controller is proposed to generate the vehicle’s trajectory which is subject to the collision-free constraint and vehicle’s physical limitations. We propose a minimalist architecture for the race car system on which there are essential tasks such as localization, object detection, backup controller, etc. Different tasks in this architecture associate with different criticality levels and can be set to different operation modes. The objective of scheduler design is to guarantee the hard deadline tasks and to maintain enough quality of service (QoS) for other tasks. We implement our proposal on Nvidia Jetson TX2 (featuring two multi-core CPUs and a GPU) as a Proof-of-Concept. Some preliminary testing results will be presented.
2:45pm-3pm
discussion, break
-
3pm-3:30pm
Simon Rohou, "Codac : Catalog Of Domains And Contractors" - reporté
Recent works in the set-membership community have shown that interval and constraint-propagation methods can be used for efficiently solving difficult problems involving nonlinear equations, differential systems, delays, time uncertainties, or unknown initial conditions. Primitive operators designed for solving simple constraints or equations are made available by the community. Some of them are gathered in the Codac library (http://codac.io), that provides tools to combine them easily, thus allowing to tackle complex problems. The outputs are sets of feasible solutions, such as boxes, tubes, or subpavings. In this talk, we will see an example of use of the Codac library, by dealing with a realistic problem of robot localization.
-
3:30pm-3:45pm
discussion, break