Home » Évènement (Page 7)

Soutenance de thèse de Vincent Raveneau (équipe DUKe)

Vincent Raveneau, doctorant au sein de l’équipe DUKe, soutiendra sa thèse intitulée « Interaction en Analyse Visuelle Progressive. Une application à la fouille progressive de motifs séquentiels » / « Interaction in Progressive Visual Analytics. An application to progressive sequential pattern mining«

mercredi 4 novembre 2020 à 15h30 à Polytech. Diffusion en direct sur Youtube : https://vraveneau.github.io/

Jury :
– Directeur thèse : Yannick Prié
– Co- encadrant : Julien Blanchard
– Rapporteurs : Adam Perer (Carengie Mellon University), Nicolas Labroche (U Tours/LIFAT)
– Autres membres : Béatrice Daille, Jean Daniel (Inria Saclay)

Résumé : Le paradigme de Progressive Visual Analytics (PVA) a été proposé en réponse aux difficultés rencontrées par les Visual Analytics lors du traitement de données massives ou de l’utilisation d’algorithmes longs, par l’usage de résultats intermédiaires et par l’interaction entre humains et algorithmes en cours d’exécution. Nous nous intéressons d’abord à la notion d’“interaction”, mal définie en PVA, dans le but d’établir une vision structurée de ce qu’est l’interaction avec un algorithme en PVA. Nous nous intéressons ensuite à la conception et à l’implémentation d’un système et d’un algorithme progressif de fouille de motifs séquentiels, qui permettent d’explorer à la fois les motifs et les données sous-jacentes, en nous concentrant sur les interactions entre analyste et algorithme. Nos travaux ouvrent des perspectives concernant 1/ l’assistance de l’analyste dans ses interactions avec un algorithme dans un contexte de PVA; 2/ une exploration poussée des interactions en PVA; 3/ la création d’algorithmes native- ment progressifs, ayant la progressivité et les
interactions au cœur de leur conception.

Mots-clés : Analyse Visuelle Progressive, Fouille Progressive de Motifs, Fouille de Motifs Séquentiels, Interaction, Données Séquentielles

Abstract: The Progressive Visual Analytics (PVA) paradigm has been proposed to alleviate difficulties of Visual Analytics when dealing with large datasets or time-consuming algorithms, by using intermediate results and interactions between the human and the running algorithm. Our work is twofold. First, by considering that the notion of “interaction” was not well defined for PVA, we focused on providing a structured vision of what in- teracting with an algorithm in PVA means. Second, we focused on the design and implementation of a progressive sequential pattern mining algorithm and system, allowing to explore both the patterns and the underlying data, with a focus on the analyst/algorithm interactions. The perspectives opened by our work deal with 1/ assisting analysts in their interactions with algorithm in PVA setting s; 2/ further exploring interaction in PVA ; 3/ creating natively progressive algorithms, for which progressiveness and interaction are at the core of the design.

Keywords: Progressive Visual Analytics, Progressive Pattern Mining, Sequential Pattern Mining, Interaction, Sequential Data

Soutenance de thèse d’Aurélie Moyon (équipes PACCE/RoMaS)

Aurélie Moyon, doctorante au sein des équipes PACCE et RoMaS, soutiendra sa thèse intitulée « Vers l’humain préservé : apports des facteurs humains pour une meilleure intégration des exosquelettes dans l’industrie » / « Toward preserved human: Human Factors benefits for a better integration of exoskeletons in Industry »

jeudi 8 octobre 2020 à 10h en visio.

Jury :
– Directrice de thèse / Co-directeur : Emilie Poirson et Jean-François Petiot
– Co-encadrant : Sébastien Leloch
– Rapporteurs : Jean-Claude Sagot (UTBM), Guillaume Thomann (G-SCOP)
– Autres membres : Jérémy Legardeur (ESTIA)

Résumé : Dans l’industrie, certaines tâches manuelles favorisent des postures pénibles et répétitives. Dans ce contexte, les exosquelettes sont considérés comme une promesse technique intéressante pour soulager la pénibilité au travail, mais soulèvent plusieurs verrous relevant des facteurs humains. Il est donc indispensable de mesurer les bénéfices réels du port de l’exosquelette, et de comprendre les facteurs qui contribuent à son acceptation par les futurs utilisateurs. Les objectifs de cette thèse sont d’investiguer les effets du port d’un exosquelette, de mieux comprendre les facteurs d’acceptation des utilisateurs finaux ainsi que d’établir des règles et outils repères pour une meilleure intégration des exosquelettes industriels. Ce travail de recherche présente l’étude des bénéfices d’un exosquelette passif, sur deux cas d’application industriels. Une démarche expérimentale centrée sur l’utilisateur permet d’identifier et de mesurer les facteurs d’acceptation de cette technologie. Des méthodes de mesures simples permettent de quantifier et de qualifier
les bénéfices du port de l’exosquelette. L’importance de la phase de familiarisation et des supports employés est mise en valeur par des expérimentions. Ces résultats alimentent un travail de normalisation avec un groupe de travail transdisciplinaire.

Mots-clés : Exosquelette, Ergonomie, Ingénierie des Facteurs Humains, Assistance à l’opérateur

Abstract: In industry, several manual tasks engage painful and repetitive postures. In this context, exoskeletons are seen as an interesting technical promise to relieve arduous work, but raise several human factors issues. It is therefore essential to measure the real benefits of wearing an exoskeleton, and to understand the factors that contribute to its acceptance by future users. The objectives of this thesis are to investigate the effects of wearing an exoskeleton, to better understand the factors contributing to the acceptance of the exoskeleton by future users, and to develop a better understanding of the effects of wearing an exoskeleton by end-users as well as to suggest new rules and tools for a better integration of industrial exoskeletons. This research work presents the study of the benefits of a passive exoskeleton, on two industrial case study. A user-centered experimental approach is used to identify and measure the acceptance factors of this technology. Simple measurement methods make it possible to quantify and qualify the benefits of wearing the exoskeleton. The importance of the familiarization phase and the support used is highlighted by experiments. These results contribute to a work of standardization with a transdisciplinary workgroup.

Keywords : Exoskeletons, Ergonomics, Human Factors Engineering, Occupational assistive systems

Soutenance de thèse d’Emile CADOREL (équipe STACK)

Emile Cadorel, doctorant au sein de l’équipe STACK, soutiendra sa thèse intitulée « Prise en compte de l’énergie dans la gestion des workflows scientifiques dans le Cloud : Une vision centrée sur le fournisseur de service » / « Energy-aware management of scientific workflows in the Cloud: A Cloud provider-centric vision »

mercredi 21 octobre 2020 à 13h00 dans l’amphi Besse sur le site de l’IMT-A.

Jury :
– Directeur thèse : Jean-Marc Menaud
– Co-encadrant ; Hélène Coullon
– Rapporteurs : Romain Rouvoy (U Lille), Patricia Stolf (IRIT-IUT Blagnac)
– Autres membres : Frédéric Desprez (LIG-Inria Rhône Alpes), Stéphane Genaud (U Strasbourg)
– Invités : Georges Da Costa (IRIT-U Sabatier)

Résumé : Les simulations scientifiques par ordinateur sont généralement très complexes et se caractérisent par de nombreux processus parallèles. Afin de mettre en évidence les parties parallèlisables, et de permettre une exécution efficace, de nombreux scientifiques ont choisi de définir leurs applications sous forme de workflows. Un workflow scientifique représente une application comme un ensemble de tâches de traitement unitaires, liées par des dépendances. De nos jours, grâce à leur faible coût, leur élasticité et leur aspect à la demande, les services de cloud computing sont largement utilisés pour l’exécution de workflows. Les utilisateurs utilisant ce type d’environnement gèrent l’exécution de leur workflow, ainsi que les ressources nécessaires, à l’aide de service standards tel que le IaaS (Infrastructure-as-a-Service). Néanmoins, comme les services de cloud ne sont pas
spécifiques à la nature de l’application à exécuter, l’utilisation des ressources physiques n’est pas aussi optimisée qu’elle pour- rait l’être. Dans cette thèse, nous proposons de déplacer la gestion et l’exécution des workflows du côté du fournisseur de Cloud afin d’offrir un nouveau type de service dédié aux workflows. Cette nouvelle approche rend possible une amélioration de la gestion des ressources et une réduction de la consommation d’énergie et de ce fait l’impact environnemental.

Mots-clés : Workflows scientifiques ; fournisseur de services de Cloud ; ordonnancement ; exécution ; optimisation energétique ; systèmes distribués ; infrastructures distribuées

Abstract: Scientific computer simulations are generally very complex and are characterized by many parallel processes. In order to highlight the parts that can be parallelized, and to enable efficient execution, many scientists have chosen to define their applica- tions as workflows. Ascientific workflow rep- resents an application as a set of unitary processing tasks, linked by dependencies. Today, because of their low cost, elasticity, and on demand nature, cloud computing services are widely used for workflow execution. Users using this type of environment manage the execution of their workflow, as well as the necessary resources, using standard services such as IaaS (Infrastructure-as-a-Service). However, because cloud services are not specific to the nature of the application to be executed, the use of physical resources is not as optimized as it could be. In this thesis, we propose to move the management and execution of workflows to the cloud provider’s side in order to offer a new type of service dedicated to workflows. This new approach makes it possible to improve resource management and reduce energy consumption and thus the envinmont impact.

Soutenance de thèse de Benjamin MOREAU (équipe GDD)

Benjamin Moreau, doctorant au sein de l’équipe GDD, soutiendra sa thèse intitulée « Faciliter la Réutilisation sur le Web des Données » / « Facilitating Reuse on the Web of Data »

vendredi 6 novembre 2020 à 14h en visio

Jury :
– Directeur thèse : Patricia Serrano Alvarado
– Co-encadrant : Emmanuel Desmontils
– Rapporteurs : Serena Villata (I3S), Olivier Cure (LIGM)
– Autres membres : Philippe Pucheral (U Versailles), Pascal Molli, Serge Garlatti (IMT-A Brest), Bernd Amann (LIP6)
– Invités : David Thoumas (Opendatasoft)

Résumé : Le Web des données est un ensemble de données liées qui peuvent être interrogées et réutilisées à l’aide de moteurs de requêtes fédérées. Pour protéger les jeux de données, les licences renseignent leurs conditions d’utilisation. Cependant, choisir une licence conforme n’est pas toujours aisé. En effet, pour protéger la réutilisation de plusieurs jeux de données, il est nécessaire de prendre en considération la compatibilité entre leurs licences. Pour faciliter la réutilisation, les moteurs de requêtes fédérées devraient respecter les licences. Dans ce contexte, nous nous intéressons à deux problèmes (1) comment calculer la relation de compatibilité entre des licences, et (2) comment respecter les licences pendant le traitement de requêtes fédérées. Pour le premier problème, nous proposons CaLi, un modèle capable d’ordonner partiellement n’importe quel ensemble de licences selon leur compatibilité. Pour le second problème, nous proposons FLiQue, un moteur de requête fédéré respectant les licences. FLiQue utilise CaLi pour détecter les conflits de compatibilité entre licences et assure que le résultat d’une requête fédérée respecte les licences. Dans le cadre de cette thèse, nous proposons également trois approches ODMTP, EvaMap et le SemanticBot ayant pour objectif de faciliter l’intégration de données au Web des Données.

Mots-clés : Web des données, données liées, RDF, SPARQL, licences, contrôle d’usage, traitement des requêtes fédérées, relâchement de requête, intégration de données, mappings RDF

—————————

Abstract: The Web of Data is a web of interlinked datasets that can be queried and reused through federated query engines. To protect
their datasets, data producers use licenses to specify their condition of reuse. But, choosing a compliant license is not easy. Licensing reuse of several licensed datasets must consider compatibility among licenses. To facilitate reuse, federated query engines should preserve license compliance. To do so, we focus on two problems (1) how to compute compatibility relations among licenses, and (2) how to ensure license compliance during federated query processing. To the first problem, we propose CaLi, a model that partially orders any set of licenses in terms of compatibility. To the second problem, we propose FLiQue, a license-aware federated query processing strategy. FLiQue uses CaLi to detect license compatibility conflicts and ensures that the result of a federated query preserves license compliance. Within the scope of this thesis, we also propose three approaches ODMTP, EvaMap, and the SemanticBot that aim to facilitate the integration of datasets to the Web of Data.

Keywords: Web of Data, Linked Data, RDF, SPARQL, licenses, usage control, federated query processing, query relaxation, data integration, RDF mappings

Soutenance de thèse de Renald GABORIAU (équipe ReV)

Renald Gaboriau, doctorant au sein de l’équipe ReV, soutiendra sa thèse intitulée « Les ateliers Rob’Autisme : le robot extension comme médiation thérapeutique auprès des personnes présentant un trouble du spectre autistique » / « The Rob’Autism groups : the extension robot as a therapeutic mediator for people with Autism Spectrum Disorder »

mercredi 23 septembre 2020 à partir de 16h00 en visio-conférence à l’École Centrale de Nantes.

Jury :
– Directrice de thèse : SAKKA Sophie, Maître de conférences HDR, École Centrale de Nantes
– Co-directeur de thèse : ACIER Didier, Professeur des universités, Université de Nantes
– Rapporteurs : DEVILLERS Laurence, Professeur des universités, Sorbonne Université / RABEYRON Thomas, Professeur des universités, Université de Lorraine
– Examinateurs : CHETOUANI Mohamed, Professeur des universités, Sorbonne Université / HAZA Marion, Maître de conférences HDR, Université de Poitiers

Résumé : L’utilisation des robots comme médiation thérapeutique pour les personnes présentant un Trouble du Spectre Autistique (TSA) est une pratique en plein essor. C’est en effet une méthode encourageante pour favoriser le développement de compétences sociales. De nombreuses expériences sont actuellement menées. Cependant, dans toutes les approches existantes, le paradigme du robot-compagnon est utilisé : le robot est programmé pour présenter des comportements pré-établis. Le projet Rob’Autisme propose une approche alternative : le robot est utilisé comme extension pour faire ou dire des choses. Les sujets présentant un TSA le programment et, par son truchement, agissent librement sur leur environnement social. De plus, ce projet inclut l’idée qu’ils pourront ensuite interagir avec les autres sans le robot. Cette thèse vise à comprendre l’intérêt de cette approche et évaluer les effets de la participation sur les interactions sociales. Durant deux ans, des groupes avec six adolescents ont été organisés et analysés à partir de méthodes quantitatives et qualitatives. Ces analyses montrent que cette approche favorise la tendance à aller vers les autres et interagir avec eux. Ce résultat est en outre généralisé à l’extérieur.

Mots-clés : Projet Rob’Autisme, robot-extension, autisme, groupe thérapeutique, médiation thérapeutique

—————-

Abstract: The use of robots as a therapeutic mediator for peolple with Autism Spectrum Disorder (ASD) is a topic which tends to develop. Indeed, it is a promising method to promote the development of social skills. Many experiments are carried out currently. But in all existing approaches, the companion robot paradigm is used : the robot is programmed to present some pre-established behaviors. Rob’Autism Project propose an alternative approach : the robot is used as an extension for doing or talking things. The autistic subjects program it and therefore act on the social environment freely. This project includes ideas that they will be able to interact with the others without the robot. This thesis aims to understand the interest of this approach and asses the effects of participation on the social interactions. During two years, groups have been set up and analyzed with quantitative and qualitative methods. These analysis show that this approach favors the tendency to go towards the others and interact with them. This result is generalized outside the group.

Keywords: Rob’Autism Project, extension-robot, autism, group therap, therapeutic mediator

Soutenance de thèse de Fatima ZAIDI (équipe SLP)

Fatima Zaidi, doctorante au sein de l’équipe SLP, soutiendra sa thèse intitulée « Development of statistical monitoring procedures for compositional data »

lundi 5 octobre 2020 à 9h en visioconférence.

Jury :
– Directeur thèse : Philippe Castagliola
– Rapporteurs : Stelios Psarakis (U Athenes), Biagio Palumbo (U Frederico II, Naples)
– Autres membres :Fernanda Otilia Figueiredo (U Porto), Marit Schoonhoven (Amsterdam Business School)

Soutenance de thèse d’Ilhem SLAMA (équipe SLP)

Ilhem SLAMA, doctorante au sein de l’équipe SLP, soutiendra sa thèse intitulée « Modélisation et optimisation du problème de planification de désassemblage dans un environnement incertain » / « Modeling and optimization of the disassembly planning problem under uncertainty »

vendredi 25 septembre 2020, dans l’amphi Georges Besse sur le site IMT-A.

Jury :
– Directeur thèse : Alexandre Dogui et Faouzi MASMOUDI Professeur, LA2MP, ENIS, Sfax
– Co-encadrant : Oussama BEN-AMMAR Maître-assistant associé, Mines Saint-Etienne
– Rapporteurs : Chu FENG Professeur, Université d’Evry – Olga BATTAIA Professeur, Business School de Bordeaux
– Autres membres : Abedlaziz DAMMAK Professeur, FSEG, Sfax – Malek MASMOUDI Maître de Conférences HDR, Université Jean-Monnet
– Invité : Lounes BENTAHA Maître de conférences, université de lumière, Lyon

Résumé : Pour tirer les intérêts économiques, notre projet de recherche propose de modéliser et d’optimiser le problème lié à la détermination du plan de démontage des produits en fin de vie tout en satisfaisant les demandes en composants sur un horizon de planification donné. Les travaux présentés dans ce manuscrit portent sur la planification de désassemblage dans un contexte certain et incertain. Nous avons considéré principalement trois modélisations principales avec leurs approches de résolution : (i) une modélisation déterministe multi-période qui traite une nomenclature de produit multi-niveaux avec le partage des composant qui cherche à maximiser le profit total, (ii) une modélisation stochastique mono-période, avec une nomenclature de produit à deux niveau et un seul type de produit. Les délais de remise à neuf sont supposés stochastiques. Le modèle cherche à minimiser l’espérance mathématique des coûts de stockage et de rupture des composants et (iii) le troisième modèle est une extension de deuxième modèle qui
cherche à traiter un problème multi-période avec une restriction de capacité des ressources. La programmation mixte en nombre entier, la modélisation analytique, la programmation stochastique et l’agrégation par scénarios sont pro- posées pour résoudre les modèles proposés. Les performances des méthodes de résolution développées sont présentées en analysant les résultats d’optimisation sur un ensemble d’instances générées aléatoirement.

Mots-clés : Désassemblage, planification de désassemblage, délai de désassemblage incertain, programmation stochastique, modélisation analytique, agrégation par scénarios

************

Abstract: Our research proposes to model and optimize the problem concerning the determination of the optimal disassembly plan for end-of-life products while satisfying the demands on components over a given planning horizon. The contributions presented in this manuscript focus on disassembly planning in a certain and uncertain context. We have considered three main models with their resolution approaches: (i) a deterministic multi-period modeling that deals with a multi-level product structure with a commonality of components that aims to maximize total profit. (ii) a single-period stochastic model with a two-level structure and a single end-of-life product type under random lead times. This model seeks to minimize the total expected cost, composed of inventory and backlog costs, and (iii) the third model is an extension of the second model which treats a multi-period problem with a resource capacity constraint. Mixed-integer programming, analytical modeling, stochastic programming, and scenario aggregation are proposed to solve the proposed models. The per- formances of the proposed resolution methods are presented by analyzing the optimization results on a set of randomly generated instances.

Keywords: disassembly, disassembly lot-sizing, random disassembly lead times, stochastic programming, analytical modeling, scenarios aggregation, simulation

Soutenance de thèse d’Abdramane BAH (équipe AeLoS)

Abdramane BAH, doctorant au sein de l’équipe AeLoS, soutiendra sa thèse intitulée « Interopérabilité et sécurité des systèmes » / « Interoperability and security of systems »

jeudi 8 octobre 2020 à 10h en visio depuis le Mali – Lien zoom : https://us02web.zoom.us/j/89366097578. Possibilité d’assister à la soutenance depuis la salle 3 du bâtiment 11 sur le site FST.

Jury :
– Directeur thèse : Christian Attiogbé
– Co-encadrants : Pascal André ; Jacqueline Konaté, Maître Assistant, Université des Sciences et des Techniques de Bamako
– Rapporteurs : Florence Sedes, Professeure, Université de Toulouse III ; Philippe ANIORTE, Professeur, Université de Pau
– Autres membres : Jean-Paul BODEVEIX, Professeur, Université de Toulouse III

Resumé : Le contrôle d’accès des services partagés est une exigence essentielle pour une fédération de services de différents domaines. Dans cette thèse, nous nous sommes attaqués à deux problèmes de contrôle d’accès : l’autorisation des utilisateurs et la délégation de l’authentiﬁcation des utilisateurs à leurs propres domaines. Pour répondre à ces problèmes, nous avons proposé une méthode d’autorisation des utilisateurs basée sur la technique de mapping d’attributs et un mécanisme de contrôle d’accès fédéré pour
mettre en oeuvre cette méthode d’autorisation. Nous avons proposé une méthode de fédération services pour déléguer l’authentiﬁcation des utilisateurs à leurs propres domaines. Le principal objectif est de permettre à divers domaines de collaborer malgré l’hétérogénéité de leurs modèles de sécurité.

Mot-clés : Fédération de domaines, Sécurité d’accès aux services, SOA

***********

Abstract: Access control for shared services is an essential requirement for a federation of services from different domains. In this thesis, we tackled two access control problems : authorizing users and delegating user authentication to their own domains. To address these problems, we have proposed a method of authorizing users
based on the attribute mapping technique and a federated access control mechanism to implement this authorization method. We have proposed a service federation method to delegate user authentication to their domains. The main objective is to allow various domains to collaborate despite the heterogeneity of their security models

Keywords: Federation of domains, Access control, SOA

Soutenance de thèse de Yang DENG (équipe Commande)

Yang Deng, doctorant au sein de l’équipe Commande, soutiendra sa thèse intitulée « Estimation du retard et commande prédictive des systèmes à retard avec une classe de retards divers » / « Delay estimation and predictor-based control of time-delay systems with a class of various delays »

mercredi 8 juillet à 10h30 en visioconférence sur Zoom (https://ec-nantes.zoom.us/j/96608195455) et se déroulera dans l’amphi du Bâtiment S de Centrale.

Jury :
– Jean-Pierre RICHARD, Professeur des université, Ecole Centrale de Lille
– Alexandre SEURET, Directeur de Recherche CNRS, LAAS Toulouse
– Pierdomenico PEPE, Professeur des universités, Université de L’Aquila, Italie
– Franck PLESTAN, Professeur des Universités, École Centrale de Nantes
– Emmanuel MOULAY, Chargé de Recherche CNRS-HdR, Université de Poitiers
– Vincent LECHAPPE, Maître de conférence, INSA Lyon

Résumé :
Le retard est un phénomène largement présent dans les systèmes de commande (i.e. retard physique, latence de communication, temps de calcul) et peut en dégrader les performances ou même les déstabiliser. Si le retard est faible, la stabilité en boucle fermée peut être garantie par des lois de commande conventionnelles mais ces techniques ne sont plus efficaces si le retard est long. Cette thèse est dédiée à la commande des systèmes à retard avec retards longs inconnus ou avec des retards incertains. Pour compenser les retards longs, la commande prédictive est adoptée et des techniques d’estimation de retard sont développées. Selon les différents types de systèmes et de retards, trois objectifs sont visés dans la thèse. Le premier objectif considère la commande des systèmes linéaires avec retards constants inconnus pour lesquels un nouvel estimateur de retard est proposé pour estimer les retards inconnus. Le retard estimé est ensuite utilisé dans la commande prédictive pour stabiliser le système. Le deuxième objectif se concentre sur la stabilisation pratique des systèmes commandés à distance avec des retards inconnus variants. Dans ce cas, les retards sont estimés de manière pratique : une boucle de communication spécifique est utilisée pour estimer le retard en temps fini puis le système est stabilisé par une commande prédictive. Les tests expérimentaux réalisés sur un réseau WiFi ont montré que l’algorithme permet d’estimer de manière robuste les retards variants. Le dernier objectif est consacré à la commande des systèmes commandés en réseau avec retards variants. La commande prédictive discrète est utilisée pour compenser les retards longs et variants et les réordonnancements de paquets dans le canal capteur-contrôleur sont également considérés. De plus, cette méthode est validée par l’asservissement visuel d’un pendule inverse commandé en réseau. Les performances obtenues sont meilleures que les méthodes de commande non-prédictives classique.

Mots-clés : Système à retard, retard long, estimation du retard, commande prédictive, système commandé en réseau

*************

Abstract: Time-delay is a widely-found phenomenon (i.e. physical dead time, communication latency, computation time) in real control systems, which can degrade the performances of the system or destabilize the system. If the time-delay is small, then the closed-loop stability can be guaranteed with conventional control techniques; but these techniques are no longer effective if the time-delay is long. This thesis is dedicated to the control of time-delay systems with unknown or uncertain long time-delays. In order to compensate long time-delays, the predictor-based control technique is adopted, and the delay estimation techniques are developed to assist the predictor-based controller. According to the different types of the systems and the time-delays, three objectives are analyzed in the thesis. The first objective considers the control of LTI systems with unknown constant delays, a new type of delay estimator is proposed to estimate the unknown time-delays, then it is plugged into a predictor-based controller to stabilize the system. The second objective focuses on the practical stabilization of remote control systems with unknown time-varying delays, at this time, the time-delays are estimated by a practical way: a specific communication loop is used to estimate the round-trip delay in finite time, and the system is stabilized with a predictor-based controller. This practical delay estimation algorithm is implemented on a real WiFi network, it can estimate the time-varying delays with good performances and robustness. The last objective is devoted to the control of networked control systems with time-varying delays, the discrete predictor-based control techniques are used to compensate long time-varying delays, and the packet reordering in the sensor-to-controller channel is also considered. Moreover, this control solution is validated on a networked visual servo inverted pendulum system, and the control performances are fairly better than the non-predictive control methods.

Keywords: Time-delay system, long delay, delay estimation, predictor-based control, networked control system.

Soutenance de thèse de Théo WINTERHALTER (équipe Gallinette)

Théo Winterhalter, doctorant au sein de l’équipe Gallinette, soutiendra sa thèse intitulée « Formalisation et Méta-Théorie de la Théorie des Types » / « Formalisation and Meta-Theory of Type Theory »

vendredi 18 septembre 2020 à 14h.

Jury :
– Directeur thèse : Nicolas Tabareau
– Co-encadrant : Mathieu Sozeau
– Rapporteurs : Andrej Bauer (U Ljubljana), Herman Geuvers (Raboud University, Nijmegen)
– Autres membres : Assia Mahboubi, Bas Spitters (Aarhus University), Andreas Abel (Goteborg University), Hugo Herbelin (U Paris Diderot), Gilles Dowek (ENS Paris Saclay)

Résumé : Dans cette thèse, je parle de la méta-théorie de la théorie des types et de la façon de la formaliser dans un assistant de preuve.
Je me concentre d’abord sur une traduction conservative de la théorie des types extensionnelle vers la théorie des types intensionnelle ou faible, entièrement écrite en Coq. La première traduction consiste en une suppression de la règle de reflection de l’égalité, tandis que la deuxième traduction produit quelque chose de plus fort : la théorie des types faibles est une théorie des types sans notion de conversion. Le résultat de conservativité implique que la conversion n’augmente pas la puissance logique de la théorie des
types.
Ensuite, je montre ma contribution au projet MetaCoq de formalisation et de spécification de Coq au sein de Coq. En particulier, j’ai travaillé sur l’implantation d’un vérificateur de type pour Coq, en Coq. Ce vérificateur de type est prouvé correct vis à vis de la spécification et peut être extrait en code OCaml et exécuté indépendamment du vérificateur de type du noyau de Coq. Pour que cela fonctionne, nous devons nous appuyer sur la métathéorie de Coq que nous développons, en partie, dans le projet MetaCoq. Cependant, en raison des théorèmes d’incomplétude de Gödel, nous ne pouvons pas prouver la cohérence de Coq dans Coq, ce qui signifie que certaines propriétés — principalement la forte normalisation — doivent être supposées, c’est-à-dire prises comme axiomes.

Mots-clés : théorie des types, formalisation, traduction de programme, vérification de type

********

Abstract: In this thesis, I talk about the metatheoryof type theory and about how to formalise it in a proof assistant.
I first focus on a conservative translation between extensional type theory and either intensional or weak type theory, entierely written in Coq. The first translation consists in a removal of the reflection of equalityr rule, whereas the second translation produces something stronger: weak type theory is a type theory with no notion of conversion. The conservativity result implies that conversion doesn’t increase the logical power of type theories.
Then, I show my work for the Meta- Coq project of formalising and specifying Coq within Coq. In particular I worked on writing a type-checker for Coq, in Coq. This type checker is proven sound with respect to the specification and can be extracted to OCaml code and run independently of Coq’s kernel type-checker. For this to work we have to rely on the meta-theory of Coq which we develop, in part, in the MetaCoq project. However, because of Gödel’s incompleteness theorems, we cannot prove consistency of Coq within Coq, and this means that some properties— mainly strong normalisation—have to be assumed, i.e. taken as axioms.

Keywords: type theory, extensionality, program translation, type checking

Archives