Cette thèse porte sur la vérification des automates temporisés, un modèle bien établi pour les systèmes temps-réels. La thèse est constituée de trois parties. La première est dédiée à la déterminisation des automates temporisés, problème qui n'a pas de solution en général. Nous proposons une méthode approchée (sur-approximation, sous-approximation, mélange des deux) fondée sur la construction d'un jeu de sûreté. Cette méthode améliore les approches existantes en combinant leurs avantages respectifs. Nous appliquons ensuite cette méthode de déterminisation à la génération automatique de tests de conformité. Dans la seconde partie, nous prenons en compte des aspects quantitatifs des systèmes temps-réel grâce à une notion de fréquence des états acceptants dans une exécution d'un automate temporisé. Plus précisément, la fréquence d'une exécution est la proportion de temps passée dans les états acceptants. Nous intéressons alors à l'ensemble des fréquences des exécutions d'un automate temporisé pour étudier, par exemple, le vide de langages seuils. Nous montrons ainsi que les bornes de l'ensemble des fréquences sont calculables pour deux classes d'automates temporisés. D'une part, les bornes peuvent être calculées en espace logarithmique par une procédure non-déterministe dans les automates temporisés à une horloge. D'autre part, elles peuvent être calculées en espace polynomial dans les automates temporisés à plusieurs horloges ne contenant pas de cycles forçant la convergence d'horloges. Finalement, nous étudions le problème de l'accessibilité des états acceptants dans des réseaux d'automates temporisés qui communiquent via des files FIFO. Nous considérons tout d'abord des automates temporisés à temps discret, et caractérisons les topologies de réseaux pour lesquelles l'accessibilité est décidable. Cette caractérisation est ensuite étendue aux automates temporisés à temps continu. / This thesis is about verification of timed automata, a well-established model for real time systems. The document is structured in three parts. The first part is dedicated to the determinization of timed automata, a problem which has no solution in general. We propose an approximate (over-approximation/under-approximation/mix) method based on the construction of a safety game. This method improves both existing approaches by combining their respective advantages. Then, we apply this determinization approach to the generation of conformance tests. In the second part, we take into account quantitative aspects of real time systems thanks to a notion of frequency of accepting states along executions of timed automata. More precisely, the frequency of a run is the proportion of time elapsed in accepting states. Then, we study the set of frequencies of runs of a timed automaton in order to decide, for example, the emptiness of threshold languages. We thus prove that the bounds of the set of frequencies are computable for two classes of timed automata. On the one hand, we prove that bounds are computable in logarithmic space by a non-deterministic procedure in one-clock timed automata. On the other hand, they can be computed in polynomial space in timed automata with several clocks, but having no cycle that forces the convergence between clocks. Finally, we study the reachability problem in networks of timed automata communicating through FIFO channels. We first consider dicrete timed automata, and characterize topologies of networks for which reachability is decidable. Then, this characterization is extended to dense-time automata.

Les systèmes robotiques et autonomes ne cessent d’évoluer et deviennent de plus en plus impliqués dans les missions à coût considérable et/ou dans les milieux humains. Par conséquent, les simulations et campagnes de tests ne sont plus adaptées à la problématique de sûreté et fiabilité des systèmes robotiques et autonomes compte tenu (i) du caractère sérieux des défaillances éventuelles dans les contextes susmentionnés (un dommage à un robot très coûteux ou plus dramatiquement une atteinte aux vies humaines) et (ii) de la nature non exhaustive de ces techniques (les tests et simulations peuvent toujours passer à côté d’un scénario d’exécution catastrophique.Les méthodes formelles, quant à elles, peinent à s’imposer dans le domaine de la robotique autonome, notamment au niveau fonctionnel des robots, i.e. les composants logiciels interagissant directement avec les capteurs et les actionneurs. Elle est due à plusieurs facteurs. D’abord, les composants fonctionnels reflètent un degré de complexité conséquent, ce qui mène souvent à une explosion combinatoire de l’espace d’états atteignables (comme l’exploration se veut exhaustive). En outre, les composants fonctionnels sont décrits à travers des languages et frameworks informels (ROS, GenoM, etc.). Leurs spécifications doivent alors être traduites en des modèles formels avant de pouvoir y appliquer les méthodes formelles associées. Ceci est souvent pénible, lent, exposé à des erreurs, et non automatique, ce qui implique un investissement dans le temps aux limites de la rentabilité. Nous proposons, dans cette thèse, de connecter GenoM3, un framework de développement et déploiement de composants fonctionnels robotiques, à des langages formels et leurs outils de vérification respectifs. Cette connexion se veut automatique: nous développons des templates en mesure de traduire n’importe quelle spécification de GenoM3 en langages formels. Ceci passe par une formalisation de GenoM3: une sémantique formelle opérationnelle est donnée au langage. Une traduction à partir de cette sémantique est réalisée vers des langages formels et prouvée correcte par bisimulation. Nous comparons de différents langages cibles, formalismes et techniques et tirerons les conclusions de cette comparaison. La modélisation se veut aussi, et surtout, efficace. Un modèle correct n’est pas forcément utile. En effet, le passage à l’échelle est particulièrement important.Cette thèse porte donc sur l'applicabilité des méthodes formelles aux compo-sants fonctionnels des systèmes robotiques et autonomes. Le but est d'aller vers des robots autonomes plus sûrs avec un comportement plus connu et prévisible. Cela passe par la mise en place d'un mécanisme de génération automatique de modèles formels à partir de modules fonctionnels de sys-tèmes robotiques et autonomes. Les langages et outils cibles sont Fiacre/TINA et UPPAAL (model checking), UPPAAL-SMC (statistical model checking), BIP/RTD-Finder (SAT solving), et BIP/Engine (enforcement de propriétés en ligne). Les modèles générés sont exploités pour vérifier des propriétés quali-tatives ou temps-réel, souvent critiques pour les systèmes robotiques et auto-nomes considérés. Parmi ces propriétés, on peut citer, à titre d'exemple, l'ordonnançabilité des tâches périodiques, la réactivité des tâches spora-diques, l'absence d’interblocages, la vivacité conditionnée (un évènement tou-jours finit par suivre un autre), la vivacité conditionnée bornée (un évène-ment toujours suit un autre dans un intervalle de temps borné), l'accessibilité (des états “indésirables” ne sont jamais atteints), etc.La thèse propose éga-lement une analyse du feedback expérimental afin de guider les ingénieurs à exploiter ces méthodes et techniques de vérification efficacement sur les mo-dèles automatiquement générés. / The goal of this thesis is to add to the efforts toward the long-sought objective of secure and safe robots with predictable and a priori known behavior. For the reasons given above, formal methods are used to model and verify crucial properties, with a focus on the functional level of robotic systems. The approach relies on automatic generation of formal models targeting several frameworks. For this, we give operational semantics to a robotic framework, then several mathematically proven translations are derived from such semantics. These translations are then automatized so any robotic functional layer specification can be translated automatically and promptly to various frameworks/languages. Thus, we provide a mathematically correct mapping from functional components to verifiable models. The obtained models are used to formulate and verify crucial properties (see examples above) on real-world complex robotic and autonomous systems. This thesis provides also a valuable feedback on the applicability of formal frameworks on real-world, complex systems and experience-based guidelines on the efficient use of formal-model automatic generators. In this context, efficiency relates to, for instance, how to use the different model checking tools optimally depending on the properties to verify, what to do when the models do not scale with model checking (e.g. the advantages and drawbacks of statistical model checking and runtime verification and when to use the former or the latter depending on the type of properties and the order of magnitude of timing constraints).

Le contenu généré dans les médias sociaux comme Twitter permet aux utilisateurs d'avoir un aperçu rétrospectif d'évènement et de suivre les nouveaux développements dès qu'ils se produisent. Cependant, bien que Twitter soit une source d'information importante, il est caractérisé par le volume et la vélocité des informations publiées qui rendent difficile le suivi de l'évolution des évènements. Pour permettre de mieux tirer profit de ce nouveau vecteur d'information, deux tâches complémentaires de recherche d'information dans les médias sociaux ont été introduites : la génération de résumé rétrospectif qui vise à sélectionner les tweets pertinents et non redondant récapitulant "ce qui s'est passé" et l'envoi des notifications prospectives dès qu'une nouvelle information pertinente est détectée. Notre travail s'inscrit dans ce cadre. L'objectif de cette thèse est de faciliter le suivi d'événement, en fournissant des outils de génération de synthèse adaptés à ce vecteur d'information. Les défis majeurs sous-jacents à notre problématique découlent d'une part du volume, de la vélocité et de la variété des contenus publiés et, d'autre part, de la qualité des tweets qui peut varier d'une manière considérable. La tâche principale dans la notification prospective est l'identification en temps réel des tweets pertinents et non redondants. Le système peut choisir de retourner les nouveaux tweets dès leurs détections où bien de différer leur envoi afin de s'assurer de leur qualité. Dans ce contexte, nos contributions se situent à ces différents niveaux : Premièrement, nous introduisons Word Similarity Extended Boolean Model (WSEBM), un modèle d'estimation de la pertinence qui exploite la similarité entre les termes basée sur le word embedding et qui n'utilise pas les statistiques de flux. L'intuition sous- jacente à notre proposition est que la mesure de similarité à base de word embedding est capable de considérer des mots différents ayant la même sémantique ce qui permet de compenser le non-appariement des termes lors du calcul de la pertinence. Deuxièmement, l'estimation de nouveauté d'un tweet entrant est basée sur la comparaison de ses termes avec les termes des tweets déjà envoyés au lieu d'utiliser la comparaison tweet à tweet. Cette méthode offre un meilleur passage à l'échelle et permet de réduire le temps d'exécution. Troisièmement, pour contourner le problème du seuillage de pertinence, nous utilisons un classificateur binaire qui prédit la pertinence. L'approche proposée est basée sur l'apprentissage supervisé adaptatif dans laquelle les signes sociaux sont combinés avec les autres facteurs de pertinence dépendants de la requête. De plus, le retour des jugements de pertinence est exploité pour re-entrainer le modèle de classification. Enfin, nous montrons que l'approche proposée, qui envoie les notifications en temps réel, permet d'obtenir des performances prometteuses en termes de qualité (pertinence et nouveauté) avec une faible latence alors que les approches de l'état de l'art tendent à favoriser la qualité au détriment de la latence. Cette thèse explore également une nouvelle approche de génération du résumé rétrospectif qui suit un paradigme différent de la majorité des méthodes de l'état de l'art. Nous proposons de modéliser le processus de génération de synthèse sous forme d'un problème d'optimisation linéaire qui prend en compte la diversité temporelle des tweets. Les tweets sont filtrés et regroupés d'une manière incrémentale en deux partitions basées respectivement sur la similarité du contenu et le temps de publication. Nous formulons la génération du résumé comme étant un problème linéaire entier dans lequel les variables inconnues sont binaires, la fonction objective est à maximiser et les contraintes assurent qu'au maximum un tweet par cluster est sélectionné dans la limite de la longueur du résumé fixée préalablement. / User-generated content on social media, such as Twitter, provides in many cases, the latest news before traditional media, which allows having a retrospective summary of events and being updated in a timely fashion whenever a new development occurs. However, social media, while being a valuable source of information, can be also overwhelming given the volume and the velocity of published information. To shield users from being overwhelmed by irrelevant and redundant posts, retrospective summarization and prospective notification (real-time summarization) were introduced as two complementary tasks of information seeking on document streams. The former aims to select a list of relevant and non-redundant tweets that capture "what happened". In the latter, systems monitor the live posts stream and push relevant and novel notifications as soon as possible. Our work falls within these frameworks and focuses on developing a tweet summarization approaches for the two aforementioned scenarios. It aims at providing summaries that capture the key aspects of the event of interest to help users to efficiently acquire information and follow the development of long ongoing events from social media. Nevertheless, tweet summarization task faces many challenges that stem from, on one hand, the high volume, the velocity and the variety of the published information and, on the other hand, the quality of tweets, which can vary significantly. In the prospective notification, the core task is the relevancy and the novelty detection in real-time. For timeliness, a system may choose to push new updates in real-time or may choose to trade timeliness for higher notification quality. Our contributions address these levels: First, we introduce Word Similarity Extended Boolean Model (WSEBM), a relevance model that does not rely on stream statistics and takes advantage of word embedding model. We used word similarity instead of the traditional weighting techniques. By doing this, we overcome the shortness and word mismatch issues in tweets. The intuition behind our proposition is that context-aware similarity measure in word2vec is able to consider different words with the same semantic meaning and hence allows offsetting the word mismatch issue when calculating the similarity between a tweet and a topic. Second, we propose to compute the novelty score of the incoming tweet regarding all words of tweets already pushed to the user instead of using the pairwise comparison. The proposed novelty detection method scales better and reduces the execution time, which fits real-time tweet filtering. Third, we propose an adaptive Learning to Filter approach that leverages social signals as well as query-dependent features. To overcome the issue of relevance threshold setting, we use a binary classifier that predicts the relevance of the incoming tweet. In addition, we show the gain that can be achieved by taking advantage of ongoing relevance feedback. Finally, we adopt a real-time push strategy and we show that the proposed approach achieves a promising performance in terms of quality (relevance and novelty) with low cost of latency whereas the state-of-the-art approaches tend to trade latency for higher quality. This thesis also explores a novel approach to generate a retrospective summary that follows a different paradigm than the majority of state-of-the-art methods. We consider the summary generation as an optimization problem that takes into account the topical and the temporal diversity. Tweets are filtered and are incrementally clustered in two cluster types, namely topical clusters based on content similarity and temporal clusters that depends on publication time. Summary generation is formulated as integer linear problem in which unknowns variables are binaries, the objective function is to be maximized and constraints ensure that at most one post per cluster is selected with respect to the defined summary length limit.

Dans les systèmes informatiques temps réel, les tâches logicielles sont contraintes par le temps. Pour garantir la sûreté du système critique contrôlé par le système temps réel, il est primordial d'estimer de manière sûre le pire temps d'exécution de chaque tâche. Les performances des processeurs actuels du commerce permettent de réduire en moyenne le temps d'exécution des tâches, mais la complexité des composants d'optimisation de la plateforme rendent difficile l'estimation du pire temps d'exécution. Il existe différentes approches d'estimation du pire temps d'exécution, souvent ségréguées et difficilement généralisables ou au prix de modèles coûteux. Les approches probabilistes basées mesures existantes sont vues comme étant rapides et simples à mettre en œuvre, mais souffrent d'un manque de systématisme et de confiance dans les estimations qu'elles fournissent. Les travaux de cette thèse étudient les conditions d'application de la théorie des valeurs extrêmes à une suite de mesures de temps d'exécution pour l'estimation du pire temps d'exécution probabiliste, et ont été implémentées dans l'outil diagxtrm. Les capacités et les limites de l'outil ont été étudiées grâce à diverses suites de mesures issues de systèmes temps réel différents. Enfin, des méthodes sont proposées pour déterminer les conditions de mesure propices à l'application de la théorie des valeurs extrêmes et donner davantage de confiance dans les estimations. / Software tasks are time constrained in real time computing systems. To ensure the safety of the critical systems that embeds the real time system, it is of paramount importance to safely estimate the worst-case execution time of each task. Modern commercial processors optimisation components enable to reduce in average the task execution time at the cost of a hard to determine task worst-case execution time. Many approaches for executing a task worst-case execution time exist but are usually segregated and hardly scalable, or by building very complex models. Measurement-based probabilistic timing analysis approaches are said to be easy and fast, but they suffer from a lack of systematism and confidence in their estimates. This thesis studies the applicability of the extreme value theory to a sequence of execution time measurements for the estimation of the probabilistic worst-case execution time, leading to the development of the diagxtrm tool. Thanks to a large panel of sequences of measurements from different real time systems, capabilities and limits of the tool are enlightened. Finally, a couple of methods are provided for determining measurements conditions that foster the application of the theory and raise more confidence in the estimates.

Cette thèse s’inscrit dans le domaine de l’automatique, et a pour but de fournir des outils utiles à l’atterrissage en mer d’hélicoptères (sur navire ou plateforme) et employés dans le cadre d’un potentiel pilotage automatique. L’objectif a donc été de développer une série de lois de commande pilotées manuellement, puis commandées de façon autonome à l’aide d’informations caméra. Les lois ainsi développées à l’aide de modèles dynamiques d’hélicoptères, limitations mécaniques incluses, se basent sur les critères de Qualité de Vol issus de la norme ADS-33. L’ensemble a fait appel à une approche anti-windup pour améliorer la robustesse face aux situations d’actionneurs en saturation. Enfin les lois issues de ces travaux ont été testées en temps-réel sur le banc de pilotage d’hélicoptères de l’ONERA Salon-de-Provence. / This thesis is related to the automatic & control engineering field, and itsmain goal is to provide useful tools for ship landing missions, tools that can be used fora potential autopilot. The objective has been to develop a series of control laws manuallypiloted, then automatically controlled by visual servoing using identified image features. Thelaws developped thanks to helicopter models with mechanical limitations were based on flyingqualities criteria from the ADS-33 standard. The process also defines an anti-windup approachto cope with actuator saturations. Finally the main results were assessed in real time withthe ONERA rotorcraft flight test bench at ONERA Salon-de-Provence.

La conception de systèmes temps-réel embarqués se développe de plus en plus avec l’intégration croissante de fonctionnalités critiques pour les applications de surveillance, notamment dans le domaine biomédical, environnemental, domotique, etc. Le développement de ces systèmes doit relever divers défis en termes de minimisation de la consommation énergétique. Gérer de tels dispositifs embarqués, entièrement autonomes, nécessite cependant de résoudre différents problèmes liés à la quantité d’énergie disponible dans la batterie, à l’ordonnancement temps-réel des tâches qui doivent être exécutées avant leurs échéances, aux scénarios de reconfiguration, particulièrement dans le cas d’ajout de tâches, et à la contrainte de communication pour pouvoir assurer l’échange des messages entre les processeurs, de façon à assurer une autonomie durable jusqu’à la prochaine recharge et ce, tout en maintenant un niveau de qualité de service acceptable du système de traitement. Pour traiter cette problématique, nous proposons dans ces travaux une stratégie de placement et d’ordonnancement de tâches permettant d’exécuter des applications temps-réel sur une architecture contenant des cœurs hétérogènes. Dans cette thèse, nous avons choisi d’aborder cette problématique de façon incrémentale pour traiter progressivement les problèmes liés aux contraintes temps-réel, énergétique et de communications. Tout d’abord, nous nous intéressons particulièrement à l’ordonnancement des tâches sur une architecture mono-cœur. Nous proposons une stratégie d’ordonnancement basée sur le regroupement des tâches dans des packs pour pouvoir calculer facilement les nouveaux paramètres des tâches afin de réobtenir la faisabilité du système. Puis, nous l’avons étendu pour traiter le cas de l’ordonnancement sur une architecture multi-cœurs homogènes. Finalement, une extension de ce dernier sera réalisée afin d’arriver à l’objectif principal qui est l’ordonnancement des tâches pour les architectures hétérogènes. L’idée est de prendre progressivement en compte des contraintes d’exécution de plus en plus complexes. Nous formalisons tous les problèmes en utilisant la formulation ILP afin de pouvoir produire des résultats optimaux. L’idée est de pouvoir situer nos solutions proposées par rapport aux solutions optimales produites par un solveur et par rapport aux autres algorithmes de l’état de l’art. Par ailleurs, la validation par simulation des stratégies proposées montre qu’elles engendrent un gain appréciable vis-à-vis des critères considérés importants dans les systèmes embarqués, notamment le coût de la communication entre cœurs et le taux de rejet des tâches. / The design of embedded real-time systems is developing more and more with the increasing integration of critical functionalities for monitoring applications, particularly in the biomedical, environmental, home automation, etc. The developement of these systems faces various challenges particularly in terms of minimizing energy consumption. Managing such autonomous embedded devices, requires solving various problems related to the amount of energy available in the battery and the real-time scheduling of tasks that must be executed before their deadlines, to the reconfiguration scenarios, especially in the case of adding tasks, and to the communication constraint to be able to ensure messages exchange between cores, so as to ensure a lasting autonomy until the next recharge, while maintaining an acceptable level of quality of services for the processing system. To address this problem, we propose in this work a new strategy of placement and scheduling of tasks to execute real-time applications on an architecture containing heterogeneous cores. In this thesis, we have chosen to tackle this problem in an incremental manner in order to deal progressively with problems related to real-time, energy and communication constraints. First of all, we are particularly interested in the scheduling of tasks for single-core architecture. We propose a new scheduling strategy based on grouping tasks in packs to calculate the new task parameters in order to re-obtain the system feasibility. Then we have extended it to address the scheduling tasks on an homogeneous multi-core architecture. Finally, an extension of the latter will be achieved in order to realize the main objective, which is the scheduling of tasks for the heterogeneous architectures. The idea is to gradually take into account the constraints that are more and more complex. We formalize the proposed strategy as an optimization problem by using integer linear programming (ILP) and we compare the proposed solutions with the optimal results provided by the CPLEX solver. Inaddition, the validation by simulation of the proposed strategies shows that they generate a respectable gain compared with the criteria considered important in embedded systems, in particular the cost of communication between cores and the rate of new tasks rejection.

Les vésicules synaptiques (VSs) sont essentielles pour la neurotransmission. Les recherches actuelles se focalisent sur la caractérisation de leur contenu en neurotransmetteurs, leur cinétique de libération, leur distribution et leur mobilité. Les VS ne sont pas présentes exclusievement en paquet dans les boutons présynaptiques mais sont echangées de façon dynamique avec le reste de l’axone dans un super-contingent (super-pool). Notre laboratoire a précédement montré que le transporteur vésiculaire de glutamate de type 1 (VGLUT1) jouerait un rôle dans la régulation du super-pool. Mon projet de thèse se focalise sur la mobilité des VS dans les axones. En premier lieu, j’ai généré une souris gain de fonction VGLUT1mEos2 afin d'étudier la mobilité des VSs et de mieux caractériser le super-pool. Ensuite j’ai engagé une étude des relation entre la structure de VGLUT1 et ses fonctions afin d’identifier les signatures moléculaires responsable de la régulation de la taille du super-pool. J’ai identifié le second motif poly-proline à l’extremité C-terminale de VGLUT1 comme étant nécessaire et suffisante pour induire une diminution de la taille du super-pool des VSs. Pour conclure mes travaux de thèse ont contribué à la compréhension du rôle de VGLUT1 dans la régulation de la mobilité des VSs et à fournir les outils nécessaires pour de futures investigations concernant la physiologie du super-pool. / Synaptic vesicles (SVs) are essential for neurotransmission, and more efforts are needed for better understanding their neurotransmitter content, release kinetics, distribution and mobility. SVs are not only clustered in presynaptic boutons, but also dynamically shared among multiple en passant presynaptic boutons, a phenomenon named SV super‐pool. Previous work from our laboratory suggested that the Vesicular GLUtamate Transporter 1 (VGLUT1) may play a role in regulating SV super-­pool size beyond loading glutamate into SV. My Ph.D project is focused on SVs mobility in axons. Firstly, I generated a VGLUT1mEos2 knock-in (KI) mouse line, which provides extended possibilities to study the SV trafficking and characterize SV super‐pool. Secondly, I engaged in a thorough VGLUT1 structure‐function analysis. I identified that VGLUT1 tends to cluster SVs in the presynaptic boutons and reduce SVs exchange with the super‐pool via the second poly‐proline motif of its C­‐terminus. Overall, my Ph.D work contributes to the knowledge of the role of VGLUT1 in regulating SVs mobility and provides new tools for the further investigations on SV super-­pool physiology.

En raison de l'augmentation des coûts d'énergie et des préoccupations environnementales telles que les empreintes de carbone élevées, les systèmes de la production d'électricité centralisée se restructurent pour profiter des avantages de la production distribuée afin de répondre aux exigences énergétiques toujours croissantes. Les microgrids sont considérés comme une solution possible pour déployer une génération distribuée qui inclut des ressources énergétiques distribuées DERs (Distributed Energy Resources)(e.g, solaire, éolienne, batterie, etc). Dans cette thèse, nous traitons les défis de la gestion d'énergie dans un microgrid industriel où les charges énergétique sont constituées de processus industriels. Notre plan consiste à diviser la gestion de l'énergie du microgrid en deux parties: la production et la demande d’énergie.Du côté de la production d'énergie, les défis incluent la modélisation des générations de puissance et le lissage des fluctuations des DER. Pour modéliser les générations de puissance, nous proposons un modèle basé sur les concepts de service courbé de Network Calculus. En utilisant cet outil mathématique, nous déterminons une quantité minimale de puissance que les DERs peuvent générer; leur agrégation nous donnera une production d'énergie totale dans le microgrid. Après cela, s'il existe un déséquilibre entre la production et la demande d'énergie, nous proposons des stratégies différentes pour minimiser les coûts d'approvisionnement énergétique. Sur la base des données réelles de la consommation d'énergie d'un site industriel situé en France, des économies significatives peuvent être réalisées en adoptant ces stratégies. Dans cette thèse, nous étudions également comment atténuer les effets des fluctuations de puissance des DERs en conjonction avec des systèmes de stockage d'énergie. Pour cela, nous proposons un algorithme de lissage gaussien et nous le comparons avec des algorithmes de lissage trouvés dans l'état de l'art. Nous avons trouvé que l'algorithme proposé utilise de batterie de moins de taille à des fins de lissage par rapport à d'autres algorithmes. À cette fin, nous sommes également intéressés à étudier les effets de la gamme admissible des fluctuations sur les tailles de la batterie.Du côté de la demande, l'objectif est de réduire les coûts de l'énergie grâce aux approches de gestion de la demande DSM (Demand Side Management) telles que Demand Response (DR) et Energy Efficiency. Comme les processus industriels consomment énormément, une petite réduction de la consommation d'énergie en utilisant les approches DSM pourrait se traduire par des économies cruciales. Cette thèse se concentre sur l'approche DR qui peut profiter des prix variables de l'électricité dans le temps pour déplacer les demandes énergétiques des heures de pointe aux heures creuses. Pour atteindre cet objectif, nous comptons sur un modèle basé sur la théorie de file d'attente pour caractériser les comportements temporels (arrivée et départ des tâches) d'un système de fabrication. Après avoir défini les processus d'arrivée et de départ de tâches, une fonction d'utilisation efficace est utilisée pour prédire le comportement de la machine dans un domaine temporel et qui peut afficher son statut (allumé/éteint) à tout moment. En prenant le statut de chaque machine dans une ligne de production comme une entrée, nous proposons également un algorithme de planification DR qui adapte la consommation d'énergie d'une ligne de production aux deux contraintes de puissance disponibles et de taux de production. L'algorithme est codé à l'aide d’une machine d’état fini déterministe (Deterministic Finite State Machine) dans laquelle les transitions d'état se produisent en insérant une tâche à l'entrée du tapis roulant (on peut aussi avoir des transitions sans insertion de taches). Nous définissons des conditions pour l'existence d’un planificateur réalisable et aussi des conditions pour accepter positivement des demandes DRs / Due to increased energy costs and environmental concerns such as elevated carbon footprints, centralized power generation systems are restructuring themselves to reap benefits of distributed generation in order to meet the ever growing energy demands. Microgrids are considered as a possible solution to deploy distributed generation which includes Distributed Energy Resources (DERs) (e.g., solar, wind, battery, etc). In this thesis, we are interested in addressing energy management challenges in an industrial microgrid where energy loads consist of industrial processes. Our plan of attack is to divide the microgrid energy management into supply and demand sides.In supply side, the challenges include modeling of power generations and smoothing out fluctuations of the DERs. To model power generations, we propose amodel based on service curve concepts of Network Calculus (NC). Using this mathematical tool, we determine a minimum amount of power the DERs can generate and aggregating them will give us total power production in the microgrid. After that, if there is an imbalance between energy supply and demand, we put forward different strategies to minimize energy procurement costs. Based on real power consumption data of an industrial site located in France, significant cost savings can be made by adopting the strategies. In this thesis, we also study how to mitigate the effects of power fluctuations of DERs in conjunction with Energy Storage Systems (ESSs). For this purpose, we propose a Gaussian-based smoothing algorithm and compare it with state-of-the-art smoothing algorithms. We found out that the proposed algorithm uses less battery size for smoothing purposes when compared to other algorithms. To this end, we are also interested in investigating effects of allowable range of fluctuations on battery sizes.In demand side, the aim is to reduce energy costs through Demand Side Management (DSM) approaches such as Demand Response (DR) and Energy Efficiency (EE). As industrial processes are power-hungry consumers, a small power consumption reduction using the DSM approaches could translate into crucial savings. This thesis focuses on DR approach that can leverage time varying electricity prices to move energy demands from peak to off-peak hours. To attain this goal, we rely on a queuing theory-based model to characterize temporal behaviors (arrival and departure of jobs) of a manufacturing system. After defining job arrival and departure processes, an effective utilization function is used to predict workstation’s (or machine’s) behavior in temporal domain that can show its status (working or idle) at any time. Taking the status of every machine in a production line as an input, we also propose a DR scheduling algorithm that adapts power consumption of a production line to available power and production rate constraints. The algorithm is coded using Deterministic Finite State Machine (DFSM) in which state transitions happen by inserting a job (or not inserting) at conveyor input. We provide conditions for existence of feasible schedules and conditions to accept DR requests positively.To verify analytical computations on the queuing part, we have enhanced Objective Modular Network Testbed in C++ (OMNET++) discrete event simulator for fitting it to our needs. We modified various libraries in OMNET++ to add machine and conveyor modules. In this thesis, we also setup a testbed to experiment with a smart DR protocol called Open Automated Demand Response (OpenADR) that enables energy providers (e.g., utility grid) to ask consumers to reduce their power consumption for a given time. The objective is to explore how to implement our DR scheduling algorithm on top of OpenADR

Avec le besoin grandissant pour des modèles d’analyse automatiques de vidéos, le suivi visuel d’objets est devenu une tache primordiale dans le domaine de la vision par ordinateur. Un algorithme de suivi dans un environnement non contraint fait face à de nombreuses difficultés: changements potentiels de la forme de l’objet, du fond, de la luminosité, du mouvement de la camera, et autres. Dans cette configuration, les méthodes classiques de soustraction de fond ne sont pas adaptées, on a besoin de méthodes de détection d’objet plus discriminantes. De plus, la nature de l’objet est a priori inconnue dans les méthodes de tracking génériques. Ainsi, les modèles d’apparence d’objets appris off-ligne ne peuvent être utilisés. L’évolution récente d’algorithmes d’apprentissage robustes a permis le développement de nouvelles méthodes de tracking qui apprennent l’apparence de l’objet de manière en ligne et s’adaptent aux variables contraintes en temps réel. Dans cette thèse, nous démarrons par l’observation que différents algorithmes de suivi ont différentes forces et faiblesses selon l’environnement et le contexte. Afin de surmonter les variables contraintes, nous démontrons que combiner plusieurs modalités et algorithmes peut améliorer considérablement la performance du suivi global dans les environnements non contraints. Plus concrètement, nous introduisant dans un premier temps un nouveau framework de sélection de trackers utilisant un critère de cohérence spatio-temporel. Dans ce framework, plusieurs trackers indépendants sont combinés de manière parallèle, chacun d’entre eux utilisant des features bas niveau basée sur différents aspects visuels complémentaires tel que la couleur, la texture. En sélectionnant de manière récurrente le tracker le plus adaptée à chaque trame, le système global peut switcher rapidement entre les différents tracker selon les changements dans la vidéo. Dans la seconde contribution de la thèse, le contexte de scène est utilisé dans le mécanisme de sélection de tracker. Nous avons conçu des features visuelles, extrait de l’image afin de caractériser les différentes conditions et variations de scène. Un classifieur (réseau de neurones) est appris grâce à ces features de scène dans le but de prédire à chaque instant le tracker qui performera le mieux sous les conditions de scènes données. Ce framework a été étendu et amélioré d’avantage en changeant les trackers individuels et optimisant l’apprentissage. Finalement, nous avons commencé à explorer une perspective intéressante où, au lieu d’utiliser des features conçu manuellement, nous avons utilisé un réseau de neurones convolutif dans le but d’apprendre automatiquement à extraire ces features de scène directement à partir de l’image d’entrée et prédire le tracker le plus adapté. Les méthodes proposées ont été évaluées sur plusieurs benchmarks publiques, et ont démontré que l’utilisation du contexte de scène améliore la performance globale du suivi d’objet. / With the increasing need for automated video analysis, visual object tracking became an important task in computer vision. Object tracking is used in a wide range of applications such as surveillance, human-computer interaction, medical imaging or vehicle navigation. A tracking algorithm in unconstrained environments faces multiple challenges : potential changes in object shape and background, lighting, camera motion, and other adverse acquisition conditions. In this setting, classic methods of background subtraction are inadequate, and more discriminative methods of object detection are needed. Moreover, in generic tracking algorithms, the nature of the object is not known a priori. Thus, off-line learned appearance models for specific types of objects such as faces, or pedestrians can not be used. Further, the recent evolution of powerful machine learning techniques enabled the development of new tracking methods that learn the object appearance in an online manner and adapt to the varying constraints in real time, leading to very robust tracking algorithms that can operate in non-stationary environments to some extent. In this thesis, we start from the observation that different tracking algorithms have different strengths and weaknesses depending on the context. To overcome the varying challenges, we show that combining multiple modalities and tracking algorithms can considerably improve the overall tracking performance in unconstrained environments. More concretely, we first introduced a new tracker selection framework using a spatial and temporal coherence criterion. In this algorithm, multiple independent trackers are combined in a parallel manner, each of them using low-level features based on different complementary visual aspects like colour, texture and shape. By recurrently selecting the most suitable tracker, the overall system can switch rapidly between different tracking algorithms with specific appearance models depending on the changes in the video. In the second contribution, the scene context is introduced to the tracker selection. We designed effective visual features, extracted from the scene context to characterise the different image conditions and variations. At each point in time, a classifier is trained based on these features to predict the tracker that will perform best under the given scene conditions. We further improved this context-based framework and proposed an extended version, where the individual trackers are changed and the classifier training is optimised. Finally, we started exploring one interesting perspective that is the use of a Convolutional Neural Network to automatically learn to extract these scene features directly from the input image and predict the most suitable tracker.

L’hallucination est une expérience subjective vécue en pleine conscience consistant en une perception impossible à distinguer d’une perception réelle, mais survenant en l’absence de tout stimulus en provenance de l’environnement externe. Les symptômes hallucinatoires, qui peuvent concerner toutes les modalités sensorielles, sont retrouvés dans divers troubles neurologiques et psychiatriques mais également chez certains sujets indemnes de toute pathologie. Dans le champ de la psychiatrie, la pathologie la plus fréquemment associée aux hallucinations reste la schizophrénie et la modalité auditive est la plus représentée, puisque 60 à 80% des patients souffrant de ce trouble sont concernés. Le retentissement fonctionnel des hallucinations auditives peut être important, altérant significativement la qualité de vie des patients.Dans ce contexte, la prise en charge de ce type de symptômes s’avère un enjeu considérable pour les personnes souffrant de schizophrénie. Pourtant, les moyens thérapeutiques actuellement disponibles (traitements médicamenteux antipsychotiques notamment) ne permettent pas toujours une rémission complète de la symptomatologie hallucinatoire et l’on considère que 25 à 30% des hallucinations auditives sont « pharmaco-résistantes ». C’est à partir de ce constat que, ces dernières années, ont émergé, pour le traitement des hallucinations auditives, des techniques de neuromodulation comme la stimulation magnétique transcrânienne répétée ou la stimulation électrique transcrânienne par courant continu. Toutefois, les résultats de ces nouvelles thérapies sur les hallucinations auditives résistantes restent modérés et le développement de stratégies alternatives demeure un enjeu de recherche majeur.Actuellement, les travaux en imagerie fonctionnelle permettent d'affiner les modèles physiopathologiques des hallucinations auditives, mais leur intérêt pourrait aller au-delà de la recherche fondamentale, avec possiblement des applications cliniques telles que l'assistance thérapeutique. Ce travail de thèse s’inscrit précisément dans le développement de l’imagerie cérébrale de « capture » des hallucinations auditives, c’est-à-dire l’identification des patterns d’activation fonctionnels associés à la survenue des hallucinations auditives.La première partie de ce travail est consacrée à la détection automatisée des hallucinations auditives en IRM fonctionnelle. L’identification des périodes hallucinatoires survenues au cours d’une session d’IRM fonctionnelle est actuellement possible par une méthode de capture semi-automatisée validée. Celle-ci permet une labellisation des données acquises au cours d’une session de repos en périodes « hallucinatoires » et « non-hallucinatoires ». Toutefois, le caractère long et fastidieux de cette méthode limite largement son emploi. Nous avons donc souhaité montrer comment les stratégies d’apprentissage machine (support vector machine ou SVM, notamment) permettent l’automatisation de cette technique par le développement de classificateurs performants, généralisables et associés à un faible coût de calcul (indispensable en vue d’une utilisation en temps réel). Nous proposons également le développement d’algorithmes de reconnaissance de la période « pré-hallucinatoire », en mettant en évidence que ce type de classificateur présente aussi des performances largement significatives. Enfin, nous avons pu montrer que l’utilisation de stratégies d’apprentissage-machine alternatives au SVM (e.g, le TV-Elastic-net), obtient des performances significativement supérieures au SVM [...] / Hallucination is a transient subjective experience perceived as real, but occurring in the absence of an appropriate stimulation coming from the external environment. Hallucinatory events, which can occur across every sensory modality, are observed in various neurological and psychiatric disorders but also among “non-clinical” populations. The most frequent disorder associated with hallucinations in the field of psychiatry is schizophrenia. Auditory-verbal experiences are particularly frequent, with a lifetime-prevalence of 60 to 80% in patients suffering from schizophrenia. Hallucinations may cause long-term disability and poorer quality of life.In this context, the management of auditory-verbal hallucinations in patients with schizophrenia constitutes a major challenge. However, despite the increasing sophistication of biological and psychosocial research methods in the field, no significant therapeutic breakthrough has occurred in the last decade and a consensus exists that a significant proportion of patients with schizophrenia (i.e., around 25 %), exhibit drug-resistant auditory-verbal hallucinations. Non-pharmacological treatments, such as repetitive transcranial magnetic stimulation (rTMS) or transcranial direct current stimulation (tDCS) have been proposed as an option for addressing the unmet medical needs described above. However, these neuromodulation techniques show a moderate effect in alleviating drug-resistant auditory-verbal hallucinations and the development of innovative therapeutic strategies remains a major challenge.In recent years, the number of brain imaging studies in the field of auditory-verbal hallucinations has grown substantially, leading to a better pathophysiological understanding of this subjective phenomenon. Recent progress in deciphering the neural underpinnings of AVHs has strengthened transdiagnostic neurocognitive models that characterize auditory-verbal hallucinations, but more specifically these findings built the bases for new therapeutic strategies. In this regards the development of auditory hallucinations “capture" brain-imaging studies (i.e. the identification of functional patterns associated with the occurrence of auditory hallucinations), was the main topic of this thesis.The first part of this work is devoted to the automatized detection of auditory-verbal hallucinations using functional MRI (fMRI). The identification of hallucinatory periods occurring during a fMRI session is now possible using a semi-automatized procedure based on an independent component analysis applied to resting fMRI data combined with a post-fMRI interview (i.e. the patient is asked to report auditory-verbal hallucinations immediately after acquisition). This “two-steps method” allows for the identification of hallucination periods (ON) and non-hallucination ones (OFF). However, the time-consuming nature of this a posteriori labelling procedure considerably limits its use. In these regards, we show how machine-learning, especially support vector machine (SVM), allows the automation of hallucinations capture. We present new results of accurate and generalizable classifiers which could be used in real-time because of their low computational-cost. We also highlight that algorithms able to identify the "pre-hallucinatory" period exhibit significant performances. Finally, we propose the use of an alternative learning-machine strategy, based on TV-Elastic-net, which achieves slightly better performances and more interpretable discriminative maps than SVM [...]