Le travail de thèse présente une méthode de développement de systèmes automatisés basée sur les méthodes formelles B et TLA+. Le développement par raffinement est au cœur de la méthode proposée. Un système automatisé est modélisé par deux composants, un contrôlé formé par le dispositif physique et son environnement et un contrôleur pilotant ce dernier. Il est exprimé par un produit synchronisé sur les actions de ces deux composants. La première contribution de la thèse concerne la proposition d'une approche qui combine le B événementiel et le langage de modélisation TLA+ pour la vérification des propriétés de vivacité. Nous définissons une extension syntaxique et sémantique du B événementiel permettant d'exprimer des propriétés de vivacité. Nous développons un prototype pour la transformation d'un modèle B en un module TLA+ sur lequel nous effectuons la preuve des propriétés de vivacité avec le model checker TLC. Pour la vérification de ce type de propriétés sur des systèmes infinis, nous proposons l'utilisation des diagrammes de prédicats qui sont des abstractions des systèmes modélisés en TLA+. La deuxième contribution est la proposition d'une technique pour représenter explicitement le temps en B événementiel. Cette technique s'appuie sur la réalisation d'un entrelacement entre un processus qui gère le temps avec les autres processus du système. Le temps modélisé est discret et son écoulement est modélisé par des événements. Cette approche est assez différente des systèmes temporisés où l'on considère que le temps s'écoule indépendamment du système. Dans la troisième contribution, nous proposons une approche de développement des systèmes automatisés en utilisant la technique de composition où il s'agit de développer conjointement le contrôleur et le composant physique qu'il contrôle et appliquer le raffinement aussi bien sur le contrôleur que le contrôlé. Le raffinement est une technique de base des méthodes que nous proposons et si notre objectif est de construire des contrôleurs corrects, le critère de correction porte sur le comportement du système automatisé qui résulte de la composition du contrôleur et du contrôlé. Nous présentons également un théorème de compositionnalité qui indique sous quelles conditions il est possible de déduire que le composé des raffinements des contrôleur et contrôlé est un raffinement du composé des contrôleur et contrôlé abstraits. La dernière contribution porte sur la définition, la preuve et l'utilisation d'un patron de raffinement pour les processus continus dans des systèmes de production manufacturière. Ce type de patron prouvé permet d'utiliser l'abstraction discrète de l'effet d'un processus continu agissant pendant un certain temps / This thesis deals with the development of automated systems while following the formal methods B and TLA+. We propose a formal methodology based on the refinement paradigm to specify and verify the system that we model by two components: the controlled system representing the physical device and its environment, and the controller that controls the system. A synchronised product on the actions of these two components is applied to specify the automated system. As a first contribution, we propose an approach combining the event B method and the language TLA+ in order to verify liveness properties defined in user requirements. Inspired by the temporal logic of actions TLA, we first extend the event B notation to specify liveness properties and we give semantics of this extended syntax over traces. Second, we give transformation rules from a temporal B model into a TLA+ module. We present, in particular, our prototype system called B2TLA+, that we have developed to support this transformation. To consider infinite systems, we use predicate diagrams as abstractions of systems modelled with TLA+. To consider the real-time concept in automated systems, we propose as a second contribution a technique explicitly representing time in B event systems. This technique is based on an interleaving between any event handling time and the other system events. By considering the well known co-design technique, we propose as a third contribution a refinement-based composition technique keeping a separation between controller and controlled systems in order to build correct automated systems satisfying user requirements. We prove a compositionality theorem with respect to refinement to get an efficient approach to verify the refinement of a synchronized composition between components. We verify the refinement of a synchronized composition by verifying separately the refinement of each component. Finally, we define, prove and use in a case study as a fourth contribution the concept of a refinement pattern for continuous processes in manufacturing systems. Such proven pattern allows us to use the discrete abstraction of the effect of continuous processes operating for a while

Les systèmes automatisés de production (SAP) représentent une classe importante des systèmes industriels qui sont de plus en plus complexes vue le grand nombre d’interaction et d’interconnexion entre leurs différents composants. En conséquence, ils sont plus sensibles aux dysfonctionnements dont les conséquences peuvent être importantes en termes de productivité, de sécurité et de qualité de production. Un défi majeur est alors de développer une approche intelligente qui peut être utilisée pour le diagnostic de ces systèmes afin de garantir leurs suretés de fonctionnement. Dans le cadre de cette thèse, nous nous intéressons seulement au diagnostic des SAP ayant une dynamique discrète. Nous présentons dans le premier chapitre ces systèmes, les dysfonctionnements possibles et la terminologie du diagnostic utilisée. Ensuite, nous présentons un état de l’art de différentes méthodes et approches existantes et aussi une synthèse de ces méthodes. Cette synthèse nous a motivé de choisir une approche à base de donnée qui s’appuie sur une technique d’apprentissage automatique, qui est le raisonnement à partir de cas (RàPC). Pour cela, nous avons présenté dans le deuxième chapitre un état de l’art sur l’apprentissage automatique et ses différentes méthodes en mettant l’accent essentiellement sur le RàPC et ses utilisations pour le diagnostic des systèmes industriels. Cette étude nous a permis de proposer dans le chapitre 3 une approche d’aide au diagnostic qui se base sur le RàPC. Cette approche s’appuie sur une phase hors ligne et une phase en ligne. La phase hors ligne permet de définir un format de représentation de cas et de construire une base de cas normaux (BCN) et une base de cas défaillants (BCD) à partir d’une base de données d’historique. La phase en ligne permet d’aider les opérateurs humains de surveillance à la prise de la décision du diagnostic la plus adéquate. Les résultats des expérimentations sur un système de tri de caisses ont présentés les piliers de cette approche qui résident au niveau du format de représentation de cas proposé et au niveau de la base de cas utilisé. Pour résoudre ces problèmes et améliorer les résultats, un nouveau format de représentation de cas est proposé dans le chapitre 4. Selon ce format et à partir des données issues du système simulé après son émulation en mode normal et fautif, les cas de la base de cas initiale sont construits. Ensuite, une phase de raisonnement et d’apprentissage incrémental est présentée. Cette phase permet non seulement le diagnostic du système surveillé mais aussi d’enrichir la base de cas suite à l’apparition des nouveaux comportements inconnus. Les expérimentations présentées dans le chapitre 5 sur « le plateau tournant » qui est un sous système du système « tri de caisses » ont permis de montrer l’amélioration des résultats et aussi d’évaluer et de comparer les performances de l’approche proposée vis-à-vis certaines approches d’apprentissage automatique et vis-à-vis une approche à base de modèle pour le diagnostic du plateau tournant. / Automated production systems (APS) represents an important class of industrial systems that are increasingly complex given the large number of interactions and interconnections between their different components. As a result, they are more susceptible to malfunctions, whose consequences can be significant in terms of productivity, safety and quality of production. A major challenge is to develop an intelligent approach that can be used to diagnose these systems to ensure their operational safety. In this thesis, we are only interested in the diagnosis of APS with discrete dynamics. We present in the first chapter these systems, the possible malfunctions and the used terminology for the diagnosis. Then, we present a state of the art of the existing methods for the diagnosis of this class of systems and also a synthesis of these methods. This synthesis motivated us to choose a data-based approach that relies on a machine learning technique, which is Case-Based Reasoning (CBR). For this reason, we presented in the second chapter a state of the art on machine learning and its different methods with a focus mainly on the CBR and its uses for the diagnosis of industrial systems. This study allowed us to propose in Chapter 3 a Case Based Decision Support System for the diagnosis of APS. This system is based on an online block and an offline block. The Offline block is used to define a case representation format and to build a Normal Case Base (NCB) and a Faulty Case Base (FCB) from a historical database. The online block helps human operators of monitoring to make the most appropriate diagnosis decision. The experiments results perform on a sorting system presented the pillars of this approach, which reside in the proposed case representation format and in the used case base. To solve these problems and improve the results, a new case representation format is proposed in chapter 4. According to this format and from the data acquired from the simulated system after its emulation in normal and faulty mode, cases of the initial case base are build. Then, a reasoning and incremental learning phase is presented. This phase allows the system diagnosis and the enrichment of the case base following the appearance of new unknown behaviors. The experiments presented in Chapter 5 and perform on the 'turntable' which is a subsystem of the 'sorting system” allowed to show the improvement of the results and also to evaluate and compare the performances of the proposed approach with some automatic learning approaches and with a model-based approach to turntable diagnosis.

Le travail présenté dans ce mémoire s'inscrit dans le domaine de la supervision des systèmes automatisés de production. Il traite plus particulièrement de la synthèse de lois de surveillance adaptées aux exigences des entreprises. La loi de surveillance est obtenue à partir d'un modèle de référence pour la supervision, la commande et la surveillance. Ce dernier fournit l'ensemble exhaustif de tous les traitements de supervision, de commande et de surveillance qui peuvent être appliqués en situation de défaillances au cours d'un cycle de production et ce, quel que soit le système de production considéré. La méthode de synthèse proposée s'appuie sur une démarche proche de la synthèse de correcteurs en automatique continue. Elle revient à raffiner successivement le modèle de référence par intégration progressive d'un ensemble de quatre propriétés qui doivent être recherchées. Ces propriétés, la sécurité, l'écologie, la qualité et la productivité sont à évaluer par le concepteur au moyen de grilles mettant en relation l'impact de quatre symptômes de défaillances sur l'ensemble des propriétés recherchées et ce, en fonction de la ressource physique considérée. Un exemple d'application basé sur un processus manufacturier réel, la plate-forme de recherche en productique SAPHIR du Laboratoire d'Automatique de Grenoble, illustre les apports de notre approche. Ces derniers se déclinent en terme de flexibilité des traitements proposés, de systématisation de la méthode proposée et de respect des propriétés recherchées.

Cette thèse présente une analyse de la consommation d'énergie des systèmes de contrôlecommande électriques des machines automatisées en vue de réduire leur consommation d'énergie. Il est notamment présenté les notions associées aux systèmes de contrôle-commande et il est développé des méthodes et un simulateur de consommation d'énergie destiné à l'analyse de la consommation d'énergie. A partir de ceci, il est réalisé une analyse selon 3 axes : consommation des composants de contrôlecommande pris individuellement, consommation des systèmes de contrôle-commande selon le type de machine et l'assemblage des composants et enfin, consommation dans le temps selon les modes de marche. Ces travaux mettent en évidence que la consommation des systèmes de contrôle-commande est souvent faible comparée à celle des actionneurs, mais qu'il est tout de même possible de réduire d'un facteur 2 la consommation d'énergie.

The main objective of this research program was to assess the status of clinical knowledge and evidence-based practice in the medical management of mass casualties, contaminated by exposure to a chemical weapon, during a medical evacuation, which is defined as from the incident site of a contaminated environment up-to a clean zone. First, in our published systematic review, we assessed past medical responses during a chemical attack. The lack of clinical data and intervention-related information, such as protection and decontamination capabilities, stresses not only the need to study acute or prehospital settings, but also a set of integrated competences in the contaminated environment (i.e.: protection, decontamination and clinical interventions) (Prospero registered CRD42019104473). Second, a method paper which presents an ongoing international retro-prospective observational study on the medical responses during a chemical attack has been submitted for publication. The goal of this study is to describe the acute clinical management of patients in the contaminated zone (1970-2036; US Clinical trial registered NCT05026645). Data gathering is currently ongoing with the use of a comprehensive online registry programmed by the Quebec Respiratory Health Research Network. In the third and fourth, we started the development of two technological innovations to improve the medical management of mass casualties, caused by a chemical weapon, in contaminated environments. The first is the creation of a mobile laboratory for the continuity of our work in both indoor and outdoor settings. The other is the launch of a research program, named VIMY Multi-System, which includes: (1) An electronic casualty card system integrating the United Kingdom National Early Warning System; (2) a forward-deployable telemedicine capability prototype – currently undergoing integration testing – that incorporates drone technology to monitor patients being clinically managed in a simulated chemically contaminated environment. Our fifth published paper, on the methods of oxygen conservation with an automated titration system (n= 60; US Clinical trial registered NCT02782936 and NCT02809807), showed that such an automated system may constitute a viable medical solution for interventions in a contaminated environment and also constitutes one of the possible solutions to improve therapeutic interventions. The system studied allows the maintenance of adequate oxygenation while reducing the use of oxygen in patients, making it possible to extend their treatment duration even under conditions of limited logistical resources in oxygen. The oxygen flow provided by the automated system allows a mean reduction in administered oxygen quantities of more than six-fold when decreasing the prescribed SpO2 target from 98 to 90% (5 L/min to1 L/min, p <0.001) in hospitalized patients with respiratory disorders. The comparison was conducted on the basis of conservative flow rate targets reported in the literature (2.5, 5.0, 10.0 and 15.0 l/min). When it comes to the automated correction of a hypoxemic condition in sick patients and healthy subjects wearing a gas mask, the prescribed SpO2 target resulted in maximum administered oxygen flow rates of 0.2 L/min and 2.9 L/min respectively. These results show a possible logistic and therapeutic optimization in the use of oxygen. Finally, these initial advances will be integrated as our research work progresses in order to improve clinical evidence-based practices in contaminated environments due to the use of chemical weapons. / L’objectif principal de cette recherche était d’évaluer l’état des connaissances et le savoir-faire de la pratique clinique dans la gestion d’un grand nombre de blessés, contaminés des suites d’une exposition à l’arme chimique, pendant leur évacuation médicale depuis le site de l’incident dans un environnement contaminé jusqu’à la zone propre. Premièrement, dans une revue systématique que nous avons publiée, nous avons évalué les réponses médicales passées lors d’attaques chimiques. Le manque de données cliniques et d’autres informations liées à l’intervention, tel que les capacités de protection et de décontamination, souligne non seulement la nécessité d’étudier l’environnement préhospitalier, mais aussi la gamme de compétences interdépendantes en milieu contaminé (c.-à-d. : protection, décontamination et interventions cliniques) (Prospero CRD42019104473). Deuxièmement, nous avons soumis pour publication la méthodologie d’une étude rétroprospective observationnelle internationale s’intéressant aux réponses médicales lors d’une attaque chimique. Le but consiste à décrire la gestion clinique en soins aigus des blessés dans la zone contaminée (1970-2036) (ClinicalTrials.gov NCT05026645). L’acquisition de données est en cours à l’aide d’un registre de données intégral en ligne qui a été programmé par le Réseau de recherche en santé respiratoire du Québec. En troisième et quatrième lieu, nous avons entrepris le développement de deux innovations technologiques afin d’améliorer la prise en charge médicale des patients en milieu contaminé à la suite de l’utilisation de l’arme chimique. L’un est la création d’un laboratoire mobile pour poursuivre nos travaux tant à l’intérieur qu’à l’extérieur. L’autre est la mise sur pied d’un programme de recherche, nommé VIMY Multi-Systèmes, qui inclut : (1) un système de carte de blessés électronique intégrant le système national d’alerte précoce du Royaume-Uni, (2) les premiers tests d’intégration d’un prototype d’une capacité de télémédecine de déploiement avancé, incluant la technologie du drone, pour une surveillance clinique globale des patients pris en charge en milieu contaminé chimique simulé. Notre cinquième publication, qui porte sur les méthodes de maintien de l’oxygénation par titrage automatisée (n=60 ; ClinicalTrials.gov NCT02782936 et NCT02809807), nous a permis de démontrer qu’un système automatisé peut constituer une solution médicale intéressante qui serait applicable dans les interventions en milieu contaminé et de surcroît comme une solution pour améliorer les actions thérapeutiques. Le système que nous avons étudié permet de maintenir une oxygénation adéquate tout en limitant la consommation d’oxygène des patients, prolongeant ainsi leur durée de traitement, notamment en cas de ressources en oxygène limitées. D’une part, le débit de l’oxygène fourni par le système automatisé a permis une réduction moyenne des quantités administrées de l’ordre de plus de six fois lors de la diminution de la cible de saturation en oxygène (SpO2) prescrite de 98 à 90 % (5 L/min à 1 L/min, p < 0,001) chez les patients hospitalisés atteints de maladies respiratoires. La comparaison s’est faite par rapport à des débits conservateurs rapportés dans la littérature (2,5, 5,0, 10,0 et 15,0 L/min). D’autre part, la correction automatisée d’une condition hypoxémique chez les patients malades et les sujets sains portant le masque à gaz, la cible SpO2 a engendré des débits maximaux d’oxygènes administrés de 2,5 et 2,9 L/min respectivement. Ainsi, nous avons démontré une optimalisation logistique et thérapeutique de la consommation de l’oxygène. Finalement, ces premières avancées seront intégrées au fur et à mesure de l’avancement de nos recherches afin d’améliorer le processus de soins en milieu contaminé issu de l’utilisation de l’arme chimique.

L'objectif principal de cette thèse est la caractérisation des dynamiques hautes fréquance en milieu côtier et en particulier leurs extrêmes, par l'intermédiaire de l'étude de série temporelle biogéochimiques à long terme enregistrées par des systèmes automatisés. Les bases de données hautes fréquences utilisées dans cette étude proviennent majoritairement du programme MAREL, qui a été mise en oeuvre par l'IFREMER. Des séries temporelles basses fréquences provenant des programmes de surveillance du littoral SOMLIT (CNRS, INSU) et SRN (Ifremer) sont mises à contribution pour appuyer l'importance des systèmes automatisés. La méthode EMD (Empirical Mode Decomposition) nous a servi de base dans de nombreuses analyses pour étudier ces séries temporelles. Nous avons aussi utilisé des méthodes plus classiques empruntées aux domaines de l'analyse numérique et de la turbulence. Cette études se décompose en 3 parties, et plusieurs annexes. Les matériels et méthodes sont présentés dans la première partie. Dans la seconde partie, la méthode EMD nous a permis de mettre en avant les fortes fluctuations contenues dans les blooms, ainsi que de mener des analyses spectrales grâce à un couplage avec la transformée de Hilbert. L'analyse en composante principale (ACP) a mis en avant les principaux forçages exercés sur la production primaire et les profils de température SOMLIT laissent supposer un impact de la stratification sur l'intensité des blooms. Dans la troisième partie, nous avons mené une étude comparative entre les données basses fréquences et hautes fréquences. Et deux méthodes de cross-corrélation (TDIC et co-spectre) nous ont permis de définir une échelle caractéristique de transition entre les températures de la Manche occidentale et orientale. En annexe, nous avons testé la robustesse de différentes méthodes d'analyses spectrales quant au manque de données dans les séries temporelles, qui est un problème inhérent aux bases de données enregistrées par des systèmes automatisés, et nous avons reproduit un article qui est en cours de soumission. / The main objective of this thesis is the characterization of high frequency dynamics in coastal areas and in particular their extremes, through the study of long-term biodeochemical time series registered by automated systems. The majority of high-frequency data sets used in this study came from MAREL program. The low-frequency time series from coastal monitoring programs SOMLIT (CNRS, INSU) and SRN (Ifremer) are employed to support the importance of automated systems. The EMD (Empirical Mode decomposition) method has provided a basis for us to study several of these time series. We also have used some methods more classical borrowed from numerical analysis field and turbulence. This study is organized in three chapters, and several appendices. The first chapter is devoted to the material and method. In the second chapter, using the EMD method we have highlighted the strong fluctuations contained in the blooms, and we have performed spectral analyzes. The principal component analysis (PCA) highlighted the main forcing exerted on primary production and SOMLIT temperature profiles suggest an impact of stratification on the intensity of blooms. In the third chapter, we conducted a comparative study between low-frequency and high-frequency data. Two cross-correlation methods (TDIC and co-spectra) allowed us to define a characteristic transition scale between the temperatures of the western and eastern English Cahnnel. In appendices we tested the robustness of different spectral analysis methods about the missing data in the time series, which is an underlying problem in the database registered by automated systems, and we reproduce a paper, which is under submission.