Home » Évènement (Page 8)

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

Soutenance de thèse de Dimitri ANTAKLY (équipes DUKe / AeLoS)

Dimitri Antakly, doctorant au sein des équipes DUKe et AeLoS, soutiendra sa thèse intitulée « Apprentissage et Vérification Statistique pour la Sécurité » / « Machine Learning and Statistical Verification for Security »

jeudi 2 juillet 2020 à 10h, sur le site de la FST au bâtiment 34 et en visio.

Jury :
– Directeur thèse : Leray Philippe
– Co-encadrant : Delahaye Benoit
– Rapporteurs : Schiex Thomas (INRAE Toulouse), Tabia Karim (Université d’Artois)
– Autres membres : Rouveirol Céline (Université Paris 13), Bertrand Nathalie (Inria Rennes)

Résumé : Les principaux objectifs poursuivis au cours de cette thèse sont en premier lieu de pouvoir combiner les avantages de l’apprentissage graphique probabiliste de modèles et de la vérification formelle afin de pouvoir construire une nouvelle stratégie pour les évaluations de sécurité. D’autre part, il s’agit d’évaluer la sécurité d’un système réel donné. Par conséquent, nous proposons une approche où un « Recursive Timescale Graphical Event Model (RTGEM) » appris d’après un flux d’évènements est considéré comme représentatif du système sous-jacent. Ce modèle est ensuite utilisé pour vérifier une propriété de sécurité. Si la propriété n’est pas vérifiée, nous proposons une méthodologie de
recherche afin de trouver un autre modèle qui la vérifiera. Nous analysons et justifions les différentes techniques utilisées dans notre approche et nous adaptons une mesure de distance entre Graphical Event Models. La mesure de distance entre le modèle appris et le proximal secure model trouvé nous donne un aperçu d’à quel point notre système réel est loin de vérifier la propriété donnée. Dans un souci d’exhaustivité, nous proposons des séries d’expériences sur des données de synthèse nous permettant de fournir des preuves
expérimentales que nous pouvons atteindre les objectifs visés.

Mots-clés : Apprentissage de modèles, Vérification formelle, Statistical Model Checking, Recursive Timescale Graphical Event Models, Flux d’événements, Evaluation de sécurité.

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

Abstract: The main objective of this thesis is to combine the advantages of probabilistic graphical model learning and formal verification in order to build a novel strategy for security assessments. The second objective is to assess the security of a given system by verifying whether it satisfies given properties and, if not, how far is it from satisfying them. We are interested in performing formal verification of this system based on event sequences collected from its execution. Consequently, we propose a model-based approach where a Recursive Timescale Graphical Event Model (RTGEM), learned from the event streams, is considered to be representative of the underlying system. This model is then used to check a security property. If the property is not verified, we propose a search methodology to find another close model that satisfies it. We discuss and justify the different techniques we use in our approach and we adapt a distance measure between Graphical Event Models. The distance measure between the learned « fittest » model and the found proximal secure model gives an insight on how far our real system is from verifying the given property. For the sake of completeness, we propose series of experiments on synthetic data allowing to provide experimental evidence that we can attain the goals.

Keywords: Model-based learning, Formal verification, Statistical Model Checking, Recursive Timescale Graphical Event Models (RTGEMs), Event streams, Security assessments.

Soutenance de thèse de Qiuyue LUO (équipe ReV)

Qiuyue Luo, doctorante au sein de l’équipe ReV, soutiendra sa thèse intitulée « Marche Bipède 3D Auto-Stabilisante » / « Self-stabilization of 3D walking of a biped robot »

jeudi 18 juin 2020 à 10h en visioconférence.

Jury :
– Rapporteurs : Olivier STASSE (Directeur de recherche, CNRS, LAAS, Toulouse), Andrea CHERUBINI (MC HDR, Associate Professor – LIRMM Université de Montpellier)
– Examinateurs: Jean Paul LAUMOND (Directeur de recherche CNRS émérite), Yannick AOUSTIN (Professeur Université de Nantes), Claude MOOG (Directeur de recherche CNRS)
– Directrice de thèse: Christine CHEVALLEREAU (Directrice de recherche CNRS)

Résumé : Les robots humanoïdes, bien adaptés pour évoluer dans le milieux humains, peuvent avec leurs bras et mains effectuer des tâches complexes. Ils peuvent être considérés comme l’un des robots ultimes. Cependant, la marche bipède reste un phénomène complexe qui n’a pas été entièrement compris.
La thèse est consacrée à trouver quelques caractéristiques physiques qui peuvent expliquer la stabilité de la marche périodique sur le sol horizontal. Dans la marche humaine, la démarche est généralement exprimée en fonction d’une variable de phase fondée sur l’état interne au lieu du temps. Les variables commandées (trajectoires du pied libre, oscillation verticale du centre de masse (CdM), mouvement du haut du corps, etc.) des robots ont une évolution désirée exprimée en fonction d’une variable de phase via l’utilisation de contraintes virtuelles et la durée des pas n’est pas explicitement imposée mais implicitement adaptée en présence de perturbations.
Dans la première partie, un modèle simplifié du robot: le modèle du pendule inversé linéaire (LIP) est utilisé pour étudier les stratégies de commande. L’influence du placement du pied libre sur le sol et les conditions de changement de jambe d’appui, en fonction du temps ou de l’état interne du robot sont étudiées. Il est montré que l’auto-synchronisation peut être obtenue lorsque la condition de transfert de la jambe d’appui est fondée sur une combinaison linéaire des positions du CdM le long des axes sagittal et frontal. De plus, l’auto-stabilisation peut être obtenue lorsque la vitesse du CdM dans le plan sagittal est prise en compte.
Afin d’analyser l’influence de l’oscillation verticale du CdM du robot sur la stabilité de marche, le modèle de pendule inversé de longueur variable (VLIP) est utilisé. Il est démontré que l’oscillation verticale du CdM, le placement du pied libre et le choix de la condition de transfert jouent un rôle crucial dans la stabilité.
Dans la dernière partie un nouveau modèle de marche, nommé le modèle essentiel est proposé. Il a la même dimension que le modèle 3D LIP mais il prend en compte la dynamique complète de l’humanoïde. Le modèle essentiel définit la dynamique de la position horizontale du CdM en fonction d’une trajectoire souhaitée du zéro moment point (ZMP). Les trajectoires de référence des variables commandées sont définies en fonction des états internes du robot et/ou d’informations externes, générant ainsi des modèles à des fins différentes. La stratégie de commande proposée pour les modèles LIP et VLIP est étendue à travers le modèle essentiel pour commander un modèle humanoïde complet.

Mots-clés : Humanoid and bipedal locomotion, passive walking, dynamic stability, hybrid systems, modeling

Abstract: Humanoid robot, which can walk by two legs and perform skillful tasks using both arms with hands, could be considered as one of the ultimate robots. However, bipedal walking remains a complex phenomenon that has not been fully understood.
The thesis is dedicated to find some physical insights that can explain the stability of periodic walking on horizontal floor. In human walking, the gait is usually expressed as a function of a phasing variable based on the internal state instead of time. The controlled variables (swing foot trajectories, vertical oscillation of center of mass (CoM), upper body motion, etc.) of the robots are based on a phasing variable via the use of virtual constraints and the step timing is not explicitly imposed but implicitly adapted under disturbances.
In the first part, a simplified model of the robot: the linear inverted pendulum (LIP) model is used to study control strategies. Landing positions of the swing foot, and conditions to switch the stance leg, based on time or on the internal state of the robot are studied. It is shown that self-synchronization can be obtained when the switching condition of the stance leg is based on a linear combination of the positions of the center of mass (CoM) along the sagittal and frontal axes. Moreover, self-stabilization can be obtained when the velocity of the CoM in the sagittal plane is taken into account
In order to analyze the influence of the vertical oscillation of the robot CoM on walking stability, the variable length inverted pendulum (VLIP) model is used. It is shown that the vertical CoM oscillation, the landing positions of the swing foot and the choice of the switching condition play a crucial role in stability.
In the last part, the essential model is proposed, which is a novel model for walking that has the same dimension as the 3D LIP model but considers the complete dynamics of the humanoid. The essential model defines the dynamics of the horizontal position of the CoM as a function of a desired trajectory of the ZMP. Reference trajectories of the controlled variables are defined based on the internal states of the robot and possible external information, thereby generating models for different purposes. The proposed control strategy for the LIP and VLIP models is extended through the essential model to control a complete humanoid model.

Keywords: Humanoid and bipedal locomotion, passive walking, dynamic stability, hybrid systems, modeling

Soutenance d’HDR de Dalila TAMZALIT (équipe NaoMod)

Dalila Tamzalit, maître de conférences au sein de l’équipe NaoMod, soutiendra son Habilitation à diriger des recherches intitulée « Vers une Ingénierie de l’Évolution Logicielle : une approche architecturale – Verrous, contributions et perspectives » / « Towards Engineering of Software Evolution : an architectural approach – issues, contributions and perspectives »

vendredi 26 juin 2020 à 14h en visio.

Le manuscrit est consultable sur le cloud.

Jury :
– Président du jury : Claude Jard
– Rapporteurs : Yamine Aït-Ameur (Professeur, IRIT / INPT-ENSEEIHT Toulouse), Marianne Huchard (Professeure, LIRMM / Université Montpellier), Houari Sahraoui (Professeur, Dpt d’informatique et recherche opérationnelle / Université de Montréal)
– Membres : Mireille Blay-Fornarino (Professeure, I3S / Université de Nice), Xavier Blanc (Professeur, LaBRI / Université de Bordeaux), Mourad Oussalah (Professeur, LS2N / Université de Nantes), Yves Caseau (Group chief information officer / Michelein Clermont-Ferrand)

Résumé :
Les travaux de recherche, présentés dans le cadre de mon projet d’Habilitation à diriger des Recherches, s’inscrivent dans la problématique générale de l’évolution des Architectures Logicielles. Il est à souligner que le terme évolution s’entend au sens large : migration, adaptation, refactoring, rétro-conception, réingénierie, restructuration, maintenance, traçabilité… Chacun de ces travaux est présenté selon son contexte, les verrous scientifiques qu’il traite, les principales contributions ainsi que sa validation et sa valorisation au travers de publications. Il est à noter qu’ils suivent un même fil conducteur, celui de prôner une Ingénierie de l’évolution des architectures logicielles, en termes de fondements, modèles et méthodologies. Ainsi, mes travaux de recherche s’articulent autour de la spécification et la formalisation : (i) des architectures logicielles évolutives et (ii) des architectures de l’évolution logicielle. La principale ligne directrice est d’identifier et de cerner les caractéristiques intrinsèques de systèmes logiciels afin de spécifier et gérer leur évolution indépendamment de leur fonctionnement. Pour y arriver, le principe clé adopté est celui de la séparation stricte des préoccupations de l’évolution des autres préoccupations. Il est couplé à une approche par abstraction (métamodèles et méthodologies). En couplant ce principe et cette approche, il a été ainsi possible de réifier différentes préoccupations liées à l’évolution sous forme de concepts statiques (modèles) et dynamiques (processus) à un haut niveau d’abstraction, permettant une représentativité aux niveaux stratégiques de décision, tout en offrant une assistance aux architectes. Ces travaux ont concerné différents paradigmes d’architectures logicielles : depuis l’objet durant ma thèse, aux composants en passant par la SOA et en considérant les styles architecturaux SaaS mutualisé et micro-services. Ces travaux ont été menés au travers d’encadrement et de co-encadrement doctoral de 9 thèses et 11 Master2, ainsi que des collaborations avec des confrères français, européens, internationaux et avec des entreprises.
Les travaux présentés ne sont qu’une partie de mes travaux de recherche, ceux portant sur et pour les problématiques d’évolution des architectures logicielles à base de composants et autour de la notion de service (SOA), notamment les styles architecturaux SaaS mutualisé et micro-services. La raison est double : ces travaux constituent l’essentiel de mes activités de recherche et mes projets futurs s’inscrivent dans leur continuité. De 2002 à 2010, ils ont porté sur les architectures logicielles à base de composants au travers de leurs langages de description, les ADLs (Architecture Description Languages). Les principales contributions ont été de proposer (1) un modèle générique pour l’évolution structurelle d’architectures logicielles, (2) un modèle de capitalisation de savoir-faire d’évolutions architecturales, (3) une approche d’extraction d’architectures logicielles à partir de systèmes objets patrimoniaux ainsi que (4) des patrons d’évolution architecturale. De 2010 à aujourd’hui, mes travaux ont porté sur les architectures logicielles autour de la notion de service (SOA, SaaS, micro-services). Les principales contributions ont été de proposer (5) un modèle d’externalisation de la gestion de la variabilité d’applications SaaS mutualisées, (6) une approche SOA de restructuration et d’adaptation de workflows d’entreprise ainsi que (7) la migration de systèmes monolithes vers des architectures micro-services.
Enfin, différentes perspectives explicitent mon projet scientifique intitulé « vers une industrialisation de l’évolution logicielle » afin de prendre en compte le contexte des nouvelles générations d’architectures logicielles. L’objectif est de tendre vers des systèmes logiciels durables dans le temps, en augmentant leur espérance de vie, idéalement de manière continue. J’attache également à ce projet des pistes qui me paraissent d’importance : la formation universitaire et les collaborations avec le monde socio-économique.

Mots-clés : Architectures Logicielles, Évolution Logicielle, Migration, Adaptation, Réification et Réutilisation des connaissances d’évolution, Styles et Patrons d’Évolution, Architectures Orientées Services (SOA), SaaS mutualisé, Variabilité, Externalisation, Micro-Services.

Abstract:
The research work, presented in the context of my Habilitation à diriger des Recherches (HdR), is part of the general field of Software Architectures evolution. The term evolution is considered in a broad sense: migration, adaptation, refactoring, reverse engineering, reengineering, restructuring, maintenance, traceability… Each of these research works is presented according to its context, the addressed scientific issues, the main contributions as well as its validation and valorisation through publications. They follow the same common idea: advocating an Engineering of software architecture evolution, in terms of foundations, models and methodologies. Thus, my research work is based on the specification and formalisation of: (i) evolving software architectures and (ii) software architectures for evolution. The main guideline is to identify and define the intrinsic features of software systems in order to specify and manage their evolution independently of their operation. To achieve this, the key principle adopted is the strict separation of evolution concerns from other concerns. It is coupled with an abstraction approach (metamodels and methodologies). By coupling this principle and this approach, it has thus been possible to reify different concerns related to evolution in the form of static (models) and dynamic (processes) concepts at a high level of abstraction, allowing representativeness at strategic levels of decision making, while offering assistance to architects. This work has concerned different paradigms of software architectures: from the object during my PhD, to components, then through SOA and considering the SaaS multitenant and micro-services architectural styles. These research works were made possible and have been carried out through the supervision and co-supervision of 9 PhD and 11 Master2 students, as well as collaborations with French, European and international colleagues and also with companies.
The presented works are only a part of my research work, those dealing with and for the evolution of component-based software architectures and around the notion of service (SOA), in particular the SaaS multitenant and micro-services architectural styles. The reason is twofold: these works represent the main part of my research activities and my future projects are in line with them. From 2002 to 2010, they focused on component-based software architectures through their description languages, the ADLs (Architecture Description Languages). The main contributions have been to propose (1) a generic model for the structural evolution of software architectures, (2) a model for capitalising know-how of architectural evolutions, (3) an approach for extracting software architectures from legacy object systems and (4) architectural evolution patterns. From 2010 to today, my work has focused on software architectures around the notion of service (SOA, SaaS, micro-services). The main contributions have been to propose (5) an outsourcing model for managing the variability of SaaS multitenant applications, (6) an SOA approach for restructuring and adapting business workflows and (7) the migration of monolithic systems to micro-services architectures.
Finally, different perspectives outline my scientific project entitled « Towards an industrialization of software evolution » in order to take into account the context of new generations of software architectures. The objective is to move towards software systems that are sustainable over time, by increasing their life expectancy, ideally in a continuous manner. I also attach importance to this project in terms of university training and collaboration with the socio-economic world.

Keywords: Software Architectures, Software Evolution, Migration, Adaptation, Reification and Reuse of Evolution Knowledge, Evolution Styles and Patterns, Service Oriented Architectures (SOA), Shared SaaS, Variability, Outsourcing, Micro-Services.

Soutenance de thèse de Saman LESSANIBAHRI (équipe RoMaS)

La soutenance de thèse de Saman Lessanibahri, doctorant au sein de l’équipe RoMaS, intitulée « Robots parallèles à câbles ayant un grand espace de travail en translation et en orientation » / « Cable-Driven Parallel Robots with Large Translation and Orientation Workspaces »

aura lieu mardi 12 mai 2020 à 14h (en visio).

Jury :

Directeur thèse : CARO Stéphane
Co-directeur : CARDOU Philippe (Université Laval, Quebec)
Rapporteurs : GOUTTEFARDE Marc (LIRMM), LARIBI Med Amine (Université de Poitiers)
Autres membres : GERMAIN Coralie (Agro-campus Ouest), LAU Darwin (Université Chinoise de Hong-Kong)

Résumé : Les Robots Parallèles à Câbles (RPC) sont également considérés comme des manipulateurs parallèles avec des câbles flexibles au lieu de liens rigides. Un RPC se compose d’un châssis de base, d’une plateforme mobile et d’un jeu de câbles reliant en parallèle la plate-forme mobile au châssis de base. Les RPC sont réputés pour leurs performances avantageuses par rapport aux robots parallèles classiques en termes de grand espace de travail de translation, de reconfigurabilité, de grande capacité de charge utile et de performances dynamiques élevées. Ils ont attiré l’intérêt de l’industrie en raison de leurs avantages et de leurs capacités fondamentales. Cependant, la plupart des RPC ne fournissentque des amplitudes de rotation limitées de laplate-forme mobile en raison des collisions entre les câbles et les pièces mobiles.
L’objectif de cette thèse est de concevoir, d’analyser et de construire des RPC hybrides pour élargir l’espace de travail d’orientation en plus de leur grand espace de translation en exploitant les boucles de câbles. Ce travail de recherche présente le développement de RPC hybrides avec un espace de travail d’orientation considérablement augmenté qui combine les avantages d’un grand espace de travail de translation des RPC et de grandes amplitudes de rotation des poignets actifs.

Mots-clés : robot parallèle à câbles, robots hybrides, espace de travail, boucles de câbles, conception

***********
Abstract: Cable-Driven Parallel Robots (CDPRs) also noted as wire-driven robots are parallel manipulators with flexible cables instead of rigid links. A CDPR consists of a base frame, a moving-platform and a set of cables connecting in parallel the moving-platform to the base frame. CDPRs are well-known for their advantageous performance over classical parallel robots in terms of large translation workspace, reconfigurability, large payload capacity and high dynamic performance. They have drawn interests towards industry thanks to their fundamental advantages and capabilities. However, most of the CDPRs provide only limited amplitudes of rotation of the movingplatform due to collisions between the cables and the moving parts. The objective of this thesis is to design, analyze and build hybrid CDPRs to enlarge the orientation workspace in addition to their large translation workspace by exploiting cableloops. This research work presents development of hybrid CDPRs with drastically augmented orientation workspac which combine advantages of large translation workspace of CDPRs and large rotational amplitudes of active wrists.

Keywords: Cable-Driven Parallel Robots, Hybrid Robots, Workspace, Cable loops, Design

Soutenance de thèse de Sébastien LEVILLY (équipe SIMS)

Sébastien Levilly, doctorant au sein de l’équipe SIMS, soutiendra sa thèse intitulée « Quantification de biomarqueurs hémodynamiques en imagerie cardiovasculaire par résonance magnétique de flux 4D » / « Hemodynamic biomarkers quantification in cardiovascular imaging by 4D phase-contrast magnetic resonance »
mardi 12 mai 2020 à 14h à en visio-conférence à l’ECN.

Jury :
– Directeur thèse : Idier Jérôme
– Co-directeur : Paul-Guilloteaux Perrine (IRS UN)
– Rapporteurs : Heinrich Christian (Telecom Physique Strasbourg), Kachenoura Nadjia (UMPC)
– Autres membres : Sigovan Monica (INSA Lyon), Memin Etienne (Inria Rennes)
– Membre invité : Serfaty Jean-Michel (IRS UN)

Résumé :
En imagerie cardiovasculaire, un biomarqueur est une information quantitative permettant d’établir une corrélation avec la présence ou le développement d’une pathologie cardiovasculaire. Ces biomarqueurs sont généralement obtenus grâce à l’imagerie de l’anatomie et du flux sanguin. Récemment, la séquence d’acquisition d’IRM de flux 4D a ouvert la voie à la mesure du flux sanguin dans un volume 3D au cours du cycle cardiaque. Or, ce type d’acquisition résulte d’un compromis entre le rapport signal sur bruit, la résolution et le temps d’acquisition. Le temps d’acquisition est limité et par conséquent les données sont bruitées et sous-résolues. Dans ce contexte, la quantification de biomarqueurs est difficile. L’objectif de cette thèse est d’améliorer la quantification de biomarqueurs et en particulier du cisaillement à la paroi. Deux stratégies ont été mises en œuvre pour atteindre cet objectif. Une première solution permettant le filtrage spatio-temporel du champ de vitesse a été proposée. Cette dernière a révélé l’importance de la paroi dans la modélisation d’un champ de vitesse. Une seconde approche, constituant la contribution majeure de cette thèse, s’est focalisée sur la conception d’un algorithme estimant le cisaillement à la paroi. L’algorithme, nommé PaLMA, s’appuie sur la modélisation locale de la paroi pour construire un modèle de vitesse autour d’un point d’intérêt. Le cisaillement est évalué à partir du modèle de la vitesse. Cet algorithme intègre une étape de régularisation a posteriori améliorant la quantification du cisaillement à la paroi. Par ailleurs, une approximation du filtre IRM est utilisée pour la première fois pour l’estimation du cisaillement. Enfin, cet algorithme a été évalué sur des données synthétiques, avec des écoulements complexes au sein de carotides, en fonction du niveau de bruit, de la résolution et de la segmentation. Il permet d’atteindre des performances supérieures à une méthode de référence dans le domaine, dans un contexte représentatif de la pratique clinique.

Mots-clés : cisaillement à la paroi, simulation numérique des fluides, IRM de flux 4D, carotide

**********

Abstract:
In cardiovascular imaging, a biomarker is quantitative information correlated with an existing or growing cardiovascular pathology. Biomarkers are generally obtained by anatomy and blood flow imaging. Recently, the 4D Flow MRI sequence opened new opportunities in measuring the blood flow within a 3D volume along the cardiac cycle. However, this sequence is a compromise between signal-to-noise ratio, resolution and acquisition time. Allocated time being limited, velocity measurements are noisy and low resolution. In that context, biomarkers’ quantification is challenging. This thesis’s purpose is to enhance biomarkers’ quantification and particularly for the wall shear stress (WSS). Two strategies have been investigated to reach that objective. A first solution allowing the spatiotemporal filtering of the velocity field has been proposed.
It revealed the importance of the wall for the velocity field modelization. A second approach, being the major contribution of this work, focused on the design of a WSS quantification algorithm. This algorithm, named PaLMA, is based on the local modelization of the wall to build a velocity model near a point of interest. The WSS is computed from the velocity model. This algorithm embeds an a posteriori regularization step to improve the WSS quantification. Besides, a blurring model of 4D Flow MRI is used for the first time in the WSS quantification context. Finally, this algorithm has been validated over synthetic datasets, with carotids’ complex flows, concerning the signal-to-noise ratio, the resolution, and the segmentation. The performances of PaLMA are superior to a reference solution in that domain, within a clinical routine context.

Keywords: wall shear stress, computational fluid dynamics, 4D Flow MRI, carotid

Soutenance de thèse de Ramzi BEN MHENNI (équipe SIMS)

Ramzi Ben Mhenni, doctorant au sein de l’équipe SIMS, soutiendra sa thèse intitulée « Méthodes de programmation en nombres mixtes pour l’optimisation parcimonieuse en traitement du signal »
mercredi 13 mai 2020 à 14h en visio-conférence à l’ECN.

Jury :
– Directeur thèse : Bourguignon Sébastien
– Co-encadrant : Ninin Jordan (ENSTA Bretagne)
– Rapporteurs : Cafieri Sonia (Ecole nationale aviation civile), Kowalski Matthieu (Laboratoire des Signaux et Systèmes)
– Autres membres : Jutten Christian (Université Grenoble Alpes), Ralaivola Liva (Aix Marseille Université)

Soutenance de thèse de Ran BAO (équipe AELOS)

Ran Bao, doctorante au sein de l’équipe AELOS, soutiendra sa thèse intitulée « Modélisation formelle de systèmes de drones civils à l’aide de méthodes probabilistes paramétrées » / « Parametric Statistical model checking of UAV flight plan »

jeudi 7 mai 2020 à 10h, en visio.

Jury :
– Directeur thèse : Chirstian Attiogbé
– Co-encadrant : Benoit Delahaye
– Rapporteurs : Patricia Bouyer-Decitre (ENS Paris Saclay), Laure Petrucci (U. Paris 13)
– Autres membres : Olga Kouchnarenko (U. Franche Comté), Claude Jard
– Membre invité : Philippe Barranger (Pixiel)

Résumé : Les drones sont maintenant très répandus dans la société et sont souvent utilisés dans des situations dangereuses pour le public environnant. Il est alors nécessaire d’étudier leur fiabilité, en particulier dans le contexte de vols au-dessus d’un public. Dans cette thèse, nous étudions la modélisation et l’analyse de drones dans le contexte de leur plan de vol. Pour cela, nous construisons plusieurs modèles probabilistes du drone et les utilisons ainsi que le plan de vol pour modéliser la trajectoire du drone. Le modèle le plus détaillé obtenu prend en compte des paramètres comme la précision de l’estimation de la position par les différents capteurs, ainsi que la force et la direction du vent. Le modèle est analysé afin de mesurer la probabilité que le drone entre dans une zone dangereuse. Du fait de la nature et de la complexité des modèles successifs obtenus, leur vérification avec les outils classique, tels que PRISM ou PARAM, est impossible. Nous utilisons donc une nouvelle méthode d’approximation, appelée Model Checking Statistique Paramétrique. Cette méthode a été implémentée dans un prototype, que nous avons mis à
l’épreuve sur ce cas d’étude complexe. Nous avons pour finir utilisé les résultats fournis par ce prototype afin de proposer des pistes permettant d’améliorer la sécurité du public dans le contexte considéré.

Mots-clés : Drone, Modèle formel, Chaîne de Markov, Model checking statistique paramétrique

*********

Abstract: Unmanned Aerial Vehicles (UAV) are now widespread in our society and are often used in a context where they can put people at risk. Studying their reliability, in particular in the context of flight above a crowd, thus becomes a necessity. In this thesis, we study the modeling and analysis of UAV in the context of their flight plan. To this purpose, we build several parametrics probabilistic models of the UAV and use them, as well as a given flight plan, in order to model its trajectory. Our most advanced model takes into account the precision of position estimation by embedded sensors, as well as wind force and direction. The model is analyzed in order to measure the probability that the drone enters an unsafe zone. Because of the nature and complexity of the obtained models, their exact verification using classical tools such as PRISM or PARAM is impossible. We therefore develop a new approximation method, called Parametric Statistical Model Checking. This method has been implemented in a prototype tool, which we tested on this complex case study. Finally, we use the result to propose some ways to improve the safety of the public in our context.

Keywords: UAV, Formal Model, Markov Chain, Parametric statistical model checking

Archives