La croissance du commerce électronique exige une hausse des performances des systèmes d'entreposage, qui sont maintenant repensés pour faire face à un volume massif de demandes à être satisfait le plus rapidement possible. Le système manuel et le système à robots mobile (SRM) sont parmi les plus utilisés pour ces activités. Le premier est un système centré sur l'humain pour réaliser des opérations complexes que les robots actuels ne peuvent pas effectuer. Cependant, les nouvelles générations de robots autonomes mènent à un remplacement progressif par le dernier pour augmenter la productivité. Quel que soit le système utilisé, plusieurs problèmes interdépendants doivent être résolus pour avoir des processus de stockage et de prélèvement efficaces. Les problèmes de stockage concernent les décisions d'où stocker les produits dans l'entrepôt. Les problèmes de prélèvement incluent le regroupement des commandes à exécuter ensemble et les itinéraires que les cueilleurs et les robots doivent suivre pour récupérer les produits demandés. Dans le système manuel, ces problèmes sont traditionnellement résolus à l'aide de politiques simples que les préparateurs peuvent facilement suivre. Malgré l'utilisation de robots, la même stratégie de solution est répliquée aux problèmes équivalents trouvés dans le SRM. Dans cette recherche, nous étudions les problèmes de stockage et de prélèvement rencontrés lors de la conception du système manuel et du SRM. Nous développons des outils d'optimisation pour aider à la prise de décision pour mettre en place leurs processus, en améliorant les mesures de performance typiques de ces systèmes. Certains problèmes traditionnels sont résolus avec des techniques améliorées, tandis que d'autres sont intégrés pour être résolus ensemble au lieu d'optimiser chaque sous-système de manière indépendante. Nous considérons d'abord un système manuel avec un ensemble connu de commandes et intégrons les décisions de stockage et de routage. Le problème intégré et certaines variantes tenant compte des politiques de routage communes sont modélisés mathématiquement. Une métaheuristique générale de recherche de voisinage variable est présentée pour traiter des instances de taille réelle. Des expériences attestent de l'efficience de la métaheuristique proposée par rapport aux modèles exacts et aux politiques de stockage communes. Lorsque les demandes futures sont incertaines, il est courant d'utiliser une stratégie de zonage qui divise la zone de stockage en zones et attribue les produits les plus demandés aux meilleures zones. Les tailles des zones sont à déterminer. Généralement, des dimensions arbitraires sont choisies, mais elles ignorent les caractéristiques de l'entrepôt et des demandes. Nous abordons le problème de dimensionnement des zones pour déterminer quels facteurs sont pertinents pour choisir de meilleures tailles de zone. Les données générées à partir de simulations exhaustives sont utilisées pour trainer quatre modèles de régression d'apprentissage automatique - moindres carrés ordinaire, arbre de régression, forêt aléatoire et perceptron multicouche - afin de prédire les dimensions optimales des zones en fonction de l'ensemble de facteurs pertinents identifiés. Nous montrons que tous les modèles entraînés suggèrent des dimensions sur mesure des zones qui performent meilleur que les dimensions arbitraires couramment utilisées. Une autre approche pour résoudre les problèmes de stockage pour le système manuel et pour le SRM considère les corrélations entre les produits. L'idée est que les produits régulièrement demandés ensemble doivent être stockés près pour réduire les coûts de routage. Cette politique de stockage peut être modélisée comme une variante du problème d'affectation quadratique (PAQ). Le PAQ est un problème combinatoire traditionnel et l'un des plus difficiles à résoudre. Nous examinons les variantes les plus connues du PAQ et développons une puissante métaheuristique itérative de recherche tabou mémétique en parallèle capable de les résoudre. La métaheuristique proposée s'avère être parmi les plus performantes pour le PAQ et surpasse considérablement l'état de l'art pour ses variantes. Les SRM permettent de repositionner facilement les pods d'inventaire pendant les opérations, ce qui peut conduire à un processus de prélèvement plus économe en énergie. Nous intégrons les décisions de repositionnement des pods à l'attribution des commandes et à la sélection des pods à l'aide d'une stratégie de prélèvement par vague. Les pods sont réorganisés en tenant compte du moment et de l'endroit où ils devraient être demandés au futur. Nous résolvons ce problème en utilisant la programmation stochastique en tenant compte de l'incertitude sur les demandes futures et suggérons une matheuristique de recherche locale pour résoudre des instances de taille réelle. Nous montrons que notre schéma d'approximation moyenne de l'échantillon est efficace pour simuler les demandes futures puisque nos méthodes améliorent les solutions trouvées lorsque les vagues sont planifiées sans tenir compte de l'avenir. Cette thèse est structurée comme suit. Après un chapitre d'introduction, nous présentons une revue de la littérature sur le système manuel et le SRM, et les décisions communes prises pour mettre en place leurs processus de stockage et de prélèvement. Les quatre chapitres suivants détaillent les études pour le problème de stockage et de routage intégré, le problème de dimensionnement des zones, le PAQ et le problème de repositionnement de pod. Nos conclusions sont résumées dans le dernier chapitre. / The rising of e-commerce is demanding an increase in the performance of warehousing systems, which are being redesigned to deal with a mass volume of demands to be fulfilled as fast as possible. The manual system and the robotic mobile fulfillment system (RMFS) are among the most commonly used for these activities. The former is a human-centered system that handles complex operations that current robots cannot perform. However, newer generations of autonomous robots are leading to a gradual replacement by the latter to increase productivity. Regardless of the system used, several interdependent problems have to be solved to have efficient storage and picking processes. Storage problems concern decisions on where to store products within the warehouse. Picking problems include the batching of orders to be fulfilled together and the routes the pickers and robots should follow to retrieve the products demanded. In the manual system, these problems are traditionally solved using simple policies that pickers can easily follow. Despite using robots, the same solution strategy is being replicated to the equivalent problems found in the RMFS. In this research, we investigate storage and picking problems faced when designing manual and RMFS warehouses. We develop optimization tools to help in the decision-making process to set up their processes and improve typical performance measures considered in these systems. Some classic problems are solved with improved techniques, while others are integrated to be solved together instead of optimizing each subsystem sequentially. We first consider a manual system with a known set of orders and integrate storage and routing decisions. The integrated problem and some variants considering common routing policies are modeled mathematically. A general variable neighborhood search metaheuristic is presented to deal with real-size instances. Computational experiments attest to the effectiveness of the metaheuristic proposed compared to the exact models and common storage policies. When future demands are uncertain, it is common to use a zoning strategy to divide the storage area into zones and assign the most-demanded products to the best zones. Zone sizes are to be determined. Commonly, arbitrary sizes are chosen, which ignore the characteristics of the warehouse and the demands. We approach the zone sizing problem to determine which factors are relevant to choosing better zone sizes. Data generated from exhaustive simulations are used to train four machine learning regression models - ordinary least squares, regression tree, random forest, and multilayer perceptron - to predict the optimal zone sizes given the set of relevant factors identified. We show that all trained models suggest tailor-made zone sizes with better picking performance than the arbitrary ones commonly used. Another approach to solving storage problems, both in the manual and RMFS, considers the correlations between products. The idea is that products constantly demanded together should be stored closer to reduce routing costs. This storage policy can be modeled as a quadratic assignment problem (QAP) variant. The QAP is a traditional combinatorial problem and one of the hardest to solve. We survey the most traditional QAP variants and develop a powerful parallel memetic iterated tabu search metaheuristic capable of solving them. The proposed metaheuristic is shown to be among the best performing ones for the QAP and significantly outperforms the state-of-the-art for its variants. The RMFS allows easy repositioning of inventory pods during operations that can lead to a more energy-efficient picking process. We integrate pod repositioning decisions with order assignment and pod selection using a wave picking strategy such that pods are parked after being requested considering when and where they are expected to be requested next. We solve this integrated problem using stochastic programming considering the uncertainty about future demands and suggest a local search matheuristic to solve real-size instances. We show that our sample average approximation scheme is effective to simulate future demands since our methods improve solutions found when waves are planned without considering the future demands. This thesis is structured as follows. After an introductory chapter, we present a literature review on the manual and RMFS, and common decisions made to set up their storage and picking processes. The next four chapters detail the studies for the integrated storage and routing problem, the zone sizing problem, the QAP, and the pod repositioning problem. Our findings are summarized in the last chapter.

Pour rester compétitives, les entreprises forestières cherchent à contrôler leurs coûts d’approvisionnement. Les abatteuses-façonneuses sont pourvues d’ordinateurs embarqués qui permettent le contrôle et l’automatisation de certaines fonctions. Or, ces technologies ne sont pas couramment utilisées et sont dans le meilleur des cas sous-utilisées. Tandis que l’industrie manifeste un intérêt grandissant pour l’utilisation de ces ordinateurs, peu de travaux de recherche ont porté sur l’apport en productivité et en conformité aux spécifications de façonnage découlant de l’usage de ces systèmes. L’objectif de l’étude était de mesurer les impacts des trois degrés d’automatisation (manuel, semi-automatique et automatique) sur la productivité (m3/hmp) et le taux de conformité des longueurs et des diamètre d’écimage des billes façonnées (%). La collecte de données s’est déroulée dans les secteurs de récolte de Produits forestiers résolu au nord du Lac St-Jean entre les mois de janvier et d'août 2015. Un dispositif en blocs complets a été mis en place pour chacun des cinq opérateurs ayant participé à l’étude. Un seuil de 5 % a été employé pour la réalisation de l’analyse des variances, après la réalisation de contrastes. Un seul cas a présenté un écart significatif de productivité attribuable au changement du degré d’automatisation employé, tandis qu’aucune différence significative n’a été détectée pour la conformité des diamètres d’écimage; des tendances ont toutefois été constatées. Les conformités de longueur obtenues par deux opérateurs ont présenté des écarts significatifs. Ceux-ci opérant sur deux équipements distincts, cela laisse entrevoir l’impact que peut aussi avoir l’opérateur sur le taux de conformité des longueurs. / All forest companies try to control their supply costs. Single-grip harvesters are equipped with onboard computers that allow control and automation of some functions. However, these technologies are not used on a regular basis and are in the best cases underutilized. While industrials are showing a growing interest in the utilization of these systems, there have been only a few studies that have documented the impacts of the use of these systems on productivity and quality conformity. The objective of this study was to measure the impacts on productivity and on bucking quality of different degrees of automation of the bucking of a single-grip harvester head. Three different automation degrees, manual, semi-automatic and automatic, have been compared with two different teams composed of 5 operators. Each operator was a different case study. Comparisons were realized on the obtained productivities and on the conformities of the logs lengths and topping diameters. Data collection was made on the logging sites operated by Resolute forest products, in the northern part of Lac St-Jean between January and August 2015. A 5% significance level has been used to realise the variances analysis, where contrasts were employed. Only one case study showed a significant productivity difference linked to the in the automation degree changes. Even if the collected data did not show significant differences on the topping diameters conformities, some tendencies were detected. However, significant differences were detected on the conformity of the lengths of the logs of two operators. Because those two operators work on different harvesters, this might show that the operator can have an impact on the lengths conformity.

Des stations de mesure de la qualité de l’eau sont utilisées pour mesurer la qualité de l'eau à haute fréquence. Pour une gestion efficace de ces mesures, la qualité des données doit être vérifiée. Dans une méthode univariée précédemment développée, des points aberrants et des fautes étaient détectés dans les données mesurées par ces stations en employant des modèles à lissage exponentiel pour prédire les données au moment suivant avec l’intervalle de confiance. Dans la présente étude, ne considérant que le cas univarié, la détection de points aberrants est améliorée par l’identification d’un modèle autorégressif à moyenne mobile sur une fenêtre mobile de données pour prédire la donnée au moment suivant. Les données de turbidité mesurées à l'entrée d'une station d'épuration municipale au Danemark sont utilisées comme étude de cas pour comparer la performance de l’utilisation des deux modèles. Les résultats montrent que le nouveau modèle permet de prédire la donnée au moment suivant avec plus de précision. De plus, l’inclusion du nouveau modèle dans la méthode univariée présente une performance satisfaisante pour la détection de points aberrants et des fautes dans les données de l'étude de cas. / Water quality monitoring stations are used to measure water quality at high frequency. For effective data management, the quality of the data must be evaluated. In a previously developed univariate method both outliers and faults were detected in the data measured by these stations by using exponential smoothing models that give one-step ahead forecasts and their confidence intervals. In the present study, the outlier detection step of the univariate method is improved by identifying an auto-regressive moving average model for a moving window of data and forecasting one-step ahead. The turbidity data measured at the inlet of a municipal treatment plant in Denmark is used as case study to compare the performance of the use of the two models. The results show that the forecasts made by the new model are more accurate. Also, inclusion of the new forecasting model in the univariate method shows satisfactory performance for detecting outliers and faults in the case study data.

L’automatisation de la détection et de l’identification des animaux est une tâche qui a de l’intérêt dans plusieurs domaines de recherche en biologie ainsi que dans le développement de systèmes de surveillance électronique. L’auteur présente un système de détection et d’identification basé sur la vision stéréo par ordinateur. Plusieurs critères sont utilisés pour identifier les animaux, mais l’accent a été mis sur l’analyse harmonique de la reconstruction en temps réel de la forme en 3D des animaux. Le résultat de l’analyse est comparé avec d’autres qui sont contenus dans une base évolutive de connaissances. / Automating the detection and identification of animals is a task that has an interest in many biological research fields and in the development of electronic security systems. The author present a detection and identification system based on computer stereo vision to achieve this task. A number of criteria are being used to identify the animals, but the emphasis is on the harmonic analysis of the animal real time reconstructed 3D shape. The result of the analysis is compared with others stored in an evolutive knowledge base.

Cette thèse s'inscrit dans la démarche de preuve de programmes à l'aide de vérification déductive. La vérification déductive consiste à produire, à partir des sources d'un programme, c'est-à-dire ce qu'il fait, et de sa spécification, c'est-à-dire ce qu'il est sensé faire, une conjecture qui si elle est vraie alors le programme et sa spécification concordent. On utilise principalement des démonstrateurs automatiques pour montrer la validité de ces formules. Quand ons'intéresse à la preuve de programmes qui utilisent des structures de données allouées en mémoire, il est élégant et efficace de spécifier son programme en utilisant la logique de séparation qui est apparu il y a une dizaine d'année. Cela implique de prouver des conjectures comportant les connectives de la logique de séparation, or les démonstrateurs automatiques ont surtout fait des progrès dans la logique du premier ordre qui ne les contient pas.Ce travail de thèse propose des techniques pour que les idées de la logique de séparation puissent apparaître dans les spécifications tout en conservant la possibilité d'utiliser des démonstrateurs pour la logique du premier ordre. Cependant les conjectures que l'ont produit ne sont pas dans la même logique du premier ordre que celles des démonstrateurs. Pour permettre une plus grande automatisation, ce travail de thèse a également défini de nouvelles conversions entre la logique polymorphe du premier ordre et la logique multi-sortée dupremier ordre utilisé par la plupart des démonstrateurs.La première partie a donné lieu à une implémentation dans l'outil Jessie, la seconde a donné lieu à une participation conséquente à l'écriture de l'outil Why3 et particulièrement dans l'architecture et écriture des transformations qui implémentent ces simplifications et conversions. / This thesis comes within the domain of proofs of programs by deductive verification. The deductive verification generates from a program source and its specification a mathematical formula whose validity proves that the program follows its specification. The program source describes what the program does and its specification represents what the program should do. The validity of the formula is mainly verified by automatic provers. During the last ten years separation logic has shown to be an elegant way to deal with programs which use data-structures with pointers. However it requires a specific logical language, provers, and specific reasoning techniques.This thesis introduces a technique to express ideas from separation logic in the traditional framework of deductive verification. Unfortunately the mathematical formulas produced are not in the same first-order logic than the ones of provers. Thus this work defines new conversions between the polymorphic first-order logic and the many-sorted logic used by most proves.The first part of this thesis leads to an implementation in the Jessietool. The second part results in an important participation to the writing of the Why3 tool, in particular in the architecture and writing of the transformations which implement these conversions.

La biologie a connu une extraordinaire révolution avec l'arrivée de nombreux génomes entièrement séquencés. L'analyse de la quantité d'informations disponibles nécessite la création et l'utilisation d'outils informatiques automatisés. L'interprétation des données biologiques prend tout son sens à la lumière de l'évolution. En ce sens, les études évolutives sont incontestablement nécessaires pour donner un sens aux données biologiques. Dans ce contexte, le laboratoire développe des outils pour étudier l'évolution des génomes (et protéomes) à travers les mutations subies. Cette thèse porte sur l'étude spécifique des événements de pertes de gènes unitaires. Ces événements peuvent révéler des pertes de fonctions très instructives pour comprendre l'évolution des espèces. En premier lieu, j'ai développé l'outil GLADX qui mime l'expertise humaine afin d'étudier automatiquement et avec précision les événements de pertes de gènes unitaires. Ces études se basent sur la création et l'interprétation de données phylogénétiques, de BLAST, de prédictions protéiques, etc., dans un contexte automatisé. Ensuite, j'ai développé une stratégie utilisant l'outil GLADX pour étudier à grande échelle les pertes de gènes unitaires au cours de l'évolution du protéome humain. La stratégie utilise d'abord comme filtre l'analyse de groupes d'orthologues fabriqués par un outil de clustérisation à partir du protéome complet de nombreuses espèces. Cette analyse a permis de détecter 6237 pertes de gènes unitaires putatives dans la lignée humaine. L'étude approfondie de ces pertes avec GLADX a mis en évidence de nombreux problèmes liés à la qualité des données disponibles dans les bases de données. / Biology has undergone an extraordinary revolution with the appearance of numerous whole genomes sequenced. Analysis of the amount of information available requires creation and use of automated tools. The interpretation of biological data becomes meaningful in light of evolution. In view of all this, evolutionary studies are undoubtedly necessary to highlight the biological data. In this context, the laboratory develops tools to study the genomes (and proteomes) evolution through all the undergone mutations. The project of this thesis focuses specifically on the events of unitary gene losses. These events may reveal loss of functions very instructive for understanding the evolution of species. First, I developed the GLADX tool that mimics human expertise to automatically and accurately investigate the events of unitary gene losses. These studies are based on the creation and interpretation of phylogenetic data, BLAST, predictions of protein, etc., in an automated environment. Secondly, I developed a strategy using GLADX tool to study, at large-scale, the loss of unitary genes during the evolution of the human proteome. The strategy uses, in the first step, the analysis of orthologous groups produced by a clustering tool from complete proteomes of numerous species. This analysis used as a filter, allowed detecting 6237 putative losses in the human lineage. The study of these unitary gene loss cases has been deepened with GLADX and allowed to highlight many problems with the quality of available data in databases.

Plusieurs études ont récemment fait l'hypothèse qu'un déficit de l'apprentissage procédural commun aux troubles neurodéveloppementaux pouvait permettre d'expliquer leur fréquente association (Nicolson et Fawcett, 2007). Tout spécialement, les circuits neuronaux impliqués dans cet apprentissage (les boucles cortico-striatale, CS et cortico-cérébelleuse, CC) pouvaient rendre compte avec pertinence de la comorbidité fréquente entre Dyslexie Développementale (DD) et Trouble de l'Acquisition de la Coordination (TAC) : 40 à 60% des enfants présentent en effet la double association. Les circuits neuronaux qui soutiennent l'apprentissage d'une séquence motrice et en particulier d'une tâche de tapping de doigts (FTT, Finger Tapping Task) sont bien connus et modélisés (Doyon, Bellec, Amsel, Penhune, Monchi, Carrier et al., 2009) et concernent tout particulièrement ces deux boucles CS et CC. Nous avons donc choisi dans cette thèse d'observer les modifications cérébrales lors de l'apprentissage d'une FTT, chez des enfants âgés de 8 à 12 ans présentant une DD, un TAC ou l'association des deux troubles. Dans un premier temps, nous avons effectué une analyse des données issues des tests neurospychologiques de l'ensemble des enfants de l'étude (20 DD, 22 TAC et 23 DysTAC). Nos résultats ne montrent pas de différences entre les trois groupes aux tests attentionnels, comportementaux et psychosociaux. Nous trouvons des différences aux subtests du WISC-IV en rapport avec les capacités visuospatiales et motrices (Cubes, Symboles, Indice de Vitesse de Traitement) où le groupe DD se montre plus performant que le groupe TAC. Aucune différence n'est retrouvée entre le groupe comorbide et les deux autres groupes, suggérant d'une part un profil cognitif partagé et commun aux troubles neurodéveloppementaux et d'autre part le caractère non cumulatif de l'association des deux troubles. Dans un second temps, nous avons analysé les données issues de l'imagerie fonctionnelle par résonnance magnétique (IRMf) des 48 enfants ayant effectués la partie IRM (16 DD, 16 TAC et 16 DysTAC) afin d'explorer les activités cérébrales lors de la réalisation d'une FTT à deux stades de l'apprentissage (début d'apprentissage et stade automatique après quinze jours d'entraînement). Nos résultats indiquent que les trois groupes d'enfants ont été capable d'accéder à l'automatisation de la FTT après un entraînement approprié, mais en utilisant des processus cérébraux compensatoires différents entre les groupes. Nos résultats ne confirment pas les hypothèses et le modèle théorique de Nicolson, postulant des déficits spécialisés des boucles CS ou CC en fonction des troubles. Par contre, nos résultats mettent très nettement en évidence des mécanismes cérébraux spécifiques aux enfants TAC. Ces derniers présentent en effet une suractivation des aires attentionnelles et un recrutement de zones cérébrales plus important lors de performances similaires à celles des autres enfants. En dernier lieu, nos données indiquent que les groupes DD et DysTAC présentent un profil commun, tant dans les résultats neuropsychologiques que dans les résultats d'imagerie, alors que le groupe TAC est clairement singulier dans son fonctionnement. / Many studies have pointed out the high frequency of co-morbid associations in neurodevelopmental disorders. However, few of them have given details of cognitive functions in developmental dyslexia (DD) and developmental coordination disorder (DCD) children and still fewer on the association of DD and DCD. The main purpose of this article is to compare the intellectual characteristics of the 3 populations and, in particular, to investigate the cognitive profiles of children with co-occurrence. Recent theories consider that procedural learning may support frequent overlap between neurodevelopemental disorders. In particular, the brain networks involved in this learning (cortico-striatal (CS) and cortico-cerebellar (CC) loops) could account for frequent co-morbidity between DCD and DD (about 40 to 60% of DD and DCD subjects suffer from both disorders). The aim of our study was to investigate cerebral changes due to the motor sequence learning process, especially the finger-tapping task (FTT), from acquisition through automatization, in children with DD, DCD, or DD and DCD. The neural circuitry supporting this action is well-known and well-modelled (Doyon et al., 2009), and includes, among others, CC and CS loops. Functional magnetic resonance imaging (fMRI) in 48 children (8-12 years old) with neurodevelopmental disorders (16 DD, 16 DCD and 16 DD+DCD) explored their brain activity during FTT, performed either after 2 weeks of training or in the early stage of learning. First, we analyzed the results in all participants (22 DCD, 20 DD and 23 DD+DCD) in tests assessing cognitive (WISC-IV), attentional (CPT-II) and behavioural (CBCL) abilities. No difference was found between the 3 groups in attention testing (CPT) and behavioural characteristics (CBCL). Significant between-groups differences were observed in Processing Speed Index (PSI) score and the block design and symbol search subtests. Post hoc group comparisons showed that DD fared better than DCD children. No significant differences were found between the co-morbid vs. pure groups: co-morbid association did not cause an accumulation of disorders. Second, our results indicated that all children with DD, DCD or both disorders performed the tasks with good automaticity, but suggested that different compensatory brain processes allowed them to access this automatization stage. Our fMRI results do not appear to confirm Nicolson's model but tend more towards shared disability in CS and CC loops for both DD and DCD, with slight between-group differences in these areas. Moreover, and in agreement with the results of previous fMRI studies in DCD children, our data disclosed increasing evidence that this group needs to invest more brain areas to achieve similar performances. Lastly, it appears that the co-morbid and DD groups are very close in cognitive profile (especially on WISC-IV) and in neural correlates associated with our paradigm, while the DCD group presents specific, distinct and particular characteristics. Our data therefore indicate a promising direction for future research on the neural mechanisms linked with learning in neurodevelopmental disorders and in understanding co-morbidity.

Les propriétés que l’on souhaite exprimer sur les applications système d’information ne peuvent se restreindre aux propriétés statiques, dites propriétés d’invariance, qui portent sur des états du système pris au même moment. En effet, certaines propriétés, dites propriétés dynamiques, peuvent faire référence à l’état passé ou futur du système. Les travaux existants sur la vérification de telles propriétés utilisent généralement le model checking dont l’efficacité pour le domaine des systèmes d’information est plutôt réduite à cause de l’explosion combinatoire de l’espace des états. Aussi, les techniques, fondées sur la preuve, requièrent des connaissances assez avancées en termes de raisonnement mathématique et sont donc difficiles à mettre en œuvre d’autant plus que ces dernières ne sont pas outillées. Pour palier ces limites, nous proposons dans cette thèse des méthodes de vérification de propriétés dynamiques basées sur la preuve en utilisant la méthode formelle B. Nous nous intéressons principalement aux propriétés d’atteignabilité et de précédence pour lesquelles nous avons défini des méthodes de génération d’obligations de preuve permettant de les prouver. Une propriété d’atteignabilité permet d’exprimer qu’il existe au moins une exécution du système qui permet d’atteindre un état cible à partir d’un état initial donné. Par contre, la propriété de précédence permet de s’assurer qu’un état donné du système est toujours précédé par un autre état. Afin de rendre ces différentes approches opérationnelles, nous avons développé un outil support qui permet de décharger l’utilisateur de la tâche de génération d’obligations de preuve qui peut être longue et fastidieuse / The properties that we would like to express on data-intensive applications cannot be limited to static properties, called invariance properties, which depend on states taken at the same time. Indeed, some properties, called dynamic properties, may refer to the past or the future states of the system. Existing work on the verification of such properties typically use model checking whose effectiveness for data-intensive applications is rather limited due to the combinatorial explosion of the state space. In addition, the techniques, based on the proof, require fairly advanced knowledge and mathematical reasoning especially that they are not always supported by tools. To overcome these limitations, we propose in this thesis proof-based verification approaches that use the B formal method. We are mainly interested in reachability and precedence properties for which we defined formal rules to generate proof obligations that permit to discharge them. A reachability property expresses that there is at least one execution scenario that permits to reach a target state from a given initial state while a precedence property ensures that a given system state is always preceded by another state. To make these different approaches workable, we have developed a support tool that permits to discharge the users from tedious and error-prone tasks

Ce travail concerne la réalisation d'une électrode enzymatique utilisable pour le suivi en ligne (<i>on-line</i>) d'un procédé de fermentation. Cette étude a nécessité la mise au point d'une nouvelle technique d'immobilisation, applicable à différentes enzymes. Elle est basée sur la formation de liaisons covalentes entre l'enzyme et l'agent portant: le glutaraldéhyde. La méthode consiste en une adsorption de l'enzyme suivie du dépôt, par vaporisation, de l'agent réticulant sur l'extrémité sensible des électrodes de pH en verre. Ce procédé d'immobilisation assure un temps de réponse extrêmement court du biocapteur. Cette performance est un avantage indéniable pour des mesures en continu, tel qu'un système d'analyse par injection en flux continu (FIA). Par la suite, nous avons développé des systèmes FIA incorporant trois différents types de cellules de détection appropriées aux besoins analytiques. Des électrodes à pénicillinase et à uréase, préparées selon la méthode décrite ci-dessus, ont été installées et utilisées dans ces cellules. Les systèmes biocapteurs-FIA, ainsi conçus, ne nécessitent alors ni réacteur enzymatique, ni réactif. De plus, le temps de réponse très court du biocapteur allie aux avantages de la FIA et aux spécificités des cellules a permis d'obtenir une cadence de mesure très élevée. Ce système d'analyse a été applique aux mesures en ligne de la concentration de pénicilline au cours de sa production fermentaire et aux mesures automatiques de l'urée dans les échantillons de sérum humain. Pour cela, nous avons automatise le système biocapteur-FIA et conçu une nouvelle cellule a écoulement agite pour l'installation des électrodes à uréase et a pénicillinase. Ce système biocapteur-FIA donne des résultats satisfaisants pour la détermination de l'urée et surtout s'est révélé extrêmement performant pour le suivi hors ligne et en ligne de la concentration de pénicilline pendant plusieurs fermentations d'une durée de 250 heures environ. Dans ce dernier cas, la comparaison des mesures effectuées avec le système biocapteur-FIA et une méthode classique de dosage (HPLC) est favorable à l'analyseur biocapteur-FIA qui assure des mesures en ligne avec une bonne fiabilité et a un moindre cout, mais aussi en raison de sa simplicité. En rendant possible une exploitation immédiate des mesures en ligne de la concentration en pénicilline par l'ordinateur central de l'installation fermentaire, le système biocapteur-FIA présente un pas important dans l'amélioration du contrôle et/ou de la modélisation des bioprocédés.

La numérisation 3D telle que pratiquée aujourd'hui repose essentiellement sur les connaissances de l'opérateur qui la réalise. La qualité des résultats reste très sensible à la procédure utilisée et par conséquent aux compétences de l'opérateur. Ainsi, la numérisation manuelle est très coûteuse en ressources humaines et matérielles et son résultat dépend fortement du niveau de technicité de l'opérateur. Les solutions de numérisation les plus avancées en milieu industriel sont basées sur une approche d'apprentissage nécessitant une adaptation manuelle pour chaque pièce. Ces systèmes sont donc semi-automatiques compte tenu de l'importance de la contribution humaine pour la planification des vues.Mon projet de thèse se focalise sur la définition d'un procédé de numérisation 3D automatique et intelligente. Ce procédé est présenté sous forme d'une séquence de processus qui sont la planification de vues, la planification de trajectoires, l'acquisition et les post-traitements des données acquises. L'originalité de notre démarche de numérisation est qu'elle est générique parce qu'elle n'est pas liée aux outils et méthodes utilisés pour la réalisation des tâches liées à chaque processus. Nous avons également développé trois méthodes de planification de vues pour la numérisation d'objets sans connaissance a priori de leurs formes. Ces méthodes garantissent une indépendance des résultats par rapport au savoir-faire de l'opérateur. L'originalité de ces approches est qu'elles sont applicables à tous types de scanners. Nous avons implanté ces méthodes sur une cellule de numérisation robotisée. Nos approches assurent une reconstruction progressive et intelligente d'un large panel d'objets de différentes classes de complexité en déplaçant efficacement le scanner