L’optimisation des structures est un processus essentiel dans la conception des systèmes mécaniques et électroniques. Cette thèse s’intéresse à la résolution des problèmes mono-objectifs et multi-objectifs des structures mécaniques et mécatroniques. En effet, les industriels ne sont pas seulement préoccupés à améliorer les performances mécaniques des pièces qu’ils conçoivent, mais ils cherchent aussi à optimiser leurs poids, leurs tailles, ainsi que leurs coûts de production. Pour résoudre ce type de problème, nous avons fait appel à des métaheuristiques robustes qui nous permettent de minimiser le coût de production de la structure mécanique et de maximiser le cycle de vie de la structure. Alors que des méthodes inappropriées de l’évolution sont plus difficiles à appliquer à des modèles mécaniques complexes en raison de temps calcul exponentiel. Il est connu que les algorithmes génétiques sont très efficaces pour les problèmes NP-difficiles, mais ils sont très lourds et trop gourmands quant au temps de calcul, d’où l’idée d’hybridation de notre algorithme génétique par l’algorithme d’optimisation par essaim de particules (PSO) qui est plus rapide par rapport à l’algorithme génétique (GA). Dans notre expérimentation, nous avons obtenu une amélioration de la fonction objectif et aussi une grande amélioration de la minimisation de temps de calcul. Cependant, notre hybridation est une idée originale, car elle est différente des travaux existants. Concernant l’avantage de l’hybridation, il s’agit généralement de trois méthodes : l’hybridation en série, l’hybridation en parallèle et l’hybridation par insertion. Nous avons opté pour l’hybridation par insertion par ce qu’elle est nouvelle et efficace. En effet, les algorithmes génétiques se composent de trois étapes principales : la sélection, le croisement et la mutation. Dans notre cas, nous remplaçons les opérateurs de mutation par l’optimisation par essaim de particules. Le but de cette hybridation est de réduire le temps de calcul ainsi que l’amélioration la solution optimale. / This thesis focuses on solving single objective problems and multiobjective of mechanical and mechatronic structures. The optimization of structures is an essential process in the design of mechanical and electronic systems. Industry are not only concerned to improve the mechanical performance of the parts they design, but they also seek to optimize their weight, size and cost of production. In order to solve this problem we have used Meta heuristic algorithms robust, allowing us to minimize the cost of production of the mechanical structure and maximize the life cycle of the structure. While inappropriate methods of evolution are more difficult to apply to complex mechanical models because of exponential calculation time. It is known that genetic algorithms are very effective for NP-hard problems, but their disadvantage is the time consumption. As they are very heavy and too greedy in the sense of time, hence the idea of hybridization of our genetic algorithm optimization by particle swarm algorithm (PSO), which is faster compared to the genetic algorithm (GA). In our experience, it was noted that we have obtained an improvement of the objective function and also a great improvement for minimizing computation time. However, our hybridization is an original idea, because it is a different and new way of existing work, we explain the advantage of hybridization and are generally three methods : hybridization in series, parallel hybridization or hybridization by insertion. We opted for the insertion hybridization it is new and effective. Indeed, genetic algorithms are three main parts : the selection, crossover and mutation. In our case,we replace the operators of these mutations by particle swarm optimization. The purpose of this hybridization is to reduce the computation time and improve the optimum solution.

Nous présentons dans cette thèse les définitions et notations liées aux systèmes de fermeture et montrons leur relation avec les théories de Horn. Nous nous intéressons ensuite à trois opérations sur les systèmes de fermeture : la borne supérieure, la borne inférieure et la différence. Nous proposons une caractérisation de ces différentes opérations selon la représentation des systèmes de fermeture que nous considérons. On s'intéresse ensuite au problème de génération d'une base d'implications mixtes d'un contexte formel. Nous étudions ce problème lorsque la donnée prise en considération est constituée des bases d'implications génériques positives et négatives de ce contexte. Trois résultats majeurs sont présentés : l'apport de propriétés et de règles d'inférence pour déduire des implications mixtes, l'impossibilité de générer une base d'implications mixtes juste et complète à partir de ces données dans le cas général, et la faisabilité dans le cas où le contexte est considéré réduit.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Cette thèse aborde deux problèmes relatifs à l’analyse et au traitement des données biologiques à haut débit: le premier touche l’analyse bioinformatique des génomes à grande échelle, le deuxième est consacré au développement d’algorithmes pour le problème de la recherche d’un classement consensus de plusieurs classements.L’épissage des ARN est un processus cellulaire qui modifie un ARN pré-messager en en supprimant les introns et en raboutant les exons. L’hétérodimère U2AF a été très étudié pour son rôle dans processus d’épissage lorsqu’il se fixe sur des sites d’épissage fonctionnels. Cependant beaucoup de problèmes critiques restent en suspens, notamment l’impact fonctionnel des mutations de ces sites associées à des cancers. Par une analyse des interactions U2AF-ARN à l’échelle génomique, nous avons déterminé qu’U2AF a la capacité de reconnaître environ 88% des sites d’épissage fonctionnels dans le génome humain. Cependant on trouve de très nombreux autres sites de fixation d’U2AF dans le génome. Nos analyses suggèrent que certains de ces sites sont impliqués dans un processus de régulation de l’épissage alternatif. En utilisant une approche d’apprentissage automatique, nous avons développé une méthode de prédiction des sites de fixation d’UA2F, dont les résultats sont en accord avec notre modèle de régulation. Ces résultats permettent de mieux comprendre la fonction d’U2AF et les mécanismes de régulation dans lesquels elle intervient.Le classement des données biologiques est une nécessité cruciale. Nous nous sommes intéressés au problème du calcul d’un classement consensus de plusieurs classements de données, dans lesquels des égalités (ex-aequo) peuvent être présentes. Plus précisément, il s’agit de trouver un classement dont la somme des distances aux classements donnés en entrée est minimale. La mesure de distance utilisée le plus fréquemment pour ce problème est la distance de Kendall-tau généralisée. Or, il a été montré que, pour cette distance, le problème du consensus est NP-difficile dès lors qu’il y a plus de quatre classements en entrée. Nous proposons pour le résoudre une heuristique qui est une nouvelle variante d’algorithme à pivot. Cette heuristique, appelée Consistent-pivot, s’avère à la fois plus précise et plus rapide que les algorithmes à pivot qui avaient été proposés auparavant. / It is thought to be more and more important to solve biological questions using Bioinformatics approaches in the post-genomic era. This thesis focuses on two problems related to high troughput data: bioinformatics analysis at a large scale, and development of algorithms of consensus ranking. In molecular biology and genetics, RNA splicing is a modification of the nascent pre-messenger RNA (pre-mRNA) transcript in which introns are removed and exons are joined. The U2AF heterodimer has been well studied for its role in defining functional 3’ splice sites in pre-mRNA splicing, but multiple critical problems are still outstanding, including the functional impact of their cancer-associated mutations. Through genome-wide analysis of U2AF-RNA interactions, we report that U2AF has the capacity to define ~88% of functional 3’ splice sites in the human genome. Numerous U2AF binding events also occur in other genomic locations, and metagene and minigene analysis suggests that upstream intronic binding events interfere with the immediate downstream 3’ splice site associated with either the alternative exon to cause exon skipping or competing constitutive exon to induce inclusion of the alternative exon. We further build up a U2AF65 scoring scheme for predicting its target sites based on the high throughput sequencing data using a Maximum Entropy machine learning method, and the scores on the up and down regulated cases are consistent with our regulation model. These findings reveal the genomic function and regulatory mechanism of U2AF, which facilitates us understanding those associated diseases.Ranking biological data is a crucial need. Instead of developing new ranking methods, Cohen-Boulakia and her colleagues proposed to generate a consensus ranking to highlight the common points of a set of rankings while minimizing their disagreements to combat the noise and error for biological data. However, it is a NP-hard questioneven for only four rankings based on the Kendall-tau distance. In this thesis, we propose a new variant of pivot algorithms named as Consistent-Pivot. It uses a new strategy of pivot selection and other elements assignment, which performs better both on computation time and accuracy than previous pivot algorithms.

Le protocole Pastry réalise une table de hachage distribué sur un réseau pair à pair organisé en un anneau virtuel de noeuds. Alors qu'il existe plusieurs implémentations de Pastry, il n'y a pas encore eu de travaux pour décrire formellement l'algorithme ou vérifier son bon fonctionnement. Intégrant des structures de données complexes et de la communication asynchrone entre des noeuds qui peuvent rejoindre ou quitter le réseau, ce protocole représente un intérêt certain pour la vérification formelle. La thèse se focalise sur le protocole Join de Pastry qui permet à un noeud de rejoindre le réseau. Les noeuds ayant intégré le réseau doivent avoir une vue du voisinage cohérente entre eux. La propriété principale de correction, appelée CorrectDelivery, assure qu'à tout moment il y a au plus un noeud capable de répondre à une requête pour une clé, et que ce noeud est le noeud le plus proche numériquement à ladite clé. Il n'est pas trivial de maintenir cette propriété en présence de churn. Ce travail nous a permis de découvrir des violations inattendues de la propriété dans les versions publiées de l'algorithme. Sur la base de cette analyse, le protocole IdealPastry est conçu et vérifié en utilisant l'assistant interactif à la preuve TLAPS pour TLA+. Le protocole LuPastry est obtenu en assouplissant certaines hypothèses de IdealPastry. Il est montré formellement que LuPastry vérifie CorrectDelivery sous l'hypothèse qu'aucun noeud ne quitte le réseau. Cette hypothèse ne peut être relâchée à cause du risque de perte de connexion du réseau dans le cas où plusieurs noeuds quittent le réseau en même temps / Pastry is a structured P2P algorithm realizing a Distributed Hash Table over an underlying virtual ring of nodes. Several implementations of Pastry are available, but no attempt has so far been made to formally describe the algorithm or to verify its properties. Since Pastry combines complex data structures, asynchronous communication, and concurrency in the presence of spontaneous join and departure of nodes, it makes an interesting target for verification. This thesis focuses on the Join protocol of Pastry that integrates new nodes into the ring. All member nodes must have a consistent key mapping among each other. The main correctness property, named CorrectDelivery, states that there is always at most one node that can deliver an answer to a lookup request for a key and this node is the numerically closest member node to that key. This property is non-trivial to preserve in the presence of churn. In this thesis, unexpected violations of CorrectDelivery in the published versions of Pastry are discovered and analyzed using the TLA+ model checker TLC. Based on the analysis, the protocol IdealPastry is designed and verified using the interactive theorem prover TLAPS for TLA+. By relaxing certain hypotheses, IdealPastry is further improved to LuPastry, which is again formally proved correct under the assumption that no nodes leave the network. This hypothesis cannot be relaxed in general due to possible network separation when particular nodes simultaneously leave the network

Dans cette thèse nous examinons en détail le problème du logarithme discret dans les corps finis. Dans la première partie, nous nous intéressons à la notion de friabilité et à l'algorithme ECM, le plus rapide test de friabilité connu. Nous présentons une amélioration de l'algorithme en analysant les propriétés galoisiennes des polynômes de division. Nous continuons la présentation par une application d'ECM dans la dernière étape du crible algébrique (NFS). Dans la deuxième partie, nous présentons NFS et son algorithme correspondant utilisant les corps de fonctions (FFS). Parmi les améliorations examinées, nous montrons qu'on peut accélérer le calcul de logarithme discret au prix d'un pré-calcul commun pour une plage de premiers ayant le même nombre de bits. Nous nous concentrons ensuite sur la phase de sélection polynomiale de FFS et nous montrons comment comparer des polynômes quelconques à l'aide d'une unique fonction. Nous concluons la deuxième partie avec un algorithme issu des récentes améliorations du calcul de logarithme discret. Le fait marquant est la création d'une procédure de descente qui a un nombre quasi-polynomial de noeuds, chacun exigeant un temps polynomial. Cela a conduit à un algorithme quasi-polynomial pour les corps finis de petite caractéristique / In this thesis we study at length the discrete logarithm problem in finite fields. In the first part, we focus on the notion of smoothness and on ECM, the fastest known smoothness test. We present an improvement to the algorithm by analyzing the Galois properties of the division polynomials. We continue by an application of ECM in the last stage of the number field sieve (NFS). In the second part, we present NFS and its related algorithm on function fields (FFS). We show how to speed up the computation of discrete logarithms in all the prime finite fields of a given bit-size by using a pre-computation. We focus later on the polynomial selection stage of FFS and show how to compare arbitrary polynomials with a unique function. We conclude the second part with an algorithm issued from the recent improvements for discrete logarithm. The key fact was to create a descent procedure which has a quasi-polynomial number of nodes, each requiring a polynomial time. This leads to a quasi-polynomial algorithm for finite fields of small characteristic

Le contexte incertain des marchés actuels a contribué au développement des systèmes manufacturiers, donnant lieu à des systèmes ayant des principes et des fonctionnalités multiples, qui essayent de répondre aux exigences changeantes. Les systèmes manufacturiers reconfigurables (RMS) constituent une classe des systèmes où les machines, les composants des machines ainsi que le système de manutention peuvent être ajoutés, modifiés, supprimés ou échangés selon les besoins de la production. Un RMS combine le haut débit des systèmes manufacturiers dédiés avec la flexibilité des systèmes flexibles. Le principal composant d'un RMS est la machine reconfigurable (RMT) qui possède une structure qui permet sa reconfiguration. Nous consacrons ce travail au problème de génération des plannings de fabrication dans un RMS, en exploitant au mieux les hauts degrés de reconfigurabilité des RMTs pour proposer des plannings efficaces. Trois problèmes liés à la fonction de génération des plannings de fabrication sont considérés : (1) la génération des process plans dans un cas unitaire où nous avons adaptés des techniques d'optimisation multicritère (NSGA-II et AMOSA), (2) la génération des process plans dans le cas multiunité où une optimisation basée sur la simulation a été adaptée, et (3) l'intégration des fonctions de génération des process plans avec l'ordonnancement où nous avons développé une nouvelle heuristique permettant d'effectuer cette intégration Toutes les approches proposées ont été validées par des expériences numériques, démontrant leur applicabilité et efficacité / The uncertain context of current markets has contributed to the development of manufacturing systems, resulting in systems with different features and principles, trying to meet the changing market demands. Reconfigurable manufacturing system (RMS) is a recent class of systems where machines, machine components and the handling system can be added, modified, deleted or exchanged according to the production needs. RMS combines the high throughput of dedicated manufacturing systems with the customizability of flexible systems. The main component of an RMS is the reconfigurable machine (RMT: Reconfigurable Machine Tool) which has a structure that allows reconfiguration. We focus in this work on CAPP (Computer-Aided Process Planning) to generate effective the process plans in an RMS that take advantage of the high degree of RMT reconfigurability Three problems associated with the function process planning are discussed: (1) the generation of process plans for a single-unit case, where we adapted multi-criteria optimization techniques (NSGA-II, AMOSA) (2) the generation of process plans in the multi-unit case, where we developed simulation based optimization technique, and (3) the integration of process planning and scheduling functions, where we developed a new heuristic aiming to achieve this integration. All the proposed approaches have been validated by numerical experiments, demonstrating their applicability and effectiveness

La propension des systèmes informatiques à subir des défaillances matérielles est à l'origine d'une recherche abondante afin de concevoir des systèmes dits tolérants aux pannes. Le procédé couramment retenu consiste à procéder à des réplications, donnant alors naissance à ce que l'on nomme un système distribué. La question se pose alors de savoir si l'on peut garantir que les multiples copies sont cohérentes entre elles. Ainsi, la recherche d'un accord devient-elle un problème à résoudre, à portée paradigmatique : le Consensus. Or, la complexité des algorithmes de Consensus rend la tache ardue : il n'est donc pas rare que l'on commette des erreurs lors de leur conception. De là découle l'idée, développée depuis plus de trente ans, de recourir à des procédés de vérification mécanique des algorithmes et de leurs preuves de correction. Ces procédés prennent place parmi ce que l'on désigne usuellement comme étant des méthodes formelles. C'est à la croisée des recherches en algorithmique distribuée et en méthodes formelles que se situent nos travaux. Plus spécifiquement, il s'agit de faire usage d'un logiciel de certification formelle, Isabelle/HOL, afin de garantir l'exactitude des preuves de correction d'algorithmes de Consensus exprimés dans un cadre formel uniforme du nom de Heard-Of, proposé en 2009 par Charron-Bost et Schiper. Nous montrons que, du fait de leur expression dans un même cadre formel, et du fait de leur proximité, suivant les cas, soit de conception (nombre de rondes, recours à des mécanismes de vote, ...) soit de forme syntaxique, soit d'hypothèses de fonctionnement (synchronisme partiel, ...), ces algorithmes présentent des preuves dont une part conséquente d?arguments sont communs. Cela permet de copier certains d'entre eux d'une preuve à l'autre, afin de réduire l'effort de certification : ces arguments peuvent alors être automatiquement évalués par la machine pour chacun d'entre eux, l'utilisateur n'ayant à intervenir que là où celle-ci est en peine, c'est-à-dire lorsque les différences algorithmiques induisent qu'il faille réviser les détails de l'argumentation. L'exposé que nous faisons de la certification que nous avons effectuée pour six algorithmes distribués dédiés à la résolution du problème du Consensus illustre cette démarche. Par conséquent, nous présentons d'abord les portions communes des démonstrations, puis détaillons ce qui est propre à chacune, l'objectif n'étant pas de permettre une lecture linéaire de chaque démonstration mais de mettre en évidence notre proposition / Computer systems fail. Whatever the reason of these failures, it has been a widespread approach to try and increase the faults-tolerance of a computer system through its replication. The resulting system is said to be a distributed one, in which replicas have to be kept consistent with each others. Hence, reaching agreement, and Consensus in particular, becomes the problem to solve - indeed, the paradigm. Solving Consensus (under various assumptions) is a hard task : algorithms designed on this purpose are subtle and proving their being correct is error-prone - whenever they are, which occasionally appears not to be the case. For more that thirty years, researchers interested in what is called Formal Methods have been working on mechanizing the verification process, in order to increase confidence in the correctness of (distributed) algorithms. The work we present here is at the intersection of distributed algorithms and formal methods. We use the Isabelle/HOL software to certify the correctness proof of various Consensus algorithms expressed in a uniform framework based on the Heard-Of Model, introduced by Charron-Bost and Schiper in 2009. Expressed in a common model, these algorithms, which, depending on the case, share some common mecanisms (number of steps, intermediate votes, ...), some elements of syntax, or types of assumptions (partial synchronism...), can be proved using some common arguments. As a consequence, the certification effort can be reduced by copying some intermediate lemmas from one proof to another and let the computer automatically parse them until some manual adaptation is required. This lead to the idea of certifying the correctness of multiple algorithms all together, instead of proving them one after the other, as one would do on paper in a traditional way. The effort of translation in the formal language of the proof assistant is then possibly reduced. Of course, each proof will also contain specific arguments, which will have to be isolated and translated into the software. Here, we illustrate this proposition through the presentation of formal certificates of correctness for six Consensus algorithms. As a consequence, on should not expect to find here a comprehensive linear presentation of each proof : we first show the arguments shared by multiple proofs, followed by those which are specific to each o them