Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.

Cette thèse est consacrée au développement de méthodes formelles pour la vérification de logiciels. Parmi les techniques les plus utilisées dans ce contexte, il y en a deux qui permettent une spécification rigoureuse de toutes les exécutions possibles d'un système et le contrôle des bogues cachés. D'un côté, la correction d'un programme peut être garantie en démontrant l'insatisfiabilité d'une formule modulo une théorie qui axiomatise les types de données impliqués; de l'autre côté, les techniques de model-checking sont utilisées pour certifier que toute exécution possible du système satisfait les propriétés désirées. Les contributions de cette thèse sont les suivantes. Dans un premier temps, nous donnons un résultat de décidabilité pour la satisfiabilité de contraintes pour des extensions intéressantes de la théories des tableaux. Ensuite, nous avons obtenu des résultats dans le prolongement de Manna et Pnueli qui ont montré qu'un mélange de la logique du premier ordre et de la logique temporelle linéaire suffit pour énoncer les problèmes de vérification pour la classe des systèmes réactifs. Ainsi, nous nous inspirons de la récente littérature sur la combinaison des procédures de décision pour établir des résultats de décidabilité et d'indécidabilité pour le problème de satisfiabilité pour des logiques permettant d'intégrer du raisonnement modulo des théories du premier ordre dans un cadre temporel. Les résultats qu'on obtient pour la logiques temporelle linéaire sont ensuite généralisés au cas où le flux temporel est décrit par une logique dont le problème de la satisfiabilité relativisée est décidable. Notre dernière contribution est la décidabilité du problème du model-checking pour le flux temporel linéaire, sous des hypothèses appropriées concernant les théories du premier ordre impliquées. La preuve de ce résultat indique qu'on pourrait employer avec succès des Solveurs Modulo des Théories dans les applications du model-checking aux systèmes ayant un nombre infini d'états. / The thesis is devoted to the development of formal methods for software verification. Indeed, two are among the most widespread techniques that allow to rigorously specify the possible executions of a system and check whether it contains bugs. On the one hand, correctness of a program can be guaranteed by showing the unsatisfiability of a formula modulo a theory which usually axiomatizes the involved datatypes; on the other hand, model checking techniques are used to certify that every possible run of the system satisfies the desired properties. The contributions of the thesis are the following: First of all, we give decidability result for the constraint satisfiability problem for interesting extensions of the theory of arrays. Secondly, along the lines of Manna and Pnueli, who have shown how a mixture of first-order logic and linear time temporal logic is sufficient to state verification problems for the class of reactive systems, we draw on the recent literature about combination of decision procedures to give decidability and undecidability results for the satisfiability problem for logics that allow to plug reasoning modulo first-order theories into a temporal setting. The results obtained in the case of linear flows of time are then generalized to temporal and modal logics whose relativized satisfiability problem is decidable. The last contribution is the decidability of the model checking problem for linear flows of time under suitable hypothesis over the first-order theories involved. The proofs of the decidability results suggest that efficient Satisfiability Modulo Theories solvers might be successfully employed in the model checking of infinite-state systems.

Le résumé en français n'a pas été communiqué par l'auteur. / The combination of several socio-economic data bases originating from different administrative sources collected on several different partitions of a geographic zone of interest into administrative units induces the so called areal interpolation problem. This problem is that of allocating the data from a set of source spatial units to a set of target spatial units. At the European level for example, the EU directive ’INSPIRE’, or INfrastructure for Spatial InfoRmation, encourages the states to provide socio-economic data on a common grid to facilitate economic studies across states. In the literature, there are three main types of such techniques: proportional weighting schemes, smoothing techniques and regression based interpolation. We propose a theoretical evaluation of these statistical techniques for the case of count related data. We find extensions of some of these methods to new cases : for example, we extend the ordinary dasymetric weightingmethod to the case of an intensive target variable Y and an extensive auxiliary quantitative variable X and we introduce a scaled version of the Poisson regression method which satisfies the pycnophylactic property. We present an empirical study on an American database as well as an R-package for implementing these methods.

L'objectif de cette thèse est d'adapter des méthodes récentes de statistique pour apporter une vision nouvelle de la transition nutritionnelle au Vietnam. Chapitre 1, nous faisons une brève introduction. Nous considérons que le Vietnam est une étude pilote sur le problème de la nutrition. Chapitre 2, nous revenons sur la question de l'estimation de la relation entre la prise de calories par personne et le revenu en utilisant six vagues de l'enquête VHLSS Survey sur la période 2004-2014. Nous adoptons plutôt la famille des modèles généralisés additifs (GAM) dans lesquels seul le revenu intervient de façon non linéaire. Nous comparons ces modèles avec une procédure récente. Les résultats mettent en relief une réponse forte de la prise de calories à un accroissement du revenu pour les foyers les plus pauvres. Chapitre 3, nous utilisons des méthodes de décomposition pour évaluer les déterminants des changements de consommation de macronutriments au Vietnam en utilisant les vagues 2004 et 2014. La méthode de décomposition récente proposée par Rothe (2015) a pour but de poursuivre la décomposition plus loin en décomposant l'effet de composition en trois composantes: la contribution directe de chaque covariable, plusieurs effets d'interaction d'ordre deux ou supérieur et un effet de la dépendance. Rothe utilise des copules pour modéliser les effets de dépendance. Chapitre 4, nous nous concentrons sur la composition de la diète en modélisant les proportions de protéines, de matières grasses et de glucides dans la prise moyenne de calories par personne. Nous utilisons des outils descriptifs pour montrer l'évolution des trois composantes au travers du temps et modélisons ensuite la consommation de macronutriments en fonction des caractéristiques des ménages avec des modèles de régression pour données de composition. Nous établissons la formule permettant le calcul des semi-elasticités de la consommation de macronutriments par rapport à la dépense totale de nourriture. Chapitre 5, nous nous penchons sur la relation entre les parts de macronutriments et l'indice de masse corporelle (IMC). Nous construisons un modèle de régression compositionnelle incluant un total pour expliquer les quantiles de l'indice de masse corporelle. Nous calculons ensuite les élasticités de l'IMC par rapport à chaque macronutriment. Notre travail est basé sur l'utilisation de la base de données de l'enquête GNS 2009-2010. Les résultats révèlent d'abord des effets significatifs de facteurs socio-économiques. / The objective of this thesis is to adapt recent statistical techniques and to bring new insights on the nutritional transition in Vietnam. Vietnam is a lower middle income country but it now faces the double burden of malnutrition characterized by the coexistence of undernutrition along with overweight and obesity, or diet-related noncommunicable diseases. Chapter 1 gives a brief introduction to this thesis. We consider Vietnam is a pilot case study about nutrition. Chapter 2, we revisit the issue of estimating the relationship between per capita calorie intake and income using six waves of the Vietnam Household Living Standard Survey over the period 2004-2014. Characterizing the response of calorie intake to income for the poorest households is a prerequisite for considering policies aimed at reducing starvation and correcting nutritional deficiencies. The classical log-log specification does not capture the nonlinearity of this relationship. We adopt rather various generalized additive models (GAM) specifications where only income is supposed to act in a nonlinear fashion and compare them with a recent procedure. The results highlight the strong response of calorie intake to an increase in income for the poorest households. A byproduct of the proposed methodology is the decomposition of the evolution of average calorie intake between the two waves into the part due to the change of population characteristics distributions and those coming from the change in calorie-income relationship, shedding new light on the nutritional transition in Vietnam. Chapter 3, we use decomposition methods to assess the determinants of changes in macronutrients consumption in Vietnam using the 2004 and 2014 waves. The common objective of decomposition methods is to decompose between-group differences in economic outcomes such as wage or income, into two components: a composition effect due to differences in observable covariates across groups, and a structure effect due to differences in the relationship that links the covariates to the considered outcome. The recent decomposition procedure proposed by Rothe (2015) aims at decomposing further the composition effect into three types of components: the direct contribution of each covariate, several two way and higher order interaction effects and a dependence. Rothe (2015) uses a parametric copula to model the dependence effects and we adapt this approach to the case of a mixture of continuous and discrete covariates. Chapter 4, we focus on food composition in terms of diet components. We consider modeling the proportions of protein, fat and carbohydrate in the average per capita calorie intake. We use descriptive tools, such as compositional biplots and ternary diagrams, to show the evolution of the three components over the years and then model macronutrients composition as a function of household characteristics, using compositional regression models. We derive the expression of the semi-elasticities of macronutrients shares with respect to food expenditure. We then compare the interpretations of these shares semi-elasticities to that of volumes of macronutrients and of total calorie intake obtained using classical linear models. Chapter 5, we focus on the relationship between macronutrient balances and body mass index. We develop a compositional regression model including a total at various quantile orders. We then compute the elasticities of BMI with respect to each macronutrient and to the total consumption. Our empirical research is based on the General Nutrition Survey 2009-2010. The results first reveal significant impacts of some socio--economics factors. All elasticities of BMI with respect to each macronutrient increase as BMI increases until a threshold (BMI=20) and then remain stable. Chapter 6, we briefly give our perspectives of future research in both mathematics and nutrition.

L'objectif de l'optimisation de forme d'une pompe générique de fond de puits est de maximiser le gain de pression par unité de longueur de la pompe, en redessinant ses aubes et son moyeu, tout en respectant un certain nombre de contraintes géométriques. On génère la représentation de la géométrie 3D de la pompe grâce à des B-splines paramétriques cubiques 2D. Pour l'optimisation on utilise une méthode de gradient classique. On emploie Fluent, un logiciel de modélisation de mécanique des fluides "boîte noire" et on procède par conséquent à un calcul de gradient incomplet de la fonction coût. Pour cela on écrit l'expression analytique exacte du gradient à l'aide d'une formule d'intégration sur les bords variables puis on ne prend en compte que les termes que l'on peut calculer ou déterminer numériquement. Les termes généralement écartés sont les dérivées des solutions de l'équation d'état par rapport au déplacement d'un point de contrôle. On a d'abord développé un code d'optimisation pour le moyeu de la pompe seul, sans aubages, et on présente les résultats obtenus. On utilise une méthode d'optimisation sans contrainte et on prend en compte par réduction du problème des contraintes d'égalité linéaires. On constate qu'après une première phase de décroissance, la fonction coût ne converge pas vers un minimum. On propose alors quelques tests de façon à analyser ce résultat. Parmi ceux-là, l'emploi des différences finies confirme que le gradient incomplet n'est pas systématiquement une direction de descente. Enfin quelques pistes sont évoquées pour l'expliquer. / The aim of the optimization of a well-pump is to maximize the pressure gain per length unit in the pump by designing its blades and hub, while taking into account some geometrical constraints. The 3D representation of the geometry of the pump is generated thanks to 2D parametric and cubic B-splines. We lead the optimization with a classical gradient method. Fluent, a computational fluid dynamics (CFD) "black box" software, is used and therefore we chose to compute an incomplete gradient of the cost function. We calculate the exact analytical expression of the gradient thanks to an integration formula on variable boundaries. Only the terms we can calculate or compute numerically are then kept. The terms we generally omit are the derivatives of the solutions of the state equations with respect to the displacement of the control points. An optimization program for the single hub of the pump has first been developed and we present its results. We use an optimization method without constraints though linear equality constraints are taken into account by reducing the problem. After a first decreasing phase, the cost function does not converge to a minimum value. We suggest some tests so as to analyze this result. Among these, the use of finite differences confirms that the incomplete gradient is not systematically a descent direction. Some ideas are finally given in order to explain this phenomenon.

Entre plusieurs conditions biologiques, le comportement d’un gène peut être affecté soit dans son niveau d’expression moyen, soit dans sa relation aux autres, caractérisée par les covariances entre gènes. Ces deux questions sont généralement traitées de manière indépendante en statistique, bien qu’elles soient clairement liées. Afin de palier à ces limitations, cette thèse vise à proposer une modélisation unifiée de ces deux questions pour identifier les gènes clés affectés dans leur moyenne et/ou dans leurs interactions. Le modèle principal est le modèle graphique gaussien avec des pénalisations sur les paramètres de la moyenne et de la matrice de précision. / When comparing different biological conditions, the expression of a gene might shift. It can be a change in terms of its average expression level characterized by its mean. Or it can be a change in terms of its interactions with other genes characterized by the covariance matrix. These two types of events are usually analysed independently even though they are clearly related. In order to alleviate these limitations, we propose in this thesis a unified strategy to address these two questions and identify key genes affected either in terms of their mean or their interactions with other genes. The main statistical model is the Gaussian graphical model with penalization on the mean and precision matrix parameters.

Cette thèse s’intéresse à la description symbolique d’arborescences vasculaires issues d’images 3D multimodales. Ce travail vise à fournir un cadre méthodologique global pour l’analyse de telles structures et plus particulièrement pour l’arbre vasculaire cérébral. Le domaine d’application clinique visé est la neurochirurgie, notamment pour la planification du geste du praticien. Notre principale contribution est le développement d’une méthode de squelettisation 3D, adaptée aux formes tubulaires et judicieuse pour la description symbolique. Nous proposons de baser la méthode de squelettisation sur la construction de l’arbre de des plus courts chemins de Dijkstra. Ainsi, nous extrayons la branche principale qui correspond à la branche la plus longue de l’arbre de Dijkstra, puis, nous détectons de manière itérative chaque branche annexe en conservant les branches de l’arbre de longueur supérieure à un seuil fixé. Puisque notre squelettisation se réalise de manière itérative, nous possédons les informations locales à chacune des branches. De cette manière, la description symbolique est facilitée et consiste alors en un partitionnement du squelette permettant la collecte de ces informations. Les algorithmes ont été implémentés sous la plateforme logicielle du laboratoire, ArtiMed, et évalués sur données simulées et cliniques. L’évaluation des méthodes de squelettisation et de description symbolique a fait l’objet de l’élaboration d’un plan d’expérience spécifique consistant en une comparaison des résultats sur une série de 18 rotations du volume initial. / This thesis describes the methodology and the evaluation of a symbolic description method applied on vascular trees from multimodal 3D images. This work aims to supply a global methodological framework for the analysis of such structures and, more particularly, for the cerebral vascular tree. The clinical application field is neurosurgery and particularly neurosurgery planning. Our method is based on the application of the minimum cost-spanning tree using Dijkstra’s algorithm and seems well appropriate to tubular objects. We skeletonize the structure in two stages: first, we extract the main branch which corresponds to the longest branch of the Dijkstra’s tree, then, we detect iteratively every secondary branch by keeping the branches of the tree which length is superior to a fixed threshold. Since our skeletonization works in an iterative way, we possess local information for each branch. In this way, the symbolic description is facilitated and consists in a partitioning of the skeleton to collect the descriptive characteristics. Algorithms were implemented on the laboratory software platform (ArtiMED) developed in Borland C++ and estimated on digital and clinical data. The evaluation scheme adopts a specific experiment approach consisting in a comparison of the results of a series of 18 rotations of the initial volume.

L'objectif de ce travail est le développement d'une méthode numérique pour simuler la diffusion de défauts cristallographiques mobiles dans les métaux irradiés, ainsi que leur absorption par les puits, afin de mieux anticiper l'évolution microstructurale de ces matériaux. Un intérêt particulier a été porté au cas de l’interaction entre les défauts ponctuels et les dislocations.Les méthodes de champ de phases sont bien adaptées à ce problème, puisqu’elles peuvent tenir compte des effets élastiques des dislocations sur la diffusion de ces défauts dans les cas les plus complexes. Le modèle de champ de phases présenté dans ce travail a été adapté pour prendre en compte la création des défauts par irradiation ainsi que leur absorption par les cœurs de dislocation à l’aide d’un nouveau paramètre d’ordre associé à la morphologie du puits. La méthode a d’abord été validée dans différents cas de référence en comparant les forces de puits obtenues numériquement aux solutions analytiques disponibles dans la littérature.Elle a ensuite été appliquée aux dislocations dans le zirconium en faisant varier leur orientation, et en tenant compte des propriétés anisotropes du cristal et des défauts ponctuels, obtenus récemment par des calculs à l'échelle atomique.L'analyse des résultats démontre que l'anisotropie de forme des défauts ponctuels favorise l'absorption des lacunes par les boucles basales, ce qui est cohérent avec la croissance du zirconium sous irradiation expérimentalement observée.Enfin, l'étude rigoureuse des boucles de dislocation révèle que les simulations par champ de phases sont plus précises que les solutions analytiques dans des domaines de densités réalistes. / The aim of this work is to develop a modelling technique for diffusion of crystallographic migrating defects in irradiated metals and absorption by sinks to better predict the microstructural evolution in those materials.The phase field technique is well suited for this problem, since it naturally takes into account the elastic effects of dislocations on point defect diffusion in the most complex cases. The phase field model presented in this work has been adapted to simulate the generation of defects by irradiation and their absorption by the dislocation cores by means of a new order parameter associated to the sink morphology. The method has first been validated in different reference cases by comparing the sink strengths obtained numerically with analytical solutions available in the literature. Then, the method has been applied to dislocations with different orientations in zirconium, taking into account the anisotropic properties of the crystal and point defects, obtained by state-of-the-art atomic calculations.The results show that the shape anisotropy of the point defects promotes the vacancy absorption by basal loops, which is consistent with the experimentally observed zirconium growth under irradiation. Finally, the rigorous investigation of the dislocation loop case proves that phase field simulations give more accurate results than analytical solutions in realistic loop density ranges.

Les méthodes d'identification dites sous-espace sont largement utilisées pour la caractérisation des modes propres et la surveillance des structures mécaniques. Elles ont fait leurs preuves pour les systèmes dont la dynamique est invariante dans le temps. Elles ne sont, toutefois, pas adaptées à des systèmes à rotors comme les hélicoptères et les éoliennes qui, de part leurs parties tournantes, sont périodiques dans le temps. Le but de cette thèse est d'étendre le champ d'application de ces méthodes à cette classe particulière de systèmes. Tout d'abord, un algorithme qui permet d'identifier certaine structure modale, dite de Floquet, est proposée. Ensuite, une étude de sensibilité est réalisée dans le but de quantifier les incertitudes, liées aux bruits ou à d'autres facteurs, sur les paramètres modaux identifiés. Enfin et partant de l'algorithme d'identification, une méthode de détection d'instabilité est développée. Cette méthode est basée sur la définition d'un résidu, fonction des paramètres modaux, et la surveillance d'un changement éventuel de ce résidu qui correspond à une déviation vers un régime instable. Ces méthodes ont été appliquées à des modèles numériques et à des données expérimentales. / Subspace identification methods are widely used for caracterizing modal param-eters and for vibration monitoring of mechanical structures. They were shown powerful for the so-called linear time-invariant systems. However, they are not adapted to rotating sys-tems such as helicopters and wind turbines, which are inherently time-periodic systems. The goal of this thesis is to extend the applicability of these methods to this particular class of systems. First, a new identification algorithm is suggested. This algorithm permits to iden-tify the so-called Floquet modal structure. Then, a sensitivity study is conducted in order to quantify uncertainties, related to noises and other sources, about the identified modal param-eters. Finally and based on the suggested identification algorithm, a method for instability detection is developed. The main feature of this method is to define some residual, which is function of modal parameters, then to detect an eventual change over it which means a possible deviation toward an unstable regime. The suggested methods were applied to both numerical and experimental data.

Les stators de turboalternateurs sont sujets à des défauts de type court-circuit entre tôles. Ces défauts induisent des points chauds pouvant impacter les performances de la machine, voir entraîner son endommagement irréversible. Dans ce travail, ces courts-circuits, ainsi que les tests utilisés pour en faire le diagnostic, ont été étudiés à l’aide d’une approche par éléments finis 3D en électromagnétisme. L’une des difficultés inhérentes à la modélisation numérique de courts-circuits entre tôles réside dans les facteurs d’échelle mis en jeu (stator, courts-circuits et vernis isolants entre tôles). Une modélisation par éléments finis brute de la géométrie réelle (empilement des tôles, représentation de l’isolant, …) impliquerait un nombre d’inconnues beaucoup trop élevé par rapport aux puissances de calcul disponibles classiquement. Ainsi, des méthodes d’homogénéisation, associées à une méthodologie de choix des zones à homogénéiser, ont été utilisées pour représenter les paquets de tôles. L’approche a été validée à partir de résultats issus d’une maquette d’étude expérimentale, notamment en considérant des défauts sous différentes conditions (position, taille, …). Les deux principaux tests de diagnostic utilisés dans l’industrie ont également été modélisés en présence de ces défauts : le test El Cid, à flux faible, et le test à 80% du flux nominal avec détection thermique. L’étude réalisée montre l’importance de certains paramètres, tels que l’étendue du défaut et les caractéristiques des matériaux, sur les signaux issus des tests. Ceci apparaît notamment au travers de la sensibilité des tests de diagnostic dans ces différentes conditions. / Turbogenerator stators are subject to faults such as interlaminar short circuits. These faults induce hot spots which may have an impact on the machine performances, leading in certain cases to irreversible damages. In this work, the short circuits, as well as the most commonly used diagnosis tests, have been studied using a 3D finite element method electromagnetic approach. One of the difficulties inherent in numerical modelling of interlaminar short circuits is to take account of the scale factor between the different parts that are involved in such problem (dimensions of the stator, short circuits and insulating varnish between laminations). A simple finite element modelling of the real geometry (lamination stack, insulation representation…) would imply a much too large number of unknowns regarding the calculation power which is classically available. Thus, in this work, to represent lamination stacks, homogenization techniques have been associated to a methodology to choose the homogenized and non-homogenized (including the fault) zones. The approach has been validated through results from an experimental prototype considering faults under different conditions (position, size…). Moreover, both main diagnosis tests, used in the industry to detect such faults, have also been modelled in the presence of a fault: the El Cid test, at low flux, and the test at 80% of the rated flux with thermal detection. The study which has been carried out shows the importance of certain parameters, such as the fault size and the material characteristics, on the diagnosis test results. This appears in particular through the diagnosis tests sensibility in these different conditions.