Amphi 6, Télécom Paris. Les 22 Novembre à partir de 12:00, et 23 Novembre jusqu’à 13:00.
Les repas du midi (22 et 23 nov) seront en salle 0A206, à coté de l’amphi 6.
Le social event est au Zeyer, à 20h.
Mardi 22 Novembre
1:30pm-2:10pm Goubault, « Guaranteed approximations of arbitrarily quantified reachability problems »
In this work, we will show how to compute inner and outer approximations of the set of vectors in R^n satisfying the general quantified formulas of the form: For all x1, exists x2, for all x3, exists x4, … , forall x2k-1, exists x2k, z=f(x1,x2,…,x2k-1,x2k) where f is a general, possibly non-linear, function. This extends our previous work which concentrated on just one for all, exists alternation, and has many applications in control, e.g. robust reachability (f is the flow function of some discrete or continuous dynamical system), motion planning, various hyper properties etc.
2:10pm-2:50pm Rohou, « Exact bounded-error continuous-time linear state estimator »
An interval-based method for estimating the state of a linear continuous-time dynamical system will be presented. In this presentation, we assume that the measurements are provided at discrete times and that all errors are bounded. Interval analysis is used to propagate the interval uncertainties continuously over time. The resulting method is guaranteed to never lose any feasible solution and provides an optimal polygonal enclosure of the state trajectory. A reproducible example will illustrate the principle of the method.
2:50pm-3:30pm Massé, « Differential inclusion contractor using matrix exponentiation »
A differential inclusion contractor based on exponential integrators will be presented. In order to get guaranteed overapproximations of reachable states, we consider the computation of exponential integrators for matrices of intervals. In order to get a precise contraction, we use intersections of parallelotops to represent set of states. The approach is illustrated with a few examples.
3:50pm-4:30pm Lopes, « Challenges for optimal resource utilization in autonomous systems »
In the context of unmanned autonomous vehicles (UAVs), we deal with systems that perform several different tasks simultaneously with varying levels of criticality. In this sense, the problem of managing resources to maximize their utilization and, at the same time, ensure the operation of the most critical tasks emerges.
4:30pm-5:10pm Cordeiro, « JMC : Mixed-Criticality Scheduling for Distributed Real-Time Systems »
As part of a state-of-the-art study on mixed-criticality drone systems, we present JMC the only research work, to our knowledge, on distributed mixed-criticality systems, in this case connected objects (IoT)
Mercredi 23 Novembre
A new method for computing an inner and outer approximation for a set defined as a projection of polynomial equations will be presented. To develop the algorithm, different concepts that are not common in the domain of interval analysis will be used : symmetries, the quotient by an equivalence relation and the choice function. The approach will be illustrated by two important applications. The first one is the inner/outer characterization of the workspace of one object with one degree of freedom. The second application is the estimation of the speed of one object seen by several observers with uncertain headings
9:40am-10:20am Mover, « Refuting Callback Reachability with Message-History Logics »
Proving assertions in event-driven programs is challenging, since programs are written as callbacks that are executed with an order determined by a larger, and often unavailable, to analyze framework (i.e., the control flow of the program is hidden in an unavailable framework implementation). […] Approaches have limitations: the former results in a too imprecise analysis, while the latter results in unsound results, even after a significant manual formalization effort. In this work, we propose an alternative approach where the program analysis user provides a sufficient framework models to prove a specific assertion correct. […] We first provide a program semantic replacing the framework with message histories and an abstract interpretation to analyze such semantic, which is still agnostic of a specification language. We then propose a temporal logic for specifying message histories, and instantiate the abstract interpretation algorithm to reason automatically on such logic.
ROS, the Robot Operating System, is a middleware that eases the programming of robotic applications significantly, bringing standard communication and synchronization mechanisms to a wide variety of operating systems and computers or embedded computer boards. However, a robotic application is a complex set of several services having many relations between them, and multiple choices have to be made regarding the software and the hardware architectures. We present our approach based on the Architecture Analysis and Design Language (AADL) and on a library of AADL models from which early analysis can be performed to allows detection of design errors early in the development process and to optimize system performances. Our approach has been applied to design the prototype of a custom industrial robot whose purpose is to clean large refrigerated rooms with several constraints that prevent the use of existing commercial robots.
11:20am-12:00am Pessaux, « Vers des tableaux et des ODEs … un jour »
The tableaux method is an automated proof search technics initially dealing with first-order logics. Many extensions have been proposed to accommodate different logics and additional theories. Toward the hope to extend this method with guaranteed simulation to prove properties on hybrid systems dynamics described by ODEs, we start with a more modest targe. We present the integration of tableaux to standard arithmetic equations. We show how an oracle can be used to deal with formula involving membership to constant intervals.
1:00pm-2:00pm Goubault, Pautet, Jaulin, Chapoutot, Masson. Réunion de travail