Cette thèse aborde les difficultés de mise au point de codes multicibles - c'est-à-dire de codes dont performances sont portables entre différentes cibles matérielles. Nous avons identifié deux principales difficultés à surmonter : l'unification de l'expression du parallélisme d'une part et la nécessité d'adapter le format de stockage des données d'autre part. Afin de mettre au point une version multicible de la bibliothèque d'algèbre linéaire Legolas++ mise au point à EDF R&D, nous avons conçu MTPS (MultiTarget Parallel Skeleton), une bibliothèque dédiée à la mise au point de codes multicible. MTPS permet d'obtenir une implémentation multicible pour les problèmes appliquant une même fonction aux différents éléments d'une collection. MTPS prend alors en charge l'adaptation du format de stockage des données en fonction de l'architecture ciblée. L'intégration des concepts de MTPS dans Legolas++ a conduit à l'obtention d'un prototype multicible de Legolas++. Ce prototype a permis de mettre au point des solveurs dont les performances sont proches de l'optimal sur différentes architectures matérielles / This thesis addresses the challenges of developing multitarget code - that is to say, codes whose performance is portable across different hardware targets. We identified two key challenges : the unification of the the parallelism expression and the need to adapt the format for storing data according to the target architecture. In order to develop a multitarget version of Legolas++, a linear algebra library developed at EDF R&D, we designed MTPS (Multi-Tatget Parallel Skeleton), a library dedicated to the development of multitarget codes. MTPS allows for multitarget implementations of problems that apply the same function to all the elements of a collection. MTPS then handles the adaptation of the format for storing data according to the targeted architecture. Integrating the concepts of MTPS in Legolas++ has led to the production of a multitarget prototype of Legolas++. This prototype has allowed the development of solvers whose performances near the harware limits on different hardware architectures

Cette thèse porte sur l'historisation des données dans les bases de données graphes. La problématique des données en graphes existe depuis longtemps mais leur exploitation par des moteurs de système de gestion de bases de données, principalement dans les moteurs NoSQL, est récente. Cette apparition est notamment liée à l'émergence des thématiques Big Data dont les propriétés intrinsèques, souvent décrites à l'aide des propriétés 3V (variété, volume, vélocité), ont révélé les limites des bases de données relationnelles classiques. L'historisation quant à elle, est un enjeu majeur des SI qui a été longtemps abordé seulement pour des raisons techniques de sauvegarde, de maintenance ou plus récemment pour des raisons décisionnelles (suites applicatives de Business Intelligence). Cependant, cet aspect s'avère maintenant prendre une place prédominante dans les applications de gestion. Dans ce contexte, les bases de données graphes qui sont de plus en plus utilisées n'ont que très peu bénéficié des apports récents de l'historisation. La première contribution consiste à étudier le nouveau poids des données historisées dans les SI de gestion. Cette analyse repose sur l'hypothèse selon laquelle les applications de gestion intègrent de plus en plus en leur sein les enjeux d'historisation. Nous discutons ce positionnement au regard de l'analyse de l'évolution des SI par rapport à cette problématique. La deuxième contribution vise, au-delà de l'étude de l'évolution des sytèmes d'information, à proposer un modèle innovant de gestion de l'historisation dans les bases de données NoSQL en graphes. Cette proposition consiste d'une part en l'élaboration d'un système unique et générique de représentation de l'historique au sein des BD NoSQL en graphes et d'autre part à proposer des modes d'interrogation (requêtes). Nous montrons qu'il est possible d'utiliser ce système aussi bien pour des requêtes simples (c'est-à-dire correspondant à ce que l'on attend en première intention d'un système d'historisation~: récupérer les précédentes versions d'une donnée) mais aussi de requêtes plus complexes qui permettent de tirer parti aussi bien de la notion d'historisation que des possibilités offertes par les bases de données graphes (par exemple, la reconnaissance de motifs dans le temps). / This thesis deals with data historization in the context of graphs. Graph data have been dealt with for many years but their exploitation in information systems, especially in NoSQL engines, is recent. The emerging Big Data and 3V contexts (Variety, Volume, Velocity) have revealed the limits of classical relational databases. Historization, on its side, has been considered for a long time as only linked with technical and backups issues, and more recently with decisional reasons (Business Intelligence). However, historization is now taking more and more importance in management applications.In this framework, graph databases that are often used have received little attention regarding historization. Our first contribution consists in studying the impact of historized data in management information systems. This analysis relies on the hypothesis that historization is taking more and more importance. Our second contribution aims at proposing an original model for managing historization in NoSQL graph databases.This proposition consists on the one hand in elaborating a unique and generic system for representing the history and on the other hand in proposing query features.We show that the system can support both simple and complex queries.Our contributions have been implemented and tested over synthetic and real databases.

Le monde des appareils mobiles permet aux utilisateurs d’installer des applications sur des terminaux personnels, mais pose des lacunes en termes de sécurité, car les utilisateurs n’ont ps les moyens de juger la dangerosité d’une application, et le risque de nuisibilité ne peut pas être limité après l’installation. Nous étudions l’analyse statique en tant qu’outil de détection de risques et de malware. Notre méthode se caractérise par un pilotage par règles, opérant sur des programmes partiels : l’un des objectifs est de proposer un langage spécifique au domaine pouvant exprimer un domaine abstrait et associer des comportements aux fonctions des librairies du système. L’expressivité est un atout important qui est obtenu au travers de l’abstraction. La technologie mobile évolue rapidement et de nouvelles manières de développer les appli- cations apparaissent fréquemment. Une analyse statique des applications doit absolument réagir rapidement à l’arrivée des nouvelles technologies, de sorte à ne pas se retrouver obsolète. Nous montrons de quelle manière il est possible de réaliser des analyses statiques que l’on peut réutiliser entre plusieurs plateformes de smartphones / The mobile device world allows users to install applications on theirpersonal devices, but typically falls short in terms of security, because theusers lack any ability to judge if an application will be dangerous, and thereis no way to limit the harmfulness of a program after it is installed.We explore static analysis as a tool for risk assessment and detection of malware behavior. Our method characterizes as a rule-driven, partial program approach: one of our goals is to provide a convenient, expressive domain-specific language to express an abstract domain and associate behavior to the library functions of the system.Expressivity is an important asset to have and it is obtained by the means of abstraction. The mobile technologies evolve fast and new ways to develop programs frequently appear.A real-world static analysis solution absolutely needs to react fast to the arrival of new technologies, in order not to fall into obsolescence. Weshow how it is possible to develop static analyses, and then to reuse them across mutiple smartphone platforms.

Le volume des données ne cesse de croître. À tel point qu'on parle aujourd'hui de "Big Data". La principale raison se trouve dans les progrès des outils informatique qui ont offert une grande flexibilité pour produire, mais aussi pour stocker des quantités toujours plus grandes. Les méthodes d'analyse de données ont toujours été confrontées à des quantités qui mettent en difficulté les capacités de traitement, ou qui les dépassent. Pour franchir les verrous technologiques associés à ces questions d'analyse, la communauté peut se tourner vers les techniques de calcul distribué. En particulier, l'extraction de motifs, qui est un des problèmes les plus abordés en fouille de données, présente encore souvent de grandes difficultés dans le contexte de la distribution massive et du parallélisme. Dans cette thèse, nous abordons deux sujets majeurs liés à l'extraction de motifs : les motifs fréquents, et les motifs informatifs (i.e., de forte entropie). / Le volume des données ne cesse de croître. À tel point qu'on parle aujourd'hui de "Big Data". La principale raison se trouve dans les progrès des outils informatique qui ont offert une grande flexibilité pour produire, mais aussi pour stocker des quantités toujours plus grandes.à l'extraction de motifs : les motifs fréquents, et les motifs informatifs (i.e., de forte entropie).

Si la pertinence de la prise en compte de la météorologie dans la gestion du trafic est bien admise, son intégration dans les outils d'aide à la décision et les stratégies de contrôle représente encore un enjeu réel pour les gestionnaires d'infrastructures. En effet, cette avancée semble légitimée par les effets significatifs d'une météorologie dégradée sur la sécurité des usagers et le comportement des conducteurs. Ainsi, au niveau de la sécurité, un sur-risque d'accident a été mis en évidence par de nombreux travaux. Or, l'étiologie de ce risque augmenté ne permet pas seulement de démontrer l'impact d'évènements météorologiques extrêmes et ponctuels (ex : tempêtes de neige), mais égalementcelui de phénomènes récurrents (ex : la pluie). La baisse de la sécurité des conducteurs se traduit concrètement par un changement de comportements des usagers (vitesses, temps inter-véhiculaires) mais aussi du flot de véhicules en général (vitesse, débit, concentration), ceci influant de manière conséquente sur la mobilité. De fait, la pluie représente ainsi la seconde cause de congestion ponctuelle.Pourtant, malgré ces enjeux indéniables, les effets de la météorologie sur le trafic demeurent mal quantifiés et ne sont guère intégrés à la modélisation ou l'estimation du trafic. Ce travail de thèse se propose ainsi de contribuer à une meilleure compréhension des effets météorologiques sur le trafic, en se focalisant sur des phénomènes de précipitations en milieu interurbain. Partant d'un état de l'art de l'impact météorologique sur le trafic, il nous est apparu que les études existantes, par leurs carences, soulèvent le besoin de fonder une méthodologie d'analyse plus rigoureuse. Cette méthodologie, une fois clairement définie, a ensuite été appliquée à des données opérationnelles. Elle nous a permis de quantifier les effets de la pluie à plusieurs niveaux selon l'échelle de représentation abordée : au niveau microscopique, considérant le comportement individuel des conducteurs, les analyses statistiques mettent en lumière des effets sur les vitesses, les temps et les distances inter-véhiculaires. Ces effets se reflètent au niveau macroscopique (celui du flot de véhicules) avec des variations de débits, de vitesses du flot et, de façon générale, de l'ensemble des paramètres formant le diagramme fondamental du trafic. Les résultats empiriques nous semblent ainsi ouvrir la voie à l'intégration du phénomène météorologique à la modélisation du trafic.Partant, nous avons développé, à ce stade de notre travail, une contribution théorique à la modélisation du trafic se fondant sur une formulation Vlasov qui permet de dériver un modèle macroscopique à deux équations à partir d'une formulation cinétique. Le modèle ainsi proposé offre un cadre propice à l'intégration d'un paramètre météorologique. La discrétisation numérique du modèle s'effectue à l'aide d'une méthode à pas fractionnaire qui permet de traiter successivement le terme source et la partie homogène du système. Pour la partie homogène du système, nous avons fait l'usage d'un schéma de type Lagrange+remap. Le comportement du modèle, couplé à une équation de transport sur les temps inter-véhiculaires, a ensuite été illustré à travers une série d'expérimentations numériques qui ont mis en évidence ses aptitudes face à des conditions météorologiques changeantes.Dans un ultime volet, notre travail s'est orienté vers de futures applications en temps réel qui se placeraient dans un cadre bayesien d'assimilation de données. Le défi à relever est celui de l'estimation en ligne du vecteur d'état du trafic au fur et à mesure de l'arrivée de nouvelles observations. Une méthode de filtrage particulaire (Monte Carlo séquentielle) nous a paru judicieuse à mobiliser, car elle s'adapte bien à la problématique du trafic routier. Plusieurs scénarios fondés sur des données opérationnelles permettent ensuite de montrer les bénéfices de l'intégration du phénomène météorologique à de telles approches. Une meilleure connaissance du phénomène météorologique doit ainsi mener à son insertion dans les modèles de trafic qui forment le substrat des outils d'aide à la décision destinés aux gestionnaires.Le travail proposé ouvre donc des perspectives pour le développement de stratégies de gestion de trafic météo-sensibles. / The integration of the weather effects into decision support tools and real time traffic management strategies represents a critical need for all road operators. The motivations are clear because of the significant effects of adverse weather on road safety and drivers' behaviors. At a safety level, the increase of the crash frequency and severity has been highlighted by several studies. This increase of the crash risk does not concern only extreme weather events, such as winter storms, but also recurring events like rain. The changes in drivers' behaviors (decrease of speeds, headways) andtraffic flow dynamics (speed, flow, density) lead to significant consequences from a mobility point of view : thus, rain represents the second largest cause of non recurring congestion (15 \%) after incidents.In spite of this context, the effects of adverse weather on traffic are not well quantified and, above all, not integrated into traffic modelling and estimation. The presented thesis research aims at contributing to a better understanding of the meteorological effects on traffic by focusing on precipitation events at interurban sections. From a literature review of the meteorological impact on traffic, we have underlined a need of a standardized methodology. Such a standardized methodology for the rain impact quantification is proposed and applied to real data. It enables aquantification of the rain effects at different levels, according to the scale of representation : at a microscopic level, the statistical analyses highlight changes in drivers speeds, time headways. Those effects reflect on the macroscopic level of traffic flow with changes in speed, flows, and, in a general way, in all the parameters composing the fundamental diagram of traffic. Hence, the empirical results pave the way for integrating the meteorological phenomenon into traffic modelling.Next, we propose a theoretical contribution to traffic modelling, based on a Vlasov formulation, which enables the derivation of a two equations macroscopic model. The proposed model offers a relevant framework for the integration of a meteorological parameter. Regarding the numerical discretization, we propose a fractionnal step method allowing to deal successively with the source terme and the homogeneous part of the system. We develop a Lagrange+remap scheme for the homogeneous part of the system. The model behaviour is illustrated through several numerical experiments which highlight the model features faced with changing meteorological conditions.In the last chapter, an effort towards future online applications is put forward. Within a Bayesian framework for data assimilation, the goal resides in the online estimation of the traffic state vector given current measurements. Based on real world data, some scenarios show the benefits of the integration of the meteorology into such approaches. Thus, a better knowledge of the weather impact on traffic leads to its integration into traffic models and will enable the improvement of decision support tools for road operators. The proposed work opens perspectives for the development ofweather-responsive traffic management strategies.

Ces travaux de thèse s’inscrivent dans le contexte technico/économique des nanomatériaux notamment les nanoparticules et les copolymères. Aujourd’hui, une révolution technologique est en cours avec l’introduction de ces matériaux dans des matrices plus ou moins complexes présentes dans notre quotidien (santé, cosmétique, bâtiment, agroalimentaire...). Ces matériaux confèrent à ces produits des propriétés uniques (mécanique, électrique, chimique, thermique, ...). Cette omniprésence associée aux enjeux économiques engendre deux problématiques liées au contrôle des procédés de fabrication et à la métrologie associée. La première est de garantir une traçabilité de ces nanomatériaux afin de prévenir tout risque sanitaire et environnemental et la seconde est d’optimiser le développement des procédés afin de pérenniser des filières économiques rentables. Pour cela, les deux techniques les plus courantes de métrologie utilisées sont : la microscopie électronique à balayage (MEB) et la microscopie à force atomique (AFM).Le premier volet des travaux est consacré au développement d’une méthodologie de fusion de données permettant d’analyser automatiquement les données en provenance de chaque microscope et d’utiliser leurs points forts respectifs afin de réduire les incertitudes de mesure en trois dimensions. Une première partie a été consacrée à la correction d’un défaut majeur d’asservissement de l’AFM qui génère des dérives et/ou sauts dans les signaux. Nous présentons une technique dirigée par les données permettant une correction de ces signaux. La méthode présentée a l’avantage de ne pas faire d’hypothèses sur les objets et leurs positions. Elle peut être utilisée en routine automatique pour l’amélioration du signal avant l’analyse des objets.La deuxième partie est consacrée au développement d’une méthode d’analyse automatique des images de nanoparticules sphériques en provenance d’un AFM ou d’un MEB. Dans le but de développer une traçabilité en 3D, il est nécessaire d’identifier et de mesurer les nanoparticules identiques qui ont été mesurées à la fois sur l’AFM et sur le MEB. Afin d’obtenir deux estimations du diamètre sur la même particule physique, nous avons développé une technique qui permet de mettre en correspondance les particules. Partant des estimations pour les deux types de microscopie, avec des particules présentes dans les deux types d'images ou non, nous présentons une technique qui permet l'agrégation d’estimateurs sur les populations de diamètres afin d'obtenir une valeur plus fiable des propriétés du diamètre des particules.Le second volet de cette thèse est dédié à l’optimisation d’un procédé de fabrication de copolymères à blocs (structures lamellaires) afin d’exploiter toutes les grandeurs caractéristiques utilisées pour la validation du procédé (largeur de ligne, période, rugosité, taux de défauts) notamment à partir d’images MEB afin de les mettre en correspondance avec un ensemble de paramètres de procédé. En effet, lors du développement d’un nouveau procédé, un plan d’expériences est effectué. L’analyse de ce dernier permet d’estimer manuellement une fenêtre de procédé plus ou moins précise (estimation liée à l’expertise de l’ingénieur matériaux). L’étape est réitérée jusqu’à l’obtention des caractéristiques souhaitées. Afin d’accélérer le développement, nous avons étudié une façon de prédire le résultat du procédé de fabrication sur l’espace des paramètres. Pour cela, nous avons étudié différentes techniques de régression que nous présentons afin de proposer une méthodologie automatique d’optimisation des paramètres d’un procédé alimentée par les caractéristiques d’images AFM et/ou MEB.Ces travaux d’agrégations d’estimateurs et d’optimisation de fenêtre de procédés permettent d’envisager le développement d’une standardisation d’analyse automatique de données issues de MEB et d’AFM en vue du développement d’une norme de traçabilité des nanomatériaux. / This thesis is included in the technical and economical context of nanomaterials, more specifically nanoparticles and block copolymer. Today, we observe a technological revolution with the introduction of these materials into matrices more or less complex present in our daily lives (health, cosmetics, buildings, food ...). These materials yield unique properties to these products (mechanical, electrical, chemical, thermal ...). This omnipresence associated with the economic stakes generates two problems related to the process control and associated metrology. The first is to ensure traceability of these nanomaterials in order to prevent any health and environmental risks and the second is to optimize the development of processes in order to sustain profitable economic sectors. For this, the two most common metrology techniques used are: scanning electron microscopy (SEM) and atomic force microscopy (AFM).The first phase of the work is devoted to the development of a data fusion methodology that automatically analyzes data from each microscope and uses their respective strengths to reduce measurement uncertainties in three dimensions. A first part was dedicated to the correction of a major defect of the AFM which generates drifts and / or jumps in the signals. We present a data-driven methodology, fast to implement and which accurately corrects these deviations. The proposed methodology makes no assumption on the object locations and can therefore be used as an efficient preprocessing routine for signal enhancement before object analysis.The second part is dedicated to the development of a method for automatic analysis of spherical nanoparticle images coming from an AFM or a SEM. In order to develop 3D traceability, it is mandatory to identify and measure the identical nanoparticles that have been measured on both AFM and SEM. In order to obtain two estimations of the diameter on the same physical particle, we developed a technique that allows to match the particles. Starting from estimates for both types of microscopy, with particles present in both kinds of images or not, we present a technique that allows the aggregation of estimators on diameter populations in order to obtain a more reliable value of properties of the particle diameter.The second phase of this thesis is dedicated to the optimization of a block copolymer process (lamellar structures) in order to capitalize on all the characteristic quantities used for the validation of the process (line width, period, roughness, defects rate) in particular from SEM images for the purpose of matching them with a set of process parameters.Indeed, during the development of a new process, an experimental plan is carried out. The analysis of the latter makes it possible to manually estimate a more or less precise process window (estimate related to the expertise of the materials engineer). The step is reiterated until the desired characteristics are obtained. In order to accelerate the development, we have studied a way of predicting the result of the process on the parameter space. For this, we studied different regression techniques that we present to propose an automatic methodology for optimizing the parameters of a process powered by AFM and / or SEM image characteristics.This work of estimator aggregation and process window optimization makes it possible to consider the development of a standardization of automatic analysis of SEM and AFM data for the development of a standard for traceability of nanomaterials.

L'interopérabilité des applications est devenue le leitmotiv des développeurs et concepteurs en ingénierie système. La plupart des approches pour l'interopérabilité existant dans l'entreprise ont pour objectif principal l'ajustement et l'adaptation des types et structures de données nécessaire à la mise en œuvre de collaboration entre entreprises. Dans le domaine des entreprises manufacturières, le produit est une composante centrale. Des travaux scientifiques proposent des solutions pour la prise en compte des systèmes d'information issus des produits, tout au long de leur cycle de vie. Mais ces informations sont souvent non corrélées. La gestion des données de produit (PDM) est couramment mise en œuvre pour gérer toute l'information relative aux produits durant tout leur cycle de vie. Cependant, ces modèles sont généralement des "îlots" indépendants ne tenant pas compte de la problématique d'interopérabilité des applications supportant ces modèles. L'objectif de cette thèse est d'étudier cette problématique d'interopérabilité appliquée aux applications utilisées dans l'entreprise manufacturière et de définir un modèle ontologique de la connaissance des entreprises relatives aux produits qu'elles fabriquent, sur la base de leurs données techniques. Le résultat de ce travail de recherche concerne la formalisation d'une méthodologie d'identification des informations de gestion techniques des produits, sous la forme d'une ontologie, pour l'interopérabilité des applications d'entreprises manufacturières, sur la base des standards existants tels que l'ISO 10303 et l'IEC 62264. / In recent years, the enterprise applications interoperability has become the leitmotiv of developers and designers in systems engineering. Most approaches to interoperability in the company have the primary objective of adjustment and adaptation of types and data structures necessary for the implementation of collaboration between companies. In the field of manufacturing, the product is a central component. Scientific works propose solutions taking into account information systems derived from products technical data throughout their life cycle. But this information is often uncorrelated. The management of product data (PDM) is commonly implemented to manage all information concerning products throughout their life cycle. The modelling of management and manufacturing processes is widely applied to both physical products and services. However, these models are generally independent “islands” ignoring the problem of interoperability between applications that support these models. The objective of this thesis is to study the problem of interoperability applied to applications used in the manufacturing environment and to define a model of the ontological knowledge of enterprises related to the products they manufacture, based on technical data, ensuring the interoperability of enterprise systems. The outcome of this research concerns the formalization of a methodology for identifying a product-centric information system in the form of an ontology, for the interoperability of applications in manufacturing companies, based on existing standard such as ISO 10303 and IEC 62264.

Comme les syst`emes mat´eriels et logiciels grandissent de fa¸con continue en ´echelle et fonctionnalit´es, la probabilit´e d’erreurs subtiles de- vient toujours plus grande. Les techniques d’abstraction, souvent bas´ees sur l’interpr´etation abstraite de Cousot, fournissent une m´ethode pour ex´ecuter symboliquement les syst`emes en utilisant le domaine abstrait `a la place du domaine concret. Dans cette th`ese, on introduit des techniques d’abstraction pour les logiques sous des interpr´etations multi-valu´ees. Beaucoup d’applications des logiques multi-valu´ees ont ´et´e trouv´ees dans la v´erification du mat´eriel et du logiciel. Pour la v´erification du mat´eriel, des outils de simulation et des r´ealisations des circuits multi-valu´es v´eritables ont ´et´e propos´es, les risques dynamiques ont ´et´e model´es en introduisant des ´etats faux pour trouver des r´egions chevauchantes des signaux en concurrence, etc. Pour la v´erification du logiciel on a besoin d’incertitude parce qu’on ne peut savoir si certains comportements devraient ˆetre possibles et on a besoin du d´esaccord parce que l’on peut avoir des acteurs diff´erents qui sont en d´esaccord pour la mani`ere dont les syst`emes devraient se comporter. Les abstractions sont obtenues en appliquant des relations d’´equivalence et apr`es, les symboles pr´edicatifs de la logique sont red´efinis `a s’appliquer cor- rectement aux classes d’´equivalence `a l’aide des politiques d’interpr´etation. On fournit des r´esultats de pr´eservation pour la logique de premier ordre, pour la logique temporelle et pour la logique temporelle de la connaissance. Avant de discuter les abstractions multi-valu´ees pour la logique temporelle, nous pr´esentons une ´etude de cas pour utiliser l’abstraction dans le contexte des mod`eles du contrˆole d’acc`es. Nous fournirons aussi une technique d’abstraction pour les types de do- nn´ees. Cette technique d’abstraction peut ˆetre ´elargie pour les types abstraits de donn´ees. Ici, les abstractions sont appliqu´ees aux sp´ecifications initiales au moyen des ´equations et ils sont appel´es des abstractions ´equationnelles. De plus, la technique d’abstraction pr´esent´ee g´en´eralise et clarifie la nature de beaucoup de techniques d’abstraction trouv´ees dans la litt´erature, telles: la technique de dupliquer les symboles pr´edicatifs, shape analysis, l’abstraction par pr´edicats, l’approche de McMillan, etc. Pour raisonner au sujet des syst`emes dynamiques, on introduit les types de donn´ees dynamiques et on ´etend la m´ethode d’abstraction ant´erieure `a ce cas. Le probl`eme principal qui survient quand on utilise les abstractions est de trouver l’abstraction convenable ou de raffiner une abstraction d´ej`a existante pour en obtenir une meilleure. On prouve que les techniques d’abstraction que nous avons introduites pour les types de donn´ees sous l’interpr´etation 3- valu´ee Kleene, peuvent ˆetre utilis´ees dans une proc´edure de raffinement. De plus, on montre que la proc´edure de raffinement guid´e par contre-exemple est plus efficace quand on l’utilise sous les abstractions ´equationnelles / As the hardware and software systems are growing continuously in scale and functionality, the likelihood of subtle errors becomes greater. Abstraction techniques, often based on abstract interpretation, provide a method for symbolically executing systems using the abstract instead of the concrete domain. In this thesis, we are concerned with abstractions for logics under multi-valued interpretations. Many applications of multi-valued logics have been found in hardware and software verification. For hardware verification, simulation tools and imple- mentations of genuinely multi-valued circuits have been proposed, dynamic hazards have been modeled by introducing pseudo states to find overlapping regions of competing signals, implementation of gates have been verified on the basis of switch level models, etc. For software verification, we need uncer- tainty because we may not know whether some behaviors should be possible, we need disagreement because we may have different stakeholders that dis- agree about how the systems should behave and we need to represent relative importance because some behaviors are essential and others may or may not be implemented. The abstractions are obtained by applying equivalence relations and then, the predicate symbols of the logic are re-defined to work properly on equiva- lence classes by using interpretation policies. We provide preservation results for first-order logic, temporal logic, and temporal logic of knowledge. As a case study, we show how abstraction can be used to solve the safety problem for protection systems which model access control policies. The use of abstraction in the context of data types, is also investigated. This technique scales well from data types to abstract data types. Here, abstractions are applied to initial specifications by means of equations and they are called equationally specified abstractions. Moreover, the abstraction technique we propose generalizes and clarifies the nature of many abstraction techniques found in the literature, such as the technique of duplicating pred- icate symbols, shape analysis, predicate abstraction, McMillan’s approach, etc. To reason about dynamic systems, we introduce dynamic data types and extend the previous abstraction technique to this case. The main problem that arises when using abstraction techniques is to find the suitable abstraction or to refine an already existing abstraction in order to obtain a better one. In this thesis, we prove that the abstraction techniques for data types, under Kleene’s three-valued interpretation, can be used in a refinement procedure. Moreover, we show that the counterexample guided abstraction refinement procedure (CEGAR) works better when used with equationally specified abstractions

Ce travail de thèse s’insère dans un projet de recherche plus global dont l’objectif est d’analyser le potentiel migratoire de cellules cancéreuses. Dans le cadre de ce doctorat, on s’intéresse à l’utilisation du traitement des images pour dénombrer et classifier les cellules présentes dans une image acquise via un microscope. Les partenaires biologistes de ce projet étudient l’influence de l’environnement sur le comportement migratoire de cellules cancéreuses à partir de cultures cellulaires pratiquées sur différentes lignées de cellules cancéreuses. Le traitement d’images biologiques a déjà donné lieu `a un nombre important de publications mais, dans le cas abordé ici et dans la mesure où le protocole d’acquisition des images acquises n'était pas figé, le défi a été de proposer une chaîne de traitements adaptatifs ne contraignant pas les biologistes dans leurs travaux de recherche. Quatre étapes sont détaillées dans ce mémoire. La première porte sur la définition des prétraitements permettant d’homogénéiser les conditions d’acquisition. Le choix d’exploiter l’image des écarts-type plutôt que la luminosité est un des résultats issus de cette première partie. La deuxième étape consiste à compter le nombre de cellules présentent dans l’image. Un filtre original, nommé filtre «halo», permettant de renforcer le centre des cellules afin d’en faciliter leur comptage, a été proposé. Une étape de validation statistique de ces centres permet de fiabiliser le résultat obtenu. L’étape de segmentation des images, sans conteste la plus difficile, constitue la troisième partie de ce travail. Il s’agit ici d’extraire des «vignettes», contenant une seule cellule. Le choix de l’algorithme de segmentation a été celui de la «Ligne de Partage des Eaux», mais il a fallu adapter cet algorithme au contexte des images faisant l’objet de cette étude. La proposition d’utiliser une carte de probabilités comme données d’entrée a permis d’obtenir une segmentation au plus près des bords des cellules. Par contre cette méthode entraine une sur-segmentation qu’il faut réduire afin de tendre vers l’objectif : «une région = une cellule». Pour cela un algorithme utilisant un concept de hiérarchie cumulative basée morphologie mathématique a été développée. Il permet d’agréger des régions voisines en travaillant sur une représentation arborescente de ces régions et de leur niveau associé. La comparaison des résultats obtenus par cette méthode à ceux proposés par d’autres approches permettant de limiter la sur-segmentation a permis de prouver l’efficacité de l’approche proposée. L’étape ultime de ce travail consiste dans la classification des cellules. Trois classes ont été définies : cellules allongées (migration mésenchymateuse), cellules rondes «blebbantes» (migration amiboïde) et cellules rondes «lisses» (stade intermédiaire du mode de migration). Sur chaque vignette obtenue à la fin de l’étape de segmentation, des caractéristiques de luminosité, morphologiques et texturales ont été calculées. Une première analyse de ces caractéristiques a permis d’élaborer une stratégie de classification, à savoir séparer dans un premier temps les cellules rondes des cellules allongées, puis séparer les cellules rondes «lisses» des «blebbantes». Pour cela on divise les paramètres en deux jeux qui vont être utilisés successivement dans ces deux étapes de classification. Plusieurs algorithmes de classification ont été testés pour retenir, au final, l’utilisation de deux réseaux de neurones permettant d’obtenir plus de 80% de bonne classification entre cellules longues et cellules rondes, et près de 90% de bonne classification entre cellules rondes «lisses» et «blebbantes». / This thesis is part of a broader research project which aims to analyze the potential migration of cancer cells. As part of this doctorate, we are interested in the use of image processing to count and classify cells present in an image acquired usinga microscope. The partner biologists of this project study the influence of the environment on the migratory behavior of cancer cells from cell cultures grown on different cancer cell lines. The processing of biological images has so far resulted in a significant number of publications, but in the case discussed here, since the protocol for the acquisition of images acquired was not fixed, the challenge was to propose a chain of adaptive processing that does not constrain the biologists in their research. Four steps are detailed in this paper. The first concerns the definition of pre-processing steps to homogenize the conditions of acquisition. The choice to use the image of standard deviations rather than the brightness is one of the results of this first part. The second step is to count the number of cells present in the image. An original filter, the so-called “halo” filter, that reinforces the centre of the cells in order to facilitate counting, has been proposed. A statistical validation step of the centres affords more reliability to the result. The stage of image segmentation, undoubtedly the most difficult, constitutes the third part of this work. This is a matter of extracting images each containing a single cell. The choice of segmentation algorithm was that of the “watershed”, but it was necessary to adapt this algorithm to the context of images included in this study. The proposal to use a map of probabilities as input yielded a segmentation closer to the edges of cells. As against this method leads to an over-segmentation must be reduced in order to move towards the goal: “one region = one cell”. For this algorithm the concept of using a cumulative hierarchy based on mathematical morphology has been developed. It allows the aggregation of adjacent regions by working on a tree representation ofthese regions and their associated level. A comparison of the results obtained by this method with those proposed by other approaches to limit over-segmentation has allowed us to prove the effectiveness of the proposed approach. The final step of this work consists in the classification of cells. Three classes were identified: spread cells (mesenchymal migration), “blebbing” round cells (amoeboid migration) and “smooth” round cells (intermediate stage of the migration modes). On each imagette obtained at the end of the segmentation step, intensity, morphological and textural features were calculated. An initial analysis of these features has allowed us to develop a classification strategy, namely to first separate the round cells from spread cells, and then separate the “smooth” and “blebbing” round cells. For this we divide the parameters into two sets that will be used successively in Two the stages of classification. Several classification algorithms were tested, to retain in the end, the use of two neural networks to obtain over 80% of good classification between long cells and round cells, and nearly 90% of good Classification between “smooth” and “blebbing” round cells.

Le programme international Argo a révolutionné l'observation globale des océans. Une flotte de plus de 3000 instruments sous-marins autonomes est en place, programmés pour fournir des mesures globales de profils de température et de salinité sur les 2000 premiers mètres de l'océan. Ces mesures sont assimilées dans des modèles océaniques conjointement aux observations satellitaires afin de décrire et prévoir l'océan. Dans cette thèse nous proposons une analyse permettant de caractériser les erreurs d'un modèle global océanique par comparaison aux données du réseau Argo. Ces erreurs sont décrites via leurs amplitudes, leurs variations régionales et temporelles ainsi que via les échelles spatiales associées. Une caractérisation des échelles spatiales à la fois pour la variabilité océanique et pour les erreurs modèles est, en particulier, menée permettant de relier la structure des erreurs modèles à celle du signal. Enfin, des techniques basées sur le contenu en information sont testées afin de pouvoir à terme mieux quantifier l'impact des observations Argo sur les systèmes d'assimilation de Mercator Océan. / The international Argo program has revolutionized the observation of the global ocean. An array of more than 3000 profiling floats is in place and provides global measurements of temperature and salinity on the first 2000 meters of the ocean. These measurements are assimilated into ocean models together with satellite observations to describe and forecast the ocean state. We propose here to characterize model errors using Argo observations. Model errors are described through their amplitude, geographical and temporal variations as well as their spatial scales. Spatial scales of both model errors and ocean signals are, in particular, estimated. This allows a comparison of model errors and ocean variability structure. Finally, techniques based on information content are tested in the longer run quantifying the impact of Argo observations in the Mercator Ocean data assimilation systems.