Programme

Programme de la semaine

Programme détaillé du lundi

Des applications aux modèles et contraintes temps réel

• : Lundi 20 - 14:00 - 15:30
• : Emmnanuel Grolleau
• : B140
• : e-grolleau-applications-modeles-contraintes-temps-reel.pdf

Le présentation utilise des exemples d'architectures logicielles et matérielles, principalement issues ou inspirées du monde des drones, de façon à présenter d'où viennent les modèles et contraintes utilisés dans les domaines liés au temps réel. Des exemples de contraintes temps réel, soient issues de contraintes de bout-en-bout sur les chaînes fonctionnelles, soient issues de contraintes locales, sont donnés. Les modèles classiques de tâches temps réel sont ensuite justifiés, et quelques unes de leurs limites mises en avant. L'aspect opérationnel est aussi adressé, en discutant des services rendus par divers RTOS. Ensuite, l'étude de l'évolution des plateformes d'exécution permet de mettre en avant les problèmes liés aux interférences par rapport aux hypothèses de "freedom from interference" exigées par l'ISO 26262. Enfin, l'impact d'avoir un système distribué sur la nécessité d'étudier l'ordonnancement des réseaux est abordé.

Programme détaillé du mardi

Vérification formelle de systèmes temps-réels

• : Mardi 21 - 9:00 - 10:00
• : Frédéric Herbreteau
• : B140
• : f-herbreteau-formal-verification-real-time-systems.pdf

La vérification formelle permet de s'assurer qu'un système satisfait une spécification donnée. Pour cela, on construit un modèle formel du système, auquel il est possible d'appliquer des algorithmes de vérification. Les automates temporisés sont utilisés depuis une trentaine d'années pour modéliser et vérifier les systèmes temps-réel. Cet exposé présentera les automates temporisés et les algorithmes de vérification.

TP - Vérification d'automates temporisés par l'exemple

• : Mardi 21 - 10:30 - 12:30
• : Frédéric Herbreteau
• : B460

Ce TP illustrera sur des exemples concrets la modélisation de systèmes temps-réels par des automates temporisés, et la vérification des modèles obtenus.

Toutes les informations du TP sont disponibles à cette adresse : https://www.labri.fr/perso/herbrete/etr-2021/etr-2021-tp.html

A Formal-Model Execution Engine to Control and Verify Critical Real-Time Systems

• : Mardi 21 - 14:00 - 15:00
• : Pierre-Emmanuel Hladik et Silvano Dal Zilio
• : B140
• : pe-hladik-hippo.pdf

Hippo is a toolchain developped at LAAS-CNRS that integrates tools for design, verification and execution of embedded real-time systems. The aim of this toolchain is to avoid gap between what designers want to express, what is verified and the behavior of the final executable code. Our approach is based on an extension of the Fiacre specification language with runtime features, such as asynchronous function calls and synchronization with events. The execution of the resulting code is supported by a dedicated execution engine that guarantees real-time behavior and that reduces the semantic gap between high-level models and executable code. During this presentation, we will show in a practical way the principles of the toolchain by illustrating how scheduling and real-time aspects are taken into consideration. We will also show an example of implementation on a real robotics application.

Controller Synthesis for Timed Systems

• : Mardi 21 - 15:00 - 16:00
• : Ocan Sankur
• : B140
• : o-sankur-controller-synthesis-timed-systems.pdf

Controller synthesis consists in automatically synthesizing policies to guide a given system so as to satisfy a formal specification. Formally, controller synthesis considers open systems where some actions are controllable, while others are uncontrollable, and the goal is to automatically synthesize a policy to enable or disable controllable actions so as to ensure that the overall behaviors of the system satisfy a given specification. In this tutorial, we describe some data structures and algorithms that are used for the controller synthesis of timed systems.

TP de Cosmos, modélisation et vérification de système probabiliste

• : Mardi 21 - 16:30 - 18:30
• : Benoit Barbot
• : B460

Les systèmes qui exhibent des comportements aléatoires demandent des méthodes particulières pour réaliser leurs vérifications. En effet pour un système déterministe la vérification ne retourne qu'une valeur booléenne : « la spécification est vérifiée ou non », Pour des systèmes probabilistes, une telle dichotomie n'est en général pas souhaitable, par exemple, car une spécification peut être violée avec une très faible probabilité. Dans ce TP nous verrons comment modéliser des systèmes probabilistes temporisés grâce aux réseaux de Petri stochastique généralisée. Nous utiliserons le modèle checker statistique Cosmos pour réaliser la vérification de ces systèmes.

Programme détaillé du mercredi

Ordonnancement temps réel : des origines à l'hétérogène

• : Mercredi 22 - 08:30 - 10:30
• : Antoine Bertout
• : B140
• : a-bertout-methodes-ordonnancement-temps-reel.pdf

Ce séminaire est dédié aux algorithmes d'ordonnancement des tâches et à la vérification du respect des contraintes temporelles d'un système temps réel. Depuis le modèle fondateur de tâches indépendantes de Liu et Layland et des résultats classiques d'ordonnancement monoprocesseur, les modèles de tâches ont gagné en expressivité (dépendances, modes d'activation, parallélisme, etc.), de concert avec la complexité des méthodes d'ordonnancement multiprocesseur et des analyses qui s'y rapportent. Dans cette présentation, nous étudierons les résultats théoriques fondamentaux du domaine et nous dresserons un panorama des contributions visant à représenter plus fidèlement les applications et les plateformes d'exécution modernes, multiprocesseur et à architectures hétérogènes.

Trampoline, un RTOS compatible OSEK/VDX et AUTOSAR

• : Mercredi 22 - 11:00 - 12:00
• : Jean-Luc Bechennec
• : B140
• : jl-bechennec-trampoline.pdf

Trampoline est un RTOS développé dans l'équipe STR du LS2N depuis 2005. Il s'agit d'un RTOS où les tâches sont ordonnancées selon une priorité fixe. Les cibles supportées sont nombreuses : ARM Cortex, PowerPC, AVR, RISC V et Posix. L'empreinte mémoire est faible: une dizaine de ko de ROM et quelques dizaines d'octets de RAM. Comme les autres RTOS AUTOSAR, sa configuration est statique et effectuée hors-ligne via un langage dédié. Tous les objets manipulés par l'OS sont donc connus à la compilation, ce qui permet d'obtenir une faible empreinte mémoire et d'effectuer des optimisations en fonction de l'application. Le but de cette session est de prendre en main Trampoline en construisant une application simple qui permettra de mettre en œuvre les composants principaux de l'OS : tâches, alarmes, événements et ressources.

A quick introduction to Worst-Case Execution Time analysis: from classic methods to open problems

• : Mercredi 22 - 13:30 - 15:00
• : Thomas Carle
• : B140
• : t-carle-otawa.pdf

The scheduling algorithms and temporal validation techniques for Real-Time systems require the knowledge of the Worst-Case Execution Time (WCET) of the tasks composing the system. The WCET of a task is an upper bound on the duration of any of the possible executions of the task. In this talk, we will briefly present the models and methods used to statically derive safe WCET bounds for tasks running in isolation on single-core processors: the Implicit Path Enumeration Technique (IPET), micro-architecture modelling using execution graphs (ExeGraphs) and static cache analysis using abstract interpretation techniques.

We will then open on more complex problems such as cache related preemption delays (CRPD) computation, and on currently open problems such as timing anomalies in complex core architectures and timing interference in parallel hardware.

TP - OTAWA, an open-source toolset dedicated to static WCET analysis

• : Mercredi 22 - 16:00 - 18:00
• : Thomas Carle
• : B460

In this lab session we will introduce the basic use of the OTAWA WCET analyzer. From programs compiled for ARM baremetal targets, we will use the static analyses implemented in OTAWA to automatically detect loops, switch-like branches and pointer function calls, and to analyze which parts of the code contribute more to the WCET, in order to optimize the source code for WCET reduction.

TP - Trampoline, un RTOS compatible OSEK/VDX et AUTOSAR

• : Mercredi 22 - 16:00 - 18:00
• : Jean-Luc Bechennec
• : B309

Trampoline est un RTOS développé dans l'équipe STR du LS2N depuis 2005. Il s'agit d'un RTOS où les tâches sont ordonnancées selon une priorité fixe. Les cibles supportées sont nombreuses : ARM Cortex, PowerPC, AVR, RISC V et Posix. L'empreinte mémoire est faible: une dizaine de ko de ROM et quelques dizaines d'octets de RAM. Comme les autres RTOS AUTOSAR, sa configuration est statique et effectuée hors-ligne via un langage dédié. Tous les objets manipulés par l'OS sont donc connus à la compilation, ce qui permet d'obtenir une faible empreinte mémoire et d'effectuer des optimisations en fonction de l'application.

Le but de cette session est de prendre en main Trampoline en construisant une application simple qui permettra de mettre en œuvre les composants principaux de l'OS : tâches, alarmes, événements et ressources.

TP - Real Time Scheduling Analysis Lab, an example with Cheddar

• : Mercredi 22 - 16:00 - 18:00
• : Frank Singhoff et Hai Nam Tran
• : B308

The objective of this tutorial is to illustrate classical real-time scheduling analysis methods and results for various hardware architectures, for example: uni/multi-processor with memory components.

The tutorial will have the form of a short lecture, with hand-outs and tools made available to participants. The lecture will present various issues raised when implementing or using real-time scheduling analysis tools with a specific focus on the Cheddar tool.

Programme détaillé du jeudi

Solutions libres pour les Systèmes Temps Réel

• : Jeudi 23 - 08:30 - 09:30
• : Pierre Ficheux
• : B140
• : p-ficheux-realtime-linux.pdf

Linux n'est pas nativement un OS temps réel mais l'utilisation des extensions PREEMPT_RT ou Xenomai permet de mettre en place des systèmes hybrides pour lesquels des applications Linux classiques cohabitent avec des applications TR dans le même environnement d'exécution.

TP - RTEMS, PREEMPT_RT et Xenomai

• : Jeudi 23 - 10:00 - 11:45
• : Pierre Ficheux
• : B460

Mise en place de solutions TR libres sur des plateformes de référence (Raspberry Pi, BeagleBone Black, QEMU).

Analyser TSN avec le calcul réseau

• : Jeudi 23 - 13:15 - 14:45
• : Marc Boyer
• : B140
• : m-boyer-analyser-tsn-calcul-reseaux.pdf

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. Cet exposé présentera dans un premier temps les principaux mécanismes temps-réel de TSN. La deuxième partie de l'exposé présentera les résultats de calcul réseau qui permettent de calculer les temps de réponse d'un réseau TSN. L'ensemble introduira le TP du lendemain sur l'outil RTaW-PEGASE d'analyse de réseau temps réel.

Toward Reliable & Available Wireless Low-power Mesh Networking

• : Jeudi 23 - 14:45 - 16:15
• : Georgios Papadopoulos
• : B140
• : g-papadopoulos-rawmn.pdf

Industrial use-case is an emerging domain of application for the IoT. It consists in re-using the IoT technologies to simplify the production chains, ease the deployment and maintenance, and make the factory more flexible and adaptable. Management cost reduction and factory automation can be achieved, in particular, by replacing the existing cables with a wireless medium, as long as an appropriate level of service for critical applications can still be guaranteed at all times. To reach this ambition, the network must be "deterministic". Deterministic in this context means that the designed and deployed low-power wireless mesh network provides guaranteed bandwidth, bounded latency, and other properties germane to the transport of time-sensitive data. A deterministic is a required property for instance, in the power grid, to ensure that high tension lines breakers can be activated within milliseconds, in public transportation to make sure that automated vehicles are operated safely for their passengers, and in industrial automation for control loops. However, the current technologies deployed for the low-power wireless mesh networks are based on best-effort packet switched network.

Combining IEEE Std 802.15.4-TSCH protocol with a blacklisting technique in conjunction with robust Scheduling Function into a low-power wireless mesh networks does not mean that ultra-high end-to-end network reliability and bounded latency is guaranteed under any network conditions. Indeed, wireless links are subject to losses, due to low link quality (i.e., multi-path fading, distance), external interferences, or outage of one node which may decrease the reliability. Thus, wireless transmissions are typically associated with a retry mechanism, such as Automatic Repeat reQuest (ARQ). Retransmission comes at a cost in terms of delay, energy consumption and bandwidth, since it requires additional timeslots under TSCH MAC. On the other hand, the standardized RPL routing protocol proposes failover mechanisms (i.e., Local and Global repair), but the delay to discover and use an alternative path is too long. Considering such challenges, in this talk, state-of-the-art proposals both from academia and from IETF standardization body will be presented. More specifically, the conducted work was employing RPL as the baseline, and extends it with multi-path redundancy, which exploits data packet replication and elimination, promiscuous overhearing, and Forward Error Correction (FEC) to combat isolated and cumulated losses in the network. The thorough performance evaluation campaign show that reliability and predictability in low-power wireless mesh networks can be guaranteed by using multiple parallel data paths instead of retransmissions along a default single path.

Programme détaillé du vendredi

TSN dans les systèmes critiques

• : Vendredi 24 - 08:30 - 09:30
• : Philippe Cuenot
• : B140
• : p-cuenot-tsn-irt.pdf

Aujourd'hui, les technologies Ethernet et TCP/IP constituent l'état de l'art de la communication réseau. Cependant, l'une des faiblesses de ces technologies est la prise en compte des communications temps réel avec des contraintes déterministes, contraintes de latence et de gigue, pour les systèmes embarqués critiques. Le groupe de travail IEEE Time-Sensitive-Network (https://1.ieee802.org/tsn/") a proposé de nouvelles normes pour améliorer la gestion temps réel du trafic Ethernet.

Le but de cette session est de présenter l'initiative EDEN portée par l'IRT Saint-Exupéry qui a pour objectif l'évaluation des normes TSN pour leur application dans une architecture réseau embarqué répondant aux besoins d'un système de communication modulaire et déterministe, sous contrainte de certification. Cette analyse réalisée dans un contexte multi-industriel soit automobile, aéronautique et spatial permettra d'établir des bonnes pratiques et synergies entre les applications réseaux critiques de ces domaines industriels.

TP - Conception et vérification de réseaux TSN avec RTaW-Pegase

• : Vendredi 24 - 10:00 - 12:00
• : Damien Guidolin
• : B460

Ce TP couvre les grandes étapes de la conception et de la vérification de réseaux TSN pour les systèmes critiques: modélisation, sélection et configuration des mécanismes de QoS, validation du respect des contraintes par évaluation de performances (analyse pire-case et simulation). Les participants découvriront comment le concepteur peut subdiviser le problème général de la conception en un ensemble de sous-problèmes qu'un outil peut résoudre de façon efficace, sinon optimale; le dialogue entre le concepteur et l'outil permettant de progresser par raffinement successifs vers une solution optimisée. Ce TP permettra d'observer le comportement dynamique des mécanismes de QoS de TSN (priorités, CBS, TAS, préemption, ATS) sur des traces de simulation d'un réseau automobile réaliste. Ce TP prolongera la session "Analyser TSN avec le calcul réseau" de la veille en présentant, sur un exemple de petite taille, 1) les séquences d'opérations dans l'algèbre (min,+) nécessaires pour borner les délais de communication à l'aide du "calcul réseau" et 2) les différences de précision que l'on peut observer avec différentes classes de fonctions (min,+) pour modéliser les courbes de service et d'arrivée.

Pour toutes questions concernant #ETR2021, contactez le comité d'organisation :

• etr2021@ensma.fr
• +33 5 49 49 80 63
• Laboratoire LIAS, ISAE-ENSMA
  Téléport 2 , 1 avenue Clément Ader
  86360 Chasseneuil-du-Poitou
  France