SCALP

In this seminar, the Loewner framework is presented as a central element bridging the realization theory with data, rational function-based approximation and identification. The presentation is divided in three parts: (1) elements on linear dynamical systems are recalled, (2) the Loewner realization minimality is stated and, finally, (3) the Loewner barycentric form is presented along with its extension to linear parametric modeling. Each part is illustrated with didactic dynamical system examples, ranging from applied mathematics to classical engineering.

Lieu : Grande salle de réunions à l'ONERA, dans la coursive du bâtiment R à Toulouse ; lien visio https://rdv.onera.fr/seminaireDTIS.

The verification of distributed systems is challenging because these systems
combine a rich structure, a high number of elements and a non-trivial temporal
evolution. A trade-off between automation and completeness of the verification
has to be made. In particular, one can use theorem provers, which offer
complete confidence but tend to require considerable expertise and effort.
Another option is to use model checkers, which offer complete automation, but
cannot handle complex data structures and configurations.

In this talk, we present recent work on verification techniques for
distributed systems that are automatic and "as complete as possible", or
complete and "as automatic as possible". We illustrate our work with the
analysis of Chord, a scalable distributed hash table.
 

Machine learning applications have been gaining considerable attention
in the field of safety-critical systems. Nonetheless, there is up to
now no accepted development process that reaches classical safety
confidence levels. This is the reason why we have developed a generic
programming framework called ACETONE that is compliant with safety
objectives (including traceability and WCET computation) for machine
learning. More practically, the framework generates C code from a
detailed description of off-line trained feed-forward deep neural
networks that preserves the semantics of the original trained model
and for which the WCET can be assessed with OTAWA. We have compared
our results with Keras2c and uTVM with static runtime on a realistic
set of benchmarks.

Lieu : ISAE Supaero, salle 11.114 (Bâtiment 11 - DFM), et en ligne via zoom : 

https://zoom.us/j/97931378938?pwd=djJpcWl1bHFLQkZDWDNUQmVSdUtHZz09

Nous nous intéressons à la politique de gestion des aléas au sein d'un drone, qui consiste à déterminer le mode de fonctionnement du drone (nominal, plus ou moins dégradé) en fonction des défaillances détectées au sein du drone, des ressources disponibles et de la phase de la mission. L'objectif est d'utiliser des techniques formelles afin d'évaluer une politique (ou un ensemble de politiques) de gestion des aléas. Nous modélisons formellement, en Alloy, les éléments décrits plus haut afin de  permettre l'utilisation de techniques formelles pour réaliser des analyses. Une  première analyse consiste à vérifier qu'une politique donnée satisfait bien des  exigences de SdF étant donné un drone avec ses ressources, sa mission, sa capacité de diagnostic, etc. Ce travail ouvre aussi la voie à des évaluations plus ambitieuses visant à traiter les cas où l'on ne dispose que de connaissances partielles sur certains éléments : la politique elle-même (il s'agira alors de synthétiser une politique complète à partir d'une politique partielle) et/ou les ressources au sein du drone (il s'agira alors de proposer une aide à la conception du drone, en indiquant par exemple des redondances indispensables à la tenue des exigences de SdF).

Real-time systems are subjected to strong timing requirements and consequently, timing analyses are necessary to check their temporal correctness.

Worst-Case-Execution-Time (WCET) analyses are of crucial importance, since they enable to check whether all results are delivered in-time. Timing Anomalies (TAs) characterize particular execution phenomena that jeopardize the predictability of the underlying systems, and may threaten the soundness of the WCET analyses. In this talk, we will focus on counter-intuitive TAs arising from scheduling effects. A timing anomaly occurs when a locally faster execution (e.g., due to a cache hit) finally leads to a larger execution time. Beyond the intuitive understanding, various formal definitions were proposed so as to capture this situation. The definitions mainly differ in two ways: the nature of thephenomenon against its consequences on WCET analyses, and the granularity adopted to define locally faster executions. Moreover, the existing definitions are often based on theoretical hardware models that do not refer to the components of the concrete architecture. We base this talk on a concrete assessment framework, from which we go over the various definitions. We argue that TAs are a concrete-hardware property and we show that none of the existing definitions is able to precisely detect TAs on a simple Out-of-Order (OoO) pipeline.

Lieu : hybride ONERA / DTIS, salle de réunion 1er étage bât. R
et visioconférence https://meet.jit.si/seminairesSCALP

Je vous propose de faire une partie d'une présentation faite à l'école d'été temps-réel 2022.
Le groupe de travail Time Sensitive Networking (TSN) de l'IEEE a développé un ensemble d'addenda à Ethernet destiné à le transformer en réseau temps réel. Je vous propose un rapide survol, où on part du fonctionnement d'un réseau Ethernet classique puis on rajoute les différents éléments de TSN.

Lieu : ISAE-SUPAERO, Salle 11.126 (Bâtiment 11 - DFM)
Et en ligne via zoom : https://zoom.us/j/98180404932?pwd=bWhDeHdLTnhCN2RLdEs2QVJxUWtMQT09

Memory interference caused by resource sharing on multicore platforms lead to execution
overheads, which is a security issue for safety-critical applications. To ensure that a given task
is not exceeding its execution deadline, predictability and interference impact must be
optimized. One way to achieve this objective is through task/memory mapping, which consists
in associating a task to a core and the task memory to a DDR memory bank. These associations
can be optimally obtained using metaheuristic multi-objective optimization algorithms. A part
from the DDR memory interference optimization, other criteria can be considered at the same
time, e.g., tasks execution parallelism, energy consumption.

Lieu : visioconférence https://meet.jit.si/seminairesSCALP

We introduce resource allocation techniques for a problem where (1) the agents express requests for obtaining item bundles as compact edge-weighted directed acyclic graphs (each path in such graphs is a bundle whose valuation is the sum of the weights of the traversed edges), and (2) the agents do not bid on the exact same items but may bid on conflicting items, that cannot be both assigned. This setting is motivated by a real application: allocating orbit slots to some users in Earth observation constellations, where items are orbit slots and bundles are sets of orbit slots that allow to observe points of interest at some frequency, and where conflicts appear in case of overlapping between two slots on the same satellite. We propose several solution methods for the allocation (utilitarian, exact leximin, approximate leximin, and greedy) and analyze their performance on several scenarios, wrt to global utility, computation time, and fairness of the allocation.

Les problèmes de planification et d’apprentissage par renforcement sont souvent représentés par des processus de décision markoviens et ses dérivés (bandits, MDP partiellement observables, MDP factorisés, etc.). L’agent doit apprendre les séquences d’actions qui maximisent l’espérance des récompenses qui peuvent être obtenues pendant l’interaction avec son environnement. Le formalisme peut servir de cadre théorique pour étudier de systèmes autonomes, tel un aéronef, un drone, un satellite, un robot, ou un agent virtuel. En effet, dans l'opération de tels systèmes se pose la question de pouvoir apprendre en temps réel et sur place, tout en préservant l’intégrité du système (i.e. en évitant sa perte). Dans cette présentation, on considère les situations où les actions peuvent entraîner des récompenses positives et négatives, qui impactent un budget initial. L’objectif est donc de trouver un bon compromis entre exploration (i.e. agir pour apprendre de nouvelles choses), exploitation (i.e. agir de manière optimale en fonction de ce qui est déjà connu), et sécurité (dans cette présentation, cela veut dire garder à vue la gestion du budget), afin de minimiser le risque de ruine (i.e. la probabilité d’épuiser son budget). C’est une thématique qui s’approche du « safe RL ». Je parlerai de trois articles publiés récemment [1, 2, 3], qui parlent de cette question de survie dans les multiarmed bandits et dans le gambler’s ruin, arrivant à l’apprentissage par renforcement, thème d’un projet en RG fraichement soumis [4].

[1] Perotto, F.S. et al. (2019). Open Problem: Risk of Ruin in Multiarmed Bandits. COLT 2019: 3194–3197.

[2] Perotto, F.S. et al. (2021). Gambler Bandits and the Regret of Being Ruined. AAMAS 2021: 1664-1667.

[3] Perotto, F.S. et al. (2021) Deciding when to quit the gambler's ruin game with unknown probabilities. Int. J. Approx. Reason. 137: 16-33.

[4] Perotto, F.S. et al. (2021) A3R (Apprentissage par Renforcement et Risque de Ruine). Projet RG. ONERA. [unpublished]

TBD