Dans les domaines critiques d'application de l'informatique, il peut être vital de disposer d'un génie logiciel qui soit capable de garantir le bon fonctionnement des systèmes produits. Dans ce contexte, la méthode B évènementielle promeut le développement de modèles abstraits du système à concevoir et l'utilisation de démonstrations formelles ainsi que de la relation de raffinement entre les modèles. Notre but est de pouvoir travailler sur des systèmes ayant des aspects temporels quantitatifs (propriétés et contraintes de temps) en restant au sein du cadre défini par la méthode B qui a déjà montré son efficacité par ailleurs, mais qui ne dispose pas de concepts spécifiques pour le temps. C'est ainsi que nous proposons l'introduction des contraintes de temps par le raffinement, ceci permet de respecter la philosophie de la méthode B et de systématiser cette approche par la formalisation de patrons de raffinement. Nos différentes modélisations du temps sont proposées sous la forme de patron à réappliquer sur le système à étudier. Nous pouvons donc étudier progressivement le système à partir d'une abstraction non-temporelle afin de le valider progressivement et de distribuer la difficulté de la preuve en plusieurs étapes. L'introduction des aspects temporels ne se fait que lorsque cela est nécessaire lors du processus de développement prouvé. Nous avons validé cette approche sur des études de cas réalistes en utilisant les outils logiciels de démonstration formelle de la méthode B. / Critical application domains of computer science require the use of software engineering methods that ensure that the resulting systems behave according to their intended functionality. In this context, the Event-B method uses an approach based on stepwise refinement, starting with abstract, high-level models of the system under development. The system models corresponding to different levels of abstraction are related by precise and formally proved refinement relations. Our goal is to extend this approach to systems whose requirements include quantitative real-time aspects (properties and temporal constraints). In this way, we benefit from the established qualities of the B method, while extending its scope to real-time aspects that it does not yet cover. More specifically, we propose to introduce time constraints by refinement, respecting the overall approach of the B method, and to systematize our approach by the use of refinement patterns. Different time models are represented by generic patterns that can be reused for the development of concrete systems. In this way we can gradually develop the system from a non-temporal abstraction and progressively validate its correctness, distributing the burden of proof is over several refinement steps. Temporal aspects are introduced step by step and only when necessary. We validated this approach using several real-world case studies, using the software tools for formal proof developed for the Event-B method.

À l’échelle mondiale, la récolte de céréales atteint plusieurs milliards de tonnes chaque année. Les producteurs céréaliers échangent leurs récoltes selon un prix déterminé par la qualité de leur production. Cette évaluation, appelée agréage, est réalisée pour chaque lot sur un échantillon jugé représentatif. La difficulté au cours de cette évaluation est de parvenir à parfaitement caractériser l'échantillon. Il faut pour cela qualifier chacun de ses éléments, en d'autres termes, il est nécessaire d'évaluer chaque grain de céréale de manière individuelle. Cette opération est historiquement réalisée par un opérateur qui isole chaque grain manuellement pour l’inspecter et l'évaluer. Ce procédé est exposé à différents problèmes : d'une part les résultats obtenus par un opérateur ne sont pas parfaitement répétables : son état de fatigue visuelle peut influencer son appréciation ; d'autre part l'évaluation dépend de l'opérateur : elle n'est pas reproductible, les résultats peuvent varier d'un opérateur à l'autre. Cette thèse a donc pour but de mettre au point un système capable de réaliser cette inspection visuelle.Le système d’acquisition est présenté dans un premier temps. Cette enceinte contient les dispositifs d’éclairage et d’acquisition d’images. Différents outils ont été mis en œuvre pour s’assurer de la justesse et de la stabilité des acquisitions. Une méthode d’apprentissage de modèles de forme est ensuite présentée : elle a pour but de définir et de modéliser le type de forme des grains de l’application considérée (blé, riz, orge). Cette étape est réalisée sur une image d’objets isolés. Deux méthodes de détection sont ensuite présentées : une approche déterministe et une approche probabiliste. Ces deux méthodes, mises au point pour segmenter les objets d’une image, utilisent des outils communs bien qu’elles soient conçues différemment. Les résultats obtenus et présentés dans cette thèse démontrent la capacité du système automatique à se positionner comme une solution fiable à la problématique d’inspection visuelle de grains de céréales. / In agriculture, the global grain harvest reached several billion tons each year. Cereal producers exchange their crops at a price determined by the quality of their production. This assessment, called grading, is performed for each set on a representative sample. The difficulty of this assessment is to fully characterize the sample. To do so, it is necessary to qualify each of its elements. In other words, it is necessary to evaluate each individual cereal grain. Historically, this has been performed manually by an operator who isolates each evaluated grain. This method is exposed to various problems: firstly, results obtained by an operator are not perfectly repeatable. For example, eyestrain can influence the assessment. On the other hand the evaluation depends on the operator: it is not reproducible. The results can vary from one operator to another. The aim of this thesis is to develop a system that can handle this visual inspection. In a first time, the acquisition system is introduced. Image acquisition and lighting parts are placed in a cabin. Several methods have been introduced to manage accuracy and stability of the acquisitions. Then, a shape model learning is detailed: this step, based on an image with manually separated objects, defines and modelizes shape of the considered cereal grains (wheat, rice, barley). Two detection approaches are then introduced: a deterministic method and a probabilistic one. Both are based on the same tools to process the objects segmentation of an image, but they deal with the question in a different way. The results provided by the system and presented in this thesis emphasize the ability of this automatic system to process the visual inspection of food products.

L'industrie est le plus grand consommateur d'énergie dans le monde et la majeure partie de sa consommation est électrique. Pour moduler la consommation et équilibrer les périodes creuses et de pic, les producteurs d'électricité dans de nombreux pays pratiquent une tarification différenciée, en anglais "time-of-use (TOU) policy", afin d’encourager les industriels et les particuliers à adapter leur consommation. Cette stratégie incite les gros consommateurs industriels, en particulier le secteur semi-conducteur où la fabrication se fait souvent par lots, à réduire leurs factures d’électricité en adaptant leur production.Dans ce travail, nous étudions plusieurs problèmes d’ordonnancement de production par lots avec tarification différenciée d'électricité. Nous nous intéressons d’abord à l’ordonnancement d’une machine par lots pour minimiser le coût total d’électricité et le makespan. Le deuxième problème étudié généralise le premier en considérant le coût d’électricité pendant les périodes inactives de la machine telles que les périodes de réglage ou d'attente. Enfin, nous traitons l’ordonnancement sur machines parallèles par lots avec des pièces non identiques. Pour chacun de ces problèmes, nous construisons des modèles mathématiques appropriés, et évaluons sa complexité. Pour la résolution, nous proposons plusieurs méthodes de ɛ-contrainte dans lesquelles des sous-problèmes sont transformés en problèmes de sac-à-doc, de sacs-à-doc multiples et ou de bin packing. Nous développons aussi une méthode itérative à deux étapes. Les performances des méthodes développées sont évaluées à l'aide d'un grand nombre d'instances représentatives générées au hasard. Les résultats numériques montrent l'efficacité de ces méthodes par rapport au logiciel commercial CPLEX. / The industrial sector is the largest consumer of the world's total energy and most of its consumption form is electricity. To strengthen the grid's peak load regulation ability, time-of-use (TOU) electricity pricing policy has been implemented in many countries to encourage electricity users to shift their consumption from on-peak periods to off-peak periods. This strategy provides a good opportunity for manufacturers to reduce their energy bills, especially for energy-intensive ones, where batch scheduling is often involved. In this thesis, several bi-objective batch scheduling problems under TOU tariffs are studied. We first investigate a single machine batch scheduling problem under TOU tariffs with the objectives of minimizing total electricity cost and makespan. This primary work is extended by further considering machine on/off switching. Finally, a parallel batch machines scheduling problem under TOU tariffs with non-identical job sizes to minimize total electricity cost and number of enabled machines is studied. For each of the considered problems, appropriate mathematical models are established, their complexities are demonstrated. Different bi-objective resolution methods are developed, including knapsack problem heuristic based ɛ-constraint method, multiple knapsack problem heuristic based ɛ-constraint method, bin packing heuristic based ɛ-constraint method and two-stage heuristic based iterative search algorithm. The performance of the proposed methods is evaluated by randomly generated instances. Extensive numerical results show that the proposed algorithms are more efficient and/or effective for the studied problems than the commercial software CPLEX.

Tableau d'honneur de la Faculté des études supérieures et postdoctorales, 2006-2007 / L'identification du gène responsable d'une maladie peut être facilitée par des méthodes statistiques telles que des études d'association basées sur le déséquilibre de liaison. Différentes stratégies d'analyse sont possibles pour ce type d'étude. Comme pour les tests d'association classiques, un devis d'échantillonnage de cas-témoins peut être utilisé. Un deuxième devis possible est l'échantillonnage de trios. On peut également choisir d'étudier l'association allélique ou haplotypique des marqueurs génétiques sélectionn és. La présente étude vise à comparer par voie de simulation la puissance de tests de déséquilibre de liaison selon la stratégie d'analyse choisie. Dans un premier temps, on s'est intéressé à la comparaison des devis d'échantillonnage cas-témoins et trios ; dans un deuxième temps, on a comparé les approches allélique et haplotypique.

La rivière Chaudière, située au sud de la Ville de Québec, est sujette aux inondations provoquées par la formation d'embâcles. Des inondations ont été enregistrées depuis 1896 jusqu'à ce jour malgré la mise en service, en 1967, d'un ouvrage de contrôle des glaces (ICS) à 3 kilomètres en amont de la Ville de Saint-Georges-de-Beauce afin de réduire les inondations causées par la glace dans le secteur le plus à risque de la rivière Chaudière. Les inondations par embâcles demeurent donc un problème récurrent qui affecte régulièrement 8 villes le long du tronçon de 90 kilomètres en aval de l'ICS. Dans le cadre d'un programme gouvernemental d'aléas d'inondation initié par le ministère des Affaires Municipales et de l'Habitation (MAMH), un mandat pour évaluer les cotes de crues en présence de glace de la rivière Chaudière a été confié à l'Université Laval. La modélisation d'embâcles combinée à des données d'observations historiques d'embâcles est utilisée pour déterminer les niveaux d'inondation par embâcles. L'approche préconisée consiste à contrôler un modèle de simulation hydraulique fluviale, plus spécifiquement le module HEC-RAS, avec un script externe en Python pour générer une distribution Monte-Carlo (MOCA) d'évènements d'embâcles le long du secteur de la rivière à l'étude. Les paramètres mécaniques tels que l'angle de frottement, la porosité et les vitesses de contrainte de cisaillement critiques sont également attribués de manière aléatoire par le script dans une plage délimitée. Les paramètres physiques et hydrologiques attribués à chaque évènement sont choisis au hasard en fonction d'une probabilité estimée à partir des observations historiques, soit le débit calculé à l'ICS, l'emplacement de l'embâcle, la longueur de l'embâcle et les degrés-jours de gel (épaisseur de la glace). Les cotes de crues selon les périodes de retour de 2, 20, 100 et 350 ans sont alors déterminées selon une équation statistique empirique de Gringorten, suivie d'une modulation pour tenir compte des facteurs externes non considérés par MOCA. Ces cotes de crues en présence de glace sont comparées à celles en eau libre telles que déterminées par la méthode classique. Le projet démontre que les niveaux d'eau calculés en présence de glace prédominent ceux en eau libre pour les villes en amont de Saint-Joseph-de-Beauce. La combinaison des niveaux d'eau en présence de glace et en eau libre, réalisée à l'aide de l'équation de la FEMA, montre que la probabilité d'atteindre un seuil spécifique d'élévation diminue la période de retour et en conséquence augmente les probabilités reliées aux inondations. Ce mémoire est le premier travail scientifique qui présente une validation complète de l'approche hydrotechnique utilisant les valeurs in situ de débit, de DJGC et de l'emplacement et de la longueur d'embâcles pour la détermination des cotes de crue par embâcles. Les valeurs de cotes de crues calculées avec la méthode MOCA sont comparées avec les données historiques dans le secteur à l'étude de la rivière Chaudière. La présente étude met en évidence les limitations et les conditions nécessaires pour l'utilisation de cette méthode. Ce projet de recherche montre aussi pour la première fois que l'approche hydrotechnique permet de calculer des courbes fréquentielles de niveaux d'eau en présence de glace qui peuvent être utilisées à des fins réglementaires au Québec. / The Chaudière River, located south of Quebec City, is prone to seasonal ice jam flooding. As early as 1896, ice induced floods have been recorded and in 1967 an ice control structure (ICS) was constructed 3 kilometers upstream of the Town of St. Georges to reduce ice flooding events in the area most at risk of the Chaudière River. Despite the construction of the ICS, flooding caused by ice jams is still an ongoing issue that regularly affects 8 towns along this reach of 90 kilometers downstream of the ICS. As part of a governmental flood hazard program that is managed by the provincial ministère des Affaires Municipales et de l'Habitation (MAMH), the mandate of assessing ice jam flood delineation has been given to Laval University. In order to achieve this objective, ice jam modelling combined with historical data is used to determine ice jam flood levels. More specifically, the approach used is to control a river hydraulic simulation model (HEC-RAS) with an external script (MOCA) written in Python to generate a Monte-Carlo distribution of ice jam flood events along the study reach. The script polls historical data of recorded ice jam events which include flow measured at the ICS, ice jam location, ice jam length, and degree days of freezing (ice thickness). Mechanical parameters such as the angle of friction, porosity and critical shear stress velocities are also randomly assigned by the script within a delimited range. The physical and hydrological parameters assigned to each event are randomly chosen based on the historical data. The flood levels according to the return periods of 2, 20, 100, and 350 years are then determined according to an empirical statistical equation and modulated to consider external factors not considered by the MOCA. These calculated flood levels are compared with the ones obtained by open water floods as determined by the classical method. The results show that the calculated ice induce water levels predominate over open water flooding for the towns upstream of Saint-Joseph-de-Beauce. The combination of ice induced and open water levels, using the FEMA equation, show that the probability of reaching a specific elevation is reduced and thus increases the probability associated with flooding. This thesis is the first scientific work that presents the complete validity of the hydrotechnical approach using in situ flows, cumulative degree-days of freezing and ice jam length and location for the determination for ice induced flood delineation combined with a MOCA framework. Calculated flood frequency levels are compared with historical ice induced flood water levels within the studied reach, as well as the conditions and limitations for using this approach. Also, this scientific document is the first to present ice-related flood levels using the hydrotechnical approach for regulatory purposes in the Province of Québec.

La représentation par réseau est un outil puissant pour la modélisation des systèmes dynamiques complexes. Elle est notamment utilisée en neurosciences pour étudier le cerveau. Cependant, extraire un connectome, soit la liste des neurones et des connexions qui les relient, demeure un défi important pour des cerveaux de plusieurs milliers de neurones. C’est le cas du cerveau de la larve du poisson-zèbre qui contient près d’une centaine de milliers de neurones. Puisque les synapses ne peuvent être directement observées, les connexions entre neurones doivent plutôt être inférées. Plusieurs méthodes classiques, dites d’inférence fonctionnelle, issues des statistiques et de la théorie de l’information, prédisent la connectivité à partir des séries temporelles qui décrivent l’activité des neurones. Plus récemment, des avancées en intelligence artificielle ont ouvert la voie à de nouvelles méthodes d’inférence. L’objectif du projet de maîtrise exposé dans ce mémoire est de comparer la performance des méthodes de l’intelligence artificielle à celle des méthodes bien établies. Puisque la connectivité réelle est nécessaire pour une telle comparaison, un simulateur de réseau de neurones est utilisé pour générer des séries temporelles d’activité à partir de connectivités réelles extraites de vidéos d’activité. Il est montré que la calibration d’un tel simulateur, dans le but d’obtenir de l’activité similaire à celle des poissons-zèbres, n’est pas une tâche triviale. Une approche d’apprentissage profond est donc conçue pour prédire, à partir de métriques d’activité globale, les paramètres de simulation idéaux. Il est ensuite montré, sur 86% des simulations générées, qu’un modèle de réseau de neurones artificiels à convolution performe significativement mieux que les autres méthodes d’inférence. Cependant, lorsqu’un entraînement supervisé est impossible, la méthode classique de transfert d’entropie performe mieux qu’un modèle d’apprentissage profond nonsupervisé sur 78% des simulations générées. / Complex network analysis is a powerful tool for the study of dynamical systems. It is often used in neuroscience to study the brain. However, extraction of complete connectomes, i.e. , the list of all neurons and connections, is still a challenge for large brains. This is the case for the brain of the zebrafish which contains almost a hundred thousand neurons. Since direct observation of synapses is still intractable for a brain of this size, connections between neurons must be inferred from their activity. It is indeed possible to extract time series of activity for all neurons, by making them fluorescent upon activation through genetic engineering and by leveraging the zebrafish’s transparency during the larval stage. Then, so-called methods of functional inference, based on information theory, can be used to predict the connectivity of neurons from time series of their activity. Recent breakthroughs in artificial intelligence have opened the door to new methods of inference. The goal of the project described in this thesis is to compare the performance of such new methods to the performance of well-established ones. Since ground truth of connectivity must be known for comparison, a simulator is used to generate synthetic time series of activity from known connectivity. It is shown that the tuning of such a simulator, in order to generate realistic data, is not an easy task. Therefore, a deep learning approach is proposed to predict optimal simulator parameters by analysis global dynamical metrics. Using the generated time series, it is shown that a convolutional neural network performs significantly better than well-established methods on 86% of simulations. However, in cases where supervised learning is impossible, the zebrafish’s case being an example, the classical method of Transfer Entropy performs better than an unsupervised deep learning model on 78% of simulations.

.

Cette thèse est consacrée à l’enrichissement du modèle mathématique classique des structures intelligentes, en tenant compte des effets thermiques, et à son étude analytique et numérique. Il s'agit typiquement de structures se présentant sous forme de capteurs ou actionneurs, piézoélectriques et/ou magnétostrictifs, dont les propriétés dépendent de la température. On présente d'abord des résultats d'existence et unicité concernant deux problèmes posés sur un domaine tridimensionnel : le problème dynamique et le problème quasi-statique. A partir du problème quasi-statique on déduit un modèle bidimensionnel de plaque grâce à la méthode des développements asymptotiques en considérant quatre types différents de conditions aux limites, chacun visant à modéliser un comportement de type capteur et/ou actionneur. Chacun des quatre problèmes se découple en un problème membranaire et un problème de flexion. Ce dernier est un problème d'évolution qui tient compte d'un effet d'inertie de rotation. On focalise ensuite notre attention sur ce problème et on en présente une étude mathématique et numérique. L'analyse numérique est complétée avec des tests effectués sous l'environnement FreeFEM++. / This thesis is devoted to the enrichment of the usual mathematical model of smart structures, by taking into account thermal effects, and to its mathematical and numerical study. By the expression "smart structures" we refer to structures acting as sensors or actuators, whose properties depend on the temperature. We present at first the results of existence and uniqueness concerning two problems posed on a three-dimensional domain: the dynamic problem and the quasi-static problem. Based on the quasi-static problem, we infer a two-dimensional plate model by means of the asymptotic expansion method by considering four different sets of boundary conditions, each one featuring a sensor-like or an actuator-like behavior. Each of the four problems decouples into a membrane problem and a flexural problem. The latter is an evolution problem that accounts for a rotational inertia effect. Attention is then focused on this problem by presenting a mathematical and numerical study of it. Our numerical analysis is complemented with numerical tests carried out under the FreeFEM++ environment.

Le problème du sac-à-dos à contraintes disjonctives (DCKP) est une variante du sac-à-dos normal. C'est un problème dans lequel certains objets peuvent être incompatibles avec d'autres. Le DCKP apparait, souvent, comme sous problème d'autres problèmes d'optimisation combinatoire plus complexes.

Une approche récente permettant d'étudier les équations issues de la Mécanique des Fluides consiste à considérer les symétries de ces équations. Les succès des développements théoriques, notamment en turbulence, ont justifié la pertinence d'une telle approche. Sur le plan numérique, les méthodes d'intégration construites sur des arguments liés à la structure géométrique des équations s'appellent les intégrateurs géométriques. Dans la première partie de la thèse, on présente la classe d'intégrateurs géométriques probablement la plus connue; ce sont les intégrateurs symplectiques pour les systèmes hamiltoniens. Dans une seconde partie, on introduit les intégrateurs variationnels, construits pour reproduire les lois de conservation des systèmes lagrangiens. Cependant, la plupart des équations de la Mécanique des Fluides ne dérive pas d'un Lagrangien. On expose alors dans la dernière partie une méthode de construction de schémas numériques respectant les symétries d'une équation. Cette méthode est basée sur une formulation moderne des repères mobiles. On présente une contribution au développement de cette méthode; elle permet d'obtenir un schéma invariant possédant un ordre de précision déterminé. Des exemples issus des équations modèles de la Mécanique des Fluides sont traités.