Home » Évènement

Soutenance de thèse de Antoine BERNABEU

Antoine BERNABEU, doctorant au sein de l’équipe STR, présentera sa thèse intitulée :

« Support d’exécution pour les systèmes intermittents » / « Runtime support for intermittent computing »

Le vendredi 15 décembre à 10h45 dans l’amphithéâtre du bâtiment S à l’École Centrale de Nantes.

Voici le lien zoom pour celles et ceux qui ne pourront pas être sur site : https://ec-nantes.zoom.us/j/97371275650

Jury :
M. Jean-Luc BÉCHENNEC, Chargé de recherche, CNRS, invité
M. Mikaël BRIDAY, Maître de conférences, École Centrale de Nantes, co-encadrant
M. Daniel CHILLET, Professeur des universités, Université de Rennes, rapporteur
M. Sébastien FAUCOU, Maître de conférences, Nantes Université, co-encadrant
M. Emmanuel GROLLEAU, Professeur des universités, ISAE-ENSMA, rapporteur
Mme Hanna KLAUDEL, Professeure des université, Université Paris Saclay, examinatrice
M. Olivier H. ROUX, Professeur des universités, École Centrale de Nantes, directeur de thèse

Résumé : Les travaux de cette thèse s’intéressent à la modélisation et le développement de mécanismes permettant une exécution efficace sur des systèmes alimentés par une énergie intermittente tels que les capteurs sans fil. De tels systèmes sont alimentés par énergie renouvelable via un petit tampon d’énergie sous la forme d’un supercondensateur.

La contribution principale est l’exploration d’une approche consciente de l’énergie pour les supports d’exécution intermittents.

Tout d’abord, nous proposons d’utiliser les réseaux de Petri temporels à coût afin de modéliser de tels systèmes et nous proposons une extension de cette sémantique afin de résoudre un problème d’ordonnancement maximisant une variable sous contrainte de coût. En combinant le modèle proposé et une approche pire cas, nous générons un ordonnancement fiable pour les systèmes intermittents qui ne commence aucunes opérations sans la certitude de les finir vis-à-vis de l’énergie disponible. Nous avons ensuite utilisé cet ordonnancement dans un support d’exécution basé sur un système d’exploitation temps-réel pour gérer l’intermittence. Ce support d’exécution utilise un modèle de consommation de l’énergie du système intermittent afin de minimiser les opérations liées à l’exécution intermittente et d’assurer la continuité des opérations de l’application malgré les interruptions fréquentes d’alimentation.

Ces travaux ont été jusqu’à la mise en oeuvre pratique d’un tel support d’exécution sur une étude de cas concernant la détection de chant des oiseaux

Mots-clés : calcul intermittent, internet des objets, réseaux de Petri temporels, support d’exécution

Abstract: The work in this thesis focuses on the modeling and development of mechanisms to enable efficient execution on systems powered by intermittent energy such as wireless sensors. Such systems are powered by renewable energy via a small energy buffer in the form of a supercapacitor.

The main contribution is the exploration of an energy-aware approach for intermittent runtimes.

First, we propose to use cost time Petri nets to model such systems and we propose an extension of this semantics to solve a scheduling problem maximizing a variable under cost constraint. By combining the proposed model and a worst-case approach, we generate a reliable scheduling for intermittent systems that does not start any operation without the certainty of finishing it with respect to the available energy. We then used this scheduling in an execution support based on a real-time operating system to manage intermittency. This runtime support uses a model of the intermittent system’s energy consumption to minimize the operations associated with intermittent execution and to ensure the continuity of the application’s operations despite frequent power interruptions.

This work has gone as far as the practical implementation of such execution support on a case study concerning the detection of birdsong.

Key words : intermittent computing, internet of things, Petri net, runtime

Soutenance de thèse de Bastien Sérée

Bastien Sérée, doctorant au sein de l’équipe STR, soutiendra sa thèse intitulée :

« Problèmes d’optimisation dans les graphes paramétrés » / « Optimisation problems in parametrized graphs »

Le 15 décembre 2022 à 10h, dans l’amphithéâtre B 008, sur le site de l’École Centrale

Jury :
– Directeur de thèse : Didier Lime
– Encadrant : Loïg Jezequel
– Examinateur·rice·s : Nathalie Sznajder, Nicolas Markey, Stéphane Le Roux, Pierre-Alain Reynier et Etienne André
– Rapporteurs : Pierre-Alain Reynier et Etienne André

Résumé :

Nous considérons des graphes orientés pondérés dont l’énergie est paramétrée. Nous proposons dans un premier temps un algorithme qui, étant donné un graphe et un de ses sommets, renvoie des arbres, chaque arbre représentant les plus courts chemins depuis la source vers tous les autres sommets du graphe pour une zone particulière de l’espace des paramètres. De plus l’union de ces zones couvre l’espace des paramètres. Nous considérons ensuite l’accessibilité dans les graphes à énergie multi-dimensionnelle, avec un type de contraintes plus absolues qui imposent que l’énergie reste entre des bornes. Nous montrons la décidabilité et la complexité du problème quel que soit le nombre de paramètres et de dimensions lorsque les paramètres prennent des valeurs entières. Nous montrons également l’indécidabilité de ce problème avec au moins un paramètre lorsque la dimension est supérieure ou égale à deux. Nous étudions enfin des jeux de parité à un et deux joueurs sur les graphes paramétrés dont l’objectif est la conjonction d’une condition qualitative sur la parité et d’une condition quantitative : l’énergie doit rester positive. Nous montrons la décidabilité et prouvons des bornes de la complexité du problème de la recherche d’une stratégie gagnante dans les cas à un et à deux joueurs.

Mots-clés : automate, graphes paramétrés, plus court chemin, jeux sur les graphes, objectifs de parité, contraintes sur l’énergie, model-checking.

Abstract:

We are considering weighted oriented graphs with parametrized energy. Firstly we propose an algorithm that, given a graph and one of its vertices, returns trees, every tree representing shortest-paths from the source to every other vertex for a particular zone of the parameter space. Moreover, union of these zones is a covering of the parameter space. Then we consider reachability in graphs with multi-dimensional energy, with stricter constraints that enforce the energy to stay between bounds. We prove decidabilty and complexity of this problem regardless of the dimension and the number of parameters when parameters take integer values. We also prove the undecidability of this problem when there is at least one parameter and the dimension is at least two. Finally we study parity games on parametrized graphs with one and two players whose objective is the conjunction of a qualiative condition on the parity and quantitative one : energy must stay positive. We show the decidability and prove bounds on the complexity of the problem of searching a winning strategy in both cases with one and two players.

Keywords: automata, parametrized graphs, shortest paths, games on graphs, parity objectives, energy constraints, model-checking

Soutenance de thèse de Ons AOUEDI

Ons AOUEDI, doctorante au sein des équipes STACK/STR, soutiendra sa thèse intitulée :

« Analyse du trafic réseau basée sur l’apprentissage automatique » / « Machine Learning-Enabled Network Traffic Analysis«

Le 2 décembre 2022 à 9h00, dans l’amphithéâtre du bâtiment 34 sur le site de la Faculté de Sciences & Techniques

Jury :

Président : Yassine HADJADJ-AOUL Professeur, Université de Rennes I, France.
Examinateurs: Adlen KSENTINI Professeur, Eurecom, Sophia Antipolis, France, Sonia BEN MOKHTAR Directrice de Recherche CNRS/INSA LYON, France Yusheng JI Professeure, National Institute of Informatics, Japon
Dir. de thèse : Benoît PARREIN Maître de Conférences HDR, Nantes Université
Co-encadrant. de thèse : Kandaraj PIAMRAT Maître de Conférences, Nantes Université

Résumé :

L’Internet des Objets entraînent par son nombre de terminaux une explosion du trafic de données. Pour augmenter la qualité globale de réseau, il est possible d’analyser intelligemment le trafic réseau afin de détecter d’éventuel comportement suspect ou malveillant. Les modèles d’apprentissage automatique et d’apprentissage profond permettent de traiter ce très grand volume de données. Néanmoins, il existe certaines limites dans la littérature, notamment la confidentialité des données, le surapprentissage (manques de diversité dans les données) ou tout simplement le manque de jeu de données labélisées. Dans cette thèse, nous proposons de nouveaux modèles s’appuyant sur l’apprentissage automatique et l’apprentissage profond afin de traiter une grande quantité de données tout en préservant la confidentialité. Notre première approche utilise un modèle d’ensemble. Les résultats montrent une diminution du surapprentissage, tout en augmentant de 10\% la précision comparé à des modèles de l’état de l’art. Notre seconde contribution s’attache aux problèmes de disponibilité des données labélisées. Nous proposons un modèle d’apprentissage semi-supervisé capable d’améliorer la précision de 11\% par rapport à un modèle supervisé équivalent. Enfin, nous proposons un système de détection d’attaque s’appuyant sur l’apprentissage fédéré. Nommé FLUIDS, il permet de réduire la surcharge réseau de 75\% (comparé à son équivalent centralisé) tout en préservant de très haute performance et la confidentialité.

Mots-clés : Apprentissage automatique, Apprentissage fédéré, analyse du trafic

Abstract :

Recent development in network communication along with the drastic increase in the number of smart devices leads to an explosion in data generation. To this end, intelligent network traffic analysis can help to understand the behavior of connected smart devices and applications as well as provides defense against cyber-attacks. In this line, Machine Learn- ing (ML) and Deep Learning (DL) models have the ability to model and uncover hidden patterns using training data or environment. Despite their benefits, major challenges need to be addressed such as model generalization (due to model overfitting), lack of label (due to the difficulty to label all the data), and privacy (due to recent regulations). In this thesis, new ML/DL-based models are proposed for tackling these challenges. The first contribu- tion focuses on improving the generalization and classification performance by proposing an ensemble blending model. The simulation results show that the accuracy of the proposed ensemble model is 10%, better than some state-of-the-art models. Second, a semi-supervised model has been proposed and the experiment results show that unlabeled data boost the classification accuracy by 11% in comparison to its supervised version. Finally, a Feder- ated Learning (FL) based Intrusion Detection System (IDS) has been proposed. It allowed the clients to learn an efficient intrusion detection model without the need to label their local data as well as to achieve high classification performance and improvement in terms of communication overhead (reduction by almost 75% in comparison to a centralized model).

Keywords : Machine Learning, Federated Learning, traffic analysis

Soutenance de thèse de Imane HAUR

Imane HAUR, doctorante au sein de l’équipe STR, soutiendra sa thèse intitulée :

« Modélisation et vérification formelles d’un RTOS multicœur conforme à AUTOSAR » / « AUTOSAR compliant multi-core RTOS formal modeling and verification »

le 30 novembre 2022, à 10h, dans l’amphithéâtre du bâtiment S, sur le campus de l’École Centrale. La présentation des travaux se fera en français.

Cette thèse a été préparée au sein du laboratoire LS2N à l’École Centrale de Nantes dans le cadre d’une thèse CIFRE avec le centre de recherche de Huawei Paris.

Jury :

Directeur de thèse : Pr. Olivier H. ROUX
Co-encadrant : Dr. Jean-Luc BÉCHENNEC (Chargé de recherche, CNRS)
Rapporteurs : Pr. Emmanuel GROLLEAU (Professeur des universités, ISAE-ENSMA); Pr. Patrick MARTINEAU (Professeur des universités, École Polytechnique de l’Université de Tours).
Autres membres : Pr. Gaétan HAINS (Professeur des universités, HUAWEI Paris research center); Pr. Isabelle PUAUT (Professeure des universités, Université de Rennes).

Résumé : La vérification formelle est une solution pour augmenter la fiabilité de l’implémentation du système.
Dans notre travail de thèse, nous nous intéressons à l’utilisation de ces méthodes pour la vérification des systèmes d’exploitation multi-cœurs temps réel. Nous proposons une approche de model-checking utilisant les réseaux de Petri temporels, étendus avec des transitions colorées et des fonctionnalités de haut niveau. Nous utilisons ce formalisme pour modéliser le système d’exploitation multi-cœur Trampoline, conforme aux standards OSEK et AUTOSAR. Nous définissons dans un premier temps ce formalisme et montrons son adéquation avec la modélisation de systèmes concurrents temps reel. Nous utilisons ensuite ce formalisme pour modéliser le système d’exploitation multi-cœur Trampoline et vérifions par model-checking sa conformité avec le standard AUTOSAR. À partir de ce modèle, nous pouvons vérifier des propriétés aussi bien sur l’OS que sur l’application telles que l’ordonnançabilité d’un système temps-réel ainsi que les mécanismes de synchronisation : accès concurrents aux structures de données du système d’exploitation, ordonnancement multi-cœur et traitement des interruptions inter-cœur. À titre d’illustration, cette méthode a permis l’identification automatique de deux erreurs possibles de l’OS Trampoline dans l’exécution concurrente, montrant une protection insuffisante des données et une synchronisation défectueuse.

Mots-clés : Vérification formelle, Model-checking, Réseaux de Petri colorés de haut niveau, Systèmes d’exploitation temps réel, Exécution multi-cœurs, Vérification d’OS AUTOSAR.

Abstract: Formal verification is a solution to increase the system’s implementation reliability. In our thesis work, we are interested in using these methods to verify multi-core RTOS. We propose a model-checking approach using time Petri nets extended with colored transitions and high-level features. We use this formalism to model the Trampoline multi-core OS, compliant with the OSEK and AUTOSAR standards. We first define this formalism and show its suitability for modeling real-time concurrent systems. We then use this formalism to model the Trampoline multi-core RTOS and verify by model-checking its conformity with the AUTOSAR standard. From this model, we can verify properties of both the OS and the application, such as the schedulability of a real-time system and the synchronization mechanisms: concurrent access to the data structures of the OS, multi-core scheduling, and inter-core interrupt handling. As an illustration, this method allowed the automatic identification of two possible errors of the Trampoline OS in concurrent execution, showing insufficient data protection and faulty synchronization.

Keywords: Formal verification, Model-checking, High-level Colored Time Petri Nets, Real-Time Operating Systems (RTOS), Multi-core execution, AUTOSAR OS verification.

Festival Instants Fertiles#9 avec Athénor (Centre national de création musicale)

Dans le cadre du festival Instants Fertiles, qui se déroulera du 19 novembre au 5 décembre 2021,

les enseignants-chercheurs des équipes Gallinette, PSI et STR : Assia MAHBOUBI, Guilhem JABER, Claude MARTINEZ, Loig JEZEQUEL sont heureux de vous convier aux représentations de leur projet « Pièces à Pédale » au Life, Base sous-marine, Boulevard de la Légion d’honneur à St-Nazaire

vendredi 3 décembre à 20h30
samedi 4 décembre à 15h
et dimanche 5 décembre dans l’après-midi de clôture du festival

Pour donner envie : « C’est une constellation de pièces qui ont en commun de s’intéresser au dédoublement de la voix et d’utiliser un dispositif électro-acoustique simple et réduit à l’essentiel : la pédale. Alessandro Bosetti est un compositeur qui aime explorer les paradoxes du rapport entre langues naturelles et musique ; et réserve une attention toute particulière à la voix « quotidienne ». La plupart de ses œuvres pour ensembles vocaux et instrumentaux, ainsi que de nombreuses pièces expérimentales pour la radio, s’inspirent de conversations, de bavardages, d’entretiens, de jeux de traduction et de malentendus.

Après avoir écrit trois solos pour instrumentiste/sujet parlant, il rencontre, à l’invitation d’Athénor, des chercheurs de l’université de Nantes. De leurs recherches et expérimentations, émergent un duo pour musicien et chercheuse ainsi qu’un opéra de chambre pour trois musiciens et quatre chercheurs en conversation modulée. »

Félicitations aux équipes SIMS et STR pour leur best paper award remporté lors de la conférence Audio Mostly 2021 !

Vincent Lostanlen (CR CNRS, équipe SIMS), Antoine Bernabeu (doctorant, équipe STR (encadrants : M. Briday, S.Faucou, O. H. Roux), Jean-Luc Béchennec (CR CNRS, équipe STR), Mikaël Briday (MCF ECN, équipe STR), Sébastien Faucou (MCF UN, équipe STR) et Mathieu Lagrange (CR CNRS, équipe SIMS) ont eu le plaisir de voir leurs travaux communs récompensés à l’occasion de la conférence Audio Mostly 2021.

Plus précisément, l’équipe mixte SIMS / STR a déposé un papier présenté lors du 2ème workshop international sur l’Internet des sons (IWIS 2021), organisé par le Département d’ingénierie de l’information et d’informatique de l’Université de Trento (Italie) qui s’est tenu du 1er au 3 septembre 2021. L’Internet des Sons est un domaine de recherche émergent, à l’intersection des domaines de l’Internet des Objets et de l’Informatique du Son et de la Musique.

Vous pouvez retrouver le talk sur la chaîne Youtube de Vincent, et l’article intitulé « Energy Efficiency is Not Enough: Towards a Batteryless Internet of Sounds » sur HAL.

Workshop CAPITAL (sCalable And PrecIse Timing AnaLysis for multicore platforms)

Le laboratoire VERIMAG organise un webinaire relatif à « l’analyse temporelle précise et passant à l’échelle pour les plates-formes multicœurs »

vendredi 4 juin 2021 de 13h à 17h30.

Sébastien Faucou et Jean-Luc Béchennec (équipe STR) assureront le discours d’ouverture et traiteront de la problématoique suivante « Formal models of timed systems: WCET analysis in single-core systems, and some ideas for timing analysis in multi-core systems« .

Programme complet et inscription.

Soutenance d’HDR d’Audrey QUEUDET (équipe STR)

Audrey Queudet, Maître de conférences au sein de l’équipe STR, soutiendra son Habilitation à Diriger des Recherches (HDR) intitulée « Synchronisation et autonomie énergétique des systèmes temps réel embarqués » / « Synchronization and energy autonomy of embedded real-time systems »

lundi 7 juin 2021 à 10h (CET) en hybride depuis l’amphi du bâtiment 34 sur le site FST.
Elle sera retransmise en direct à l’adresse suivante : https://live.lifesizecloud.com/extension/5627660

Jury :
Maryline Chetto, Professeur des Universités LS2N / Université de Nantes — Présidente
Daniel Chillet, Professeur des Universités IRISA Rennes / ENSSAT — Rapporteur
Alfons Crespo, Professeur des Universités, Escuela Técnica Superior de Ingeniera Informatica de Valencia — Examinateur
Laurent George, Professeur des Universités LIGM / ESIEE Paris — Rapporteur
Pascal Richard, Professeur des Universités LIAS / IUT de Poitiers — Rapporteur
Liliana Cucu-Grosjean, Chargée de Recherche INRIA Paris — Examinatrice

Lien vers le manuscrit : https://uncloud.univ-nantes.fr/index.php/s/kZrFCXRfPCoZbWN

Résumé (du manuscrit) :

Les travaux présentés dans ce document s’articulent selon deux axes de recherche principaux : (i) la synchronisation d’applications temps réel multicœur, et (ii) l’autonomie énergétique des systèmes temps réel embarqués. Ces problématiques sont abordées du point de vue de l’ordonnancement en prenant en compte plusieurs types de contraintes : des contraintes temporelles, des contraintes de partage de ressources, des contraintes de qualité de service (QoS), et des contraintes d’énergie.

Gérer efficacement les accès concurrents à la mémoire dans un contexte temps réel multicœur se révèle complexe. Le verrouillage systématique peut réduire le parallélisme de la plate-forme d’exécution et engendrer par là-même une baisse significative des performances. Forts de ce constat, nous avons donc étudié l’adaptation des mémoires transactionnelles (mécanismes de synchronisation non-bloquant) aux systèmes temps réel multicœur. Au travers d’une étude expérimentale, nous avons comparé les performances de plusieurs mémoires transactionnelles afin de déterminer les facteurs clés (ex : système d’exploitation, politique d’ordonnancement, allocateur mémoire) influant sur la gigue d’exécution des transactions, gigue pouvant impacter directement le respect des contraintes temporelles des tâches dans un système temps réel. Nous avons ensuite proposé une mémoire transactionnelle logicielle temps réel hard, la STM-HRT, permettant de garantir la progression de toutes les transactions du système. Une analyse fonctionnelle et temporelle de la STM-HRT nous a permis de valider le mécanisme de synchronisation non bloquant proposé.

Les systèmes embarqués de nouvelle génération tels que les nœuds de capteurs sans fil se sont multipliés ces dernières années. Pour nombre de ces systèmes, l’autonomie énergétique est une problématique capitale. La technologie du energy harvesting consistant à capter l’énergie dans l’environnement pour alimenter un système, permet en particulier de doter ces systèmes embarqués aux ressources contraintes, d’une capacité d’autosuffisance énergétique. L’informatique “intelligente” embarquée au sein de ces systèmes possède très souvent des exigences temps réel au niveau des traitements logiciels. Il convient alors de garantir le fonctionnement perpétuel du système en gérant conjointement deux types de contraintes : le temps et l’énergie. C’est précisément l’objet de nos contributions sur cette thématique, en considérant le problème du point de vue de l’ordonnancement des tâches applicatives sur le processeur. Nous avons tout d’abord mis en évidence l’inefficacité des ordonnanceurs temps réel “classiques” tels que EDF, incapable à s’accommoder des fluctuations de l’énergie d’alimentation. Nous avons cependant montré qu’il reste le meilleur ordonnanceur non-oisif dans le contexte du energy harvesting et qu’il constitue le meilleur choix d’intégration pour un système ne pouvant disposer d’une estimation prédictive de l’énergie exploitable. Nos travaux ont ensuite consisté en l’identification de quelques-unes propriétés clés d’un ordonnanceur dans le contexte du energy harvesting. Puis, nous avons contribué au problème de la faisabilité d’un ensemble de tâches temps réel à contraintes strictes dans ce même contexte, par la proposition d’un nouveau test, robuste vis-à-vis de la puissance de la source d’énergie. Les contributions présentées par la suite visent à apporter des solutions adaptées aux situations de surcharge temporaire de traitement et/ou de consommation énergétique dont un système peut souffrir. Sur la base d’un nouveau modèle de tâches intégrant des contraintes de QoS, nous avons proposé de nouveaux ordonnanceurs contrôlant notamment le nombre et l’identité des jobs de tâches abandonnés en cas de surcharge. Nous avons enfin proposé un test de faisabilité nécessaire intégrant conjointement les contraintes de QoS et d’énergie.

—————————————————————————————————————————————————————————————————————————————————————-

Abstract (of the manuscript):

The work presented in this document addresses two main research concerns: (i) the synchronization of multicore real-time applications, and (ii) the energy autonomy of embedded real-time systems. These problems are approached from a scheduling point of view by taking into account several types of constraints: temporal constraints, resource sharing constraints, quality of service (QoS) constraints, and energy constraints.

Efficiently managing concurrent memory access in a multicore real-time context is complex. Systematic locking can reduce the parallelism of the execution platform and thus lead to a significant performance loss. Based on this observation, we have studied the adaptation of transactional memories (non-blocking synchronization mechanisms) to multicore real-time systems. Through an experimental study, we compared the performance of several transactional memories in order to determine the key factors (e.g. operating system, scheduling policy, memory allocator) impacting the execution jitter of transactions, jitter that can directly impact the respect of the temporal constraints of tasks in a real-time system. We then proposed a hard real-time software transactional memory, called STM-HRT, which guarantees the progress of all transactions in the system. A functional and temporal analysis of the STM-HRT allowed us to validate the proposed non-blocking synchronization mechanism.

New generation embedded systems such as wireless sensor nodes have been proliferating in recent years. For many of these systems, energy autonomy is a key issue. The technology of energy harvesting, which consists of capturing energy from the environment to power a system, makes it possible in particular to provide these resource-constrained embedded systems with the capacity for energy self-sufficiency. The intelligence embedded in these systems has very often real-time requirements in terms of software processing. It is then necessary to guarantee the perpetual operation of the system by jointly managing two types of constraints: time and energy. This is precisely the purpose of our contributions on this topic, by considering the problem from the point of view of the scheduling of tasks on the processor. We first highlighted the inefficiency of “classical” real-time schedulers such as EDF, which are unable to cope with fluctuations in the supply energy. However, we have shown that it remains the best non-idling scheduler in the context of energy harvesting and that it is the best choice of integration for a system that cannot have a predictive estimate of the exploitable energy. Our work then consisted in identifying some key properties of a scheduler in the energy harvesting context. Then, we contributed to the problem of the feasibility of a set hard real-time tasks in this same context, by proposing a new test which is robust with respect to the power of the energy source. The contributions presented right after aim at providing solutions adapted to situations of transient processing and/or energy consumption overload that a system may suffer from. Based on a new task model integrating QoS constraints, we have proposed new schedulers controlling in particular the number and identity of task jobs skipped in case of overload. Finally, we proposed a necessary feasibility test integrating both QoS and energy constraints.

Journée Scientifique du programme WISE le 17/12

Inscription et programme sur le site web We Network (agenda/journée scientifique).

En visioconférence, le 17 décembre 2020 de 13:00 à 17:30

3 ateliers : Connected Devices, Smart Sensors & Smart Power

Présentation des projets COWIN et SPARTES (Mikaël, STR) pour le LS2N (atelier Objets Connectés)

Soutenance de thèse de Khaoula BOUKIR (équipe STR)

Khaoula Boukir, doctorante au sein de l’équipe STR, soutiendra sa thèse intitulée « Mise en œuvre de politiques d’ordonnancement temps réel multiprocesseur prouvée » / « Proven implementation of multiprocessor real-time scheduling policies »

mercredi 16 décembre 2020 à 10h en visio.

Lien de connexion : https://univ-nantes-fr.zoom.us/j/86296772127?pwd=RXFzQU1lem9tQzFsQXMySFc4cjRaZz09 (Meeting ID: 862 9677 2127 / Passcode: 960277)

Jury :
– Directeur de thèse : Jean-Luc Béchennec, Chargé de recherche, CNRS
– Co-encadrant : Anne-Marie Déplanche, Maître de conférences, Université de Nantes
– Rapporteurs : Claire Pagetti Ingénieur recherche, ONERA ; Emmanuel Grolleau, Professeur des universités, ISAE-ENSMA
– Autres membres : Isabelle Puaut, Professeur des universités, Université de Rennes 1 ; Pascal Richard, Professeur des universités, Université de Poitiers ; Pierre-Emmanuel Hladik, Maître de conférences, INSA de Toulouse ; Olivier-Henri Roux, Professeur des universités, Centrale Nantes

Résumé : L’implémentation d’une nouvelle politique d’ordonnancement au sein d’un système d’exploitation temps réel n’est pas une tâche facile. Le passage de la spécification littéraire abstraite d’une politique à mise en oeuvre sur une plateforme réelle exige que des choix de réalisation soient faits et que des contraintes de diverses natures inhérentes à cette dernière soient prises en compte. Par conséquent, l’implémentation d’un ordonnanceur doit impérativement être accompagnée d’un travail de vérification permettant d’apporter un niveau de confiance en la validant la conformité du comportement de l’ordonnanceur implémenté par rapport à sa spécification d’origine.
Dans cette thèse, nous nous intéressons à l’utilisation des méthodes formelles pour la vérification des implémentations d’ordonnanceurs temps réel. Nous proposons une approche de vérification de type « model-checking », que nous conduisons sur des implémentations d’ordonnanceurs globaux menées au sein de Trampoline, un système d’exploitation temps réel conforme aux standardx OSEK/VDX et AUTOSAR. Pour chaque implémentation, un modèle décrivant son fonctionnement est élaboré avec des machines à états finis et temporisées. Ce modèle est stimulé par des générateurs produisant des scénarios indéterministes d’événements d’ordonnancement afin d’observer la réaction de l’implémentation à vérifier face à diverses situations. La vérification est alors menée en examinant la satisfaction d’une ensemble d’exigences spécifiées en fonction du comportement attendu de l’implémentation tel que stipulé dans la littérature. Cette approche a permis la vérification de la correction fonctionnelle du comportement de deux implémentations d’ordonnanceurs globaux dans Trampoline : G-EDF et EDF-US. Toutefois, son caractère modulaire et générique permet d’en envisager l’usage pour d’autres politiques et dans d’autres systèmes d’exploitation

Mots-clés : Politique d’ordonnancement temps réel, système d’exploitation temps réel, Implémentation d’ordonnancement, Model-checking

———————————————————————————————————————————————————

Abstract: Implementing a new scheduling policy within a real-time operating system is not an easy rask. Moving from an abstract literary specification of a policy to its implementation within a real platform requires making choices of realization and considering various contraints inherent to the latter. Consequently, a scheduler implementation work shall imperatively be supported by a verification study allowing to bring a level of confidence by validating the conformity of the behavior of the implemented scheduler compared to its original specification. In this thesis, we are interested in the use of formal methods for the verification of real-time scheduler implementations. We propose a « modelchecking » approach, which we conduct on global
scheduler implementations carried out on Trampoline, a real-time operating system compliant with OSEK/VDX and AUTOSAR standards. For each implementation, a model describing its behavior is elaborated with finite state and timed machines. This model is stimulated by generators producing indeterministic scenarios of scheduling events in order to observe the reaction of the implementation under various situations. The verification is then conducted by examining the satisfaction of a set of specified requirements according to the expected behavior of the implementation as stipulated in the literature.
This approach allowed the verification of the functional correction of the behavior of two implementations of global schedulers in Trampoline: G-EDF and EDF-US. However, its modular and generic character allows to consider its use for other policies and in other operating systems.

Keywords: Real-time scheduling policy, Real-time operating system, Scheduer implementation, Model-checking

Archives