Home » évènement

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

Journées annuelles du groupe de travail Vérification du GDR Informatique et Mathématiques

Les prochaines journées annuelles du GT Vérif auront lieu du 17 au 19 juin 2019 au bâtiment S sur le site de Centrale Nantes.

Elles visent à rassembler la communauté française en vérification formelle, et en particulier les chercheurs juniors, doctorants et post-doctorants, avec pour objectif de favoriser les collaborations et l’ouverture sur des thématiques liées à la vérification. Les domaines inclus sont :

  • la vérification informatique de systèmes, modélisant des systèmes de freinage aux protocoles de communications en passant par les programmes,
  • l’emploi de techniques de preuve automatiques ou interactives (model-checking, déduction automatique, assistants de preuve, solveurs SMT, etc. ainsi que leurs combinaisons),
  • l’utilisation de logiques pour raisonner sur les propriétés des systèmes (par exemple les logiques temporelles, spatiales, probabilistes ou avec données),
  • les techniques d’abstraction pour la vérification.

Programme :

  • Mardi 18/06 16:10-17:00 : Olivier H. Roux (LS2N) : Model-checking real-time systems with Roméo
  • Mercredi 19/06 9:00-9:50 : Charlotte Truchet (LS2N) et Ghiles Ziat (LIP6) : Programmation par contraintes et interprétation abstraite

Pour plus d’infos, voir le site http://gt-verif.loria.fr/Wiki.jsp?page=JA-2019

Soutenance de thèse de Yrvann EMZIVAT (équipe STR)

Yrvann Emzivat, soutiendra sa thèse intitulée « Architecture d’un organe de Survie pour la conception de Véhicules Autonomes Agiles et Sûrs »
mercredi 30 mai 2018 à 14h dans l’amphi du bâtiment S sur le site de Centrale.

Jury :

Rapporteurs :
Mme Claire PAGETTI, Ingénieur de Recherche, ONERA
M. Fawzi NASHASHIBI, Directeur de Recherche, INRIA Rocquencourt

Examinateurs :
M. Philippe BONNIFAIT, Professeur des Universités, Université de Technologie de Compiègne
M. Javier IBANEZ-GUZMAN, Expert véhicule autonome, Renault

Directeurs de thèse :
M. Olivier H. ROUX, Professeur des Universités, École Centrale de Nantes
M. Philippe MARTINET, Directeur de Recherche, INRIA Sophia Antipolis

Résumé :

L’automatisation de la tâche de conduite s’inscrit dans un contexte de développement d’une mobilité durable. Il s’agit d’une solution prometteuse qui pourrait bien contribuer à la création de nouveaux moyens de transports sûrs et respectueux de l’environnement. Cependant, concevoir un véhicule autonome reste un défi majeur. C’est pour cette raison qu’il incombe aujourd’hui à l’utilisateur de reprendre le contrôle du véhicule à chaque fois que les
circonstances s’y prêtent. Il semble pourtant peu judicieux de confier une telle responsabilité à un être humain dont l’implication dans la tâche de conduite est moindre. Les travaux menés dans le cadre de cette thèse portent sur la conception de véhicules autonomes habiles et sûrs. C’est plus précisément le développement d’un système capable de gérer de potentielles défaillances seul, d’élaborer des stratégies de repli par lui-même et de s’adapter à un environnement complexe qui est abordé ici.

Mots-clés : véhicules autonomes, sûreté de fonctionnement, architecture, modes dégradés, échappatoire, adaptabilité

********

Title : Safety System Architecture for the Design of Dependable and Adaptable Autonomous Vehicles

Abstract:

Driving automation is often presented as a viable solution to the prevailing challenges of sustainable mobility. It has the potential to create a paradigm shift in transportation technology, by providing a medium for cleaner, safer and more efficient means of transportation, while providing a better user experience overall. However, designing a dependable Automated Driving System is a challenge in itself. Current systems lack common sense and have trouble behaving in a truly cautionary manner, which is why a fallback-ready user is expected to take over in the event of a performance-relevant system failure affecting the dynamic driving task. Yet it seems unwise to rely on human drivers to act as a safety net for the purpose of offsetting the lack of maturity of Automated Driving Systems, for automation changes their active involvement into a monitoring role and creates new challenges, such as complacency, automation dependency, lack of understanding and misuse. This work places emphasis on the design of dependable and adaptable Automated Driving Systems. In particular, the thesis addresses the problem of designing a new ADS primary subsystem, whose role it is to monitor the state of the ADS, supervise its actions and respond as needed to guarantee the safety of its occupants and of others.

Keywords: autonomous vehicles, safety, architecture, graceful degradation, fallback strategy, adaptability

Khaoula BOUKIR (équipe STR) arrive 2ème à la finale nantaise de MT180 !

Khaoula Boukir, doctorante de 2ème année au sein de l’équipe STR, concourait le 13 février dernier à la finale nantaise de « Ma thèse en 180 secondes ». Arrivée seconde avec son sujet « politiques d’ordonnancement temps réel multiprocesseur prouvées », elle participera donc à la finale régionale de MT180. Bonne chance à elle !

Soutenance de thèse de Rola EL OSTA

Rola El Osta (équipe STR) soutiendra sa thèse intitulée : « Contribution to real time scheduling for energy autonomous systems »

jeudi 26 octobre 2017 à 14h30, à l’IUT de Carquefou – salle D1/26.

Jury : M. Mathieu JAN (Ingénieur de Recherche, HDR au CEA, Rapporteur), M. Daniel CHILLET (Professeur à l’université de Rennes 1, Rapporteur), M. Abdelhamid MELLOUK (Professeur à l’université de Paris 12, Examinateur), M. Hussein EL GHOR (Maître de conférences à l’IUT de Saida – Université libanaise, Examinateur),  M. Rafic HAGE (Professeur à l’IUT de Saida – Université libanaise, Examinateur), Mme Maryline CHETTO (Professeure à l’université de Nantes, Directrice de thèse).

Résumé :
Aujourd’hui, la récupération d’énergie renouvelable (energy harvesting) comme celle envisagée pour de nombreux objets sans fil, rend possible un fonctionnement quasi-perpétuel de ces systèmes, sans intervention humaine, car sans recharge périodique de batterie ou de pile. Concevoir ce type de système autonome d’un point de vue énergétique devient très
complexe lorsque celui-ci a en plus un comportement contraint par le temps et en particulier doit respecter des échéances de fin d’exécution au plus tard.
Comme pour tout système temps réel, une problématique incontournable est de trouver un mécanisme d’ordonnancement dynamique capable de prendre en compte conjointement deux contraintes clés : le temps et l’énergie. Dans cette thèse, nous nous intéressons à l’ordonnancement de tâches mixtes constituées de tâches périodiques et de tâches apériodiques souples sans échéance, tout en répondant à une question clé: comment servir les tâches apériodiques pour minimiser leur temps de réponse sans remettre en
question la faisabilité des tâches périodiques. Nous considérons un système monoprocesseur monofréquence, alimenté par un réservoir d’énergie approvisionné par une source environnementale. Dans ce cadre, nous avons proposé quatre nouveaux serveurs de tâches apériodiques utilisables avec l’ordonnanceur optimal ED-H. L’étude a comporté une phase de validation théorique puis une étude de simulation.

Mots- clés : Earliest Deadline First, récupération d’énergie, service apériodique, ordonnancement préemptif.

Abstract:
Nowadays, renewable energy harvesting such as that envisaged for many wireless things, allows the quasi-perpetual systems operation without human intervention because it works without periodic recharging of battery.
From an energy point of view, the design of this type of autonomous system becomes more complex since this process has in addition a behavior constrained by time, and particularly has to meet latest timing deadlines. As with any real-time system, an unavoidable problem is to find a dynamic scheduling mechanism able of considering jointly two key constraints: time and energy. In this thesis, we focus on scheduling of mixed tasks consisting of periodic tasks and soft aperiodic tasks without deadline, by providing
appropriate solutions for the following question: how to serve aperiodic tasks in order to minimize their response time without challenging the feasibility of periodic tasks. We consider a single-frequency uniprocessor system, powered by an energy reservoir which is charged through an ambient energy source. In this context, four new aperiodic task servers were proposed, based on the optimal scheduler ED-H. A theoretical analysis was performed with validation by a simulation study.

Keywords: Earliest Deadline First, energy harvesting, aperiodic servicing, preemptive scheduling.

Copyright : LS2N 2017 - Mentions Légales - 
 -