De nombreuses méthodes de traitement du signal reposent sur des résultats puissants d'approximation numérique. Un exemple significatif en est l'utilisation de l'approximation de type Chebyshev pour l'élaboration de filtres numériques.En pratique, le caractère fini des formats numériques utilisés en machine entraîne des difficultés supplémentaires pour la conception de filtres numériques (le traitement audio et le traitement d'images sont deux domaines qui utilisent beaucoup le filtrage). La majorité des outils actuels de conception de filtres ne sont pas optimisés et ne certifient pas non plus la correction de leurs résultats. Notre travail se veut un premier pas vers un changement de cette situation.La première partie de la thèse traite de l'étude et du développement de méthodes relevant de la famille Remez/Parks-McClellan pour la résolution de problèmes d'approximation polynomiale de type Chebyshev, en utilisant l'arithmétique virgule-flottante.Ces approches sont très robustes, tant du point de vue du passage à l'échelle que de la qualité numérique, pour l'élaboration de filtres à réponse impulsionnelle finie (RIF).Cela dit, dans le cas des systèmes embarqués par exemple, le format des coefficients du filtre qu'on utilise en pratique est beaucoup plus petit que les formats virgule flottante standard et d'autres approches deviennent nécessaires.Nous proposons une méthode (quasi-)optimale pour traîter ce cas. Elle s'appuie sur l'algorithme LLL et permet de traiter des problèmes de taille bien supérieure à ceux que peuvent traiter les approches exactes. Le résultat est ensuite utilisé dans une couche logicielle qui permet la synthèse de filtres RIF pour des circuits de type FPGA.Les résultats que nous obtenons en sortie sont efficaces en termes de consommation d'énergie et précis. Nous terminons en présentant une étude en cours sur les algorithmes de type Remez pour l'approximation rationnelle. Ce type d'approches peut être utilisé pour construire des filtres à réponse impulsionnelle infinie (RII) par exemple. Nous examinons les difficultés qui limitent leur utilisation en pratique. / The field of signal processing methods and applications frequentlyrelies on powerful results from numerical approximation. One suchexample, at the core of this thesis, is the use of Chebyshev approximationmethods for designing digital filters.In practice, the finite nature of numerical representations adds an extralayer of difficulty to the design problems we wish to address using digitalfilters (audio and image processing being two domains which rely heavilyon filtering operations). Most of the current mainstream tools for thisjob are neither optimized, nor do they provide certificates of correctness.We wish to change this, with some of the groundwork being laid by thepresent work.The first part of the thesis deals with the study and development ofRemez/Parks-McClellan-type methods for solving weighted polynomialapproximation problems in floating-point arithmetic. They are veryscalable and numerically accurate in addressing finite impulse response(FIR) design problems. However, in embedded and power hungry settings,the format of the filter coefficients uses a small number of bits andother methods are needed. We propose a (quasi-)optimal approach basedon the LLL algorithm which is more tractable than exact approaches.We then proceed to integrate these aforementioned tools in a softwarestack for FIR filter synthesis on FPGA targets. The results obtainedare both resource consumption efficient and possess guaranteed accuracyproperties. In the end, we present an ongoing study on Remez-type algorithmsfor rational approximation problems (which can be used for infinite impulseresponse (IIR) filter design) and the difficulties hindering their robustness.

FundaÃÃo Cearense de Apoio ao Desenvolvimento Cientifico e TecnolÃgico / A noÃÃo de menor ponto-fixo de um operador à amplamente aplicada na ciÃncia da computaÃÃo como, por exemplo, no contexto das linguagens de consulta para bancos de dados relacionais. Algumas extensÃes da LÃgica de Primeira-Ordem (FOL)1 com operadores de ponto-fixo em estruturas finitas, como a lÃgica de menor ponto-fixo (LFP)2, foram propostas para lidar com problemas relacionados à expressividade de FOL. A LFP captura as classes de complexidade PTIME sobre a classe das estruturas finitas ordenadas. A caracterizaÃÃo descritiva de classes computacionais à uma abordagem central em Teoria do Modelos Finitos (FMT)3. O teorema de Trakhtenbrot, considerado o ponto de partida para FMT, estabelece que a validade sobre modelos finitos nÃo à recursivamente enumerÃvel, isto Ã, a completude falha sobre modelos finitos. Este resultado à baseado na hipÃtese de que qualquer sistema dedutivo à de natureza finita. Entretanto, nos podemos relaxar tal hipÃtese como foi feito no escopo da teoria da prova para aritmÃtica. A teoria da prova tem raÃzes no programa de Hilbert. ConseqÃÃncias teÃricas da noÃÃo de prova sÃo, por exemplo, relacionadas a teoremas de normalizaÃÃo, consistÃncia, decidibilidade, e resultados de complexidade. A teoria da prova para aritmÃtica tambÃm à motivada pelos teoremas de incompletude de GÃdel, cujo alvo foi fornecer um exemplo de um princÃpio matemÃtico verdadeiro e significativo que nÃo à derivÃvel na aritmÃtica de primeira-ordem. Um meio de apresentar esta prova à baseado na definiÃÃo de um sistema de prova com uma regra infinitÃria, a w-rule, que estabiliza a consistÃncia da aritmÃtica de primeira-ordem atravÃs de uma perspectiva de teoria da prova. Motivados por esta prova, iremos propor aqui um sistema infinitÃrio de prova para LFP que nos permitirà investigar propriedades em teoria da prova. Com tal sistema dedutivo infinito, pretendemos apresentar uma teoria da prova para uma lÃgica tradicionalmente definida no escopo de FMT. Permanece aberto um caminho alternativo de provar resultados jà obtidos com FMT e tambÃm novos resultados do ponto de vista da teoria da prova. AlÃm disso, iremos propor um procedimento de normalizaÃÃo com restriÃÃes para este sistema dedutivo, que pode ser usado em um provador de teoremas para computar consultas em banco de dados relacionais / The notion of the least fixed-point of an operator is widely applied in computer science as, for instance, in the context of query languages for relational databases. Some extensions of FOL with _xed-point operators on finite structures, as the least fixed-point logic (LFP), were proposed to deal with problem problems related to the expressivity of FOL. LFP captures the complexity class PTIME over the class of _nite ordered structures. The descriptive characterization of computational classes is a central issue within _nite model theory (FMT). Trakhtenbrot's theorem, considered the starting point of FMT, states that validity over finite models is not recursively enumerable, that is, completeness fails over finite models. This result is based on an underlying assumption that any deductive system is of finite nature. However, we can relax such assumption as done in the scope of proof theory for arithmetic. Proof theory has roots in the Hilbert's programme. Proof theoretical consequences are, for instance, related to normalization theorems, consistency, decidability, and complexity results. The proof theory for arithmetic is also motivated by Godel incompleteness theorems. It aims to o_er an example of a true mathematically meaningful principle not derivable in first-order arithmetic. One way of presenting this proof is based on a definition of a proof system with an infinitary rule, the w-rule, that establishes the consistency of first-order arithmetic through a proof-theoretical perspective. Motivated by this proof, here we will propose an in_nitary proof system for LFP that will allow us to investigate proof theoretical properties. With such in_nitary deductive system, we aim to present a proof theory for a logic traditionally defined within the scope of FMT. It opens up an alternative way of proving results already obtained within FMT and also new results through a proof theoretical perspective. Moreover, we will propose a normalization procedure with some restrictions on the rules, such this deductive system can be used in a theorem prover to compute queries on relational databases.

Submitted by Renata Lopes (renatasil82@gmail.com) on 2017-05-26T17:30:30Z No. of bitstreams: 1 ceilimarcolinomoreira.pdf: 628590 bytes, checksum: 89404f2fdb6f6a266713327a91a21c05 (MD5) / Approved for entry into archive by Adriana Oliveira (adriana.oliveira@ufjf.edu.br) on 2017-05-29T19:02:09Z (GMT) No. of bitstreams: 1 ceilimarcolinomoreira.pdf: 628590 bytes, checksum: 89404f2fdb6f6a266713327a91a21c05 (MD5) / Made available in DSpace on 2017-05-29T19:02:09Z (GMT). No. of bitstreams: 1 ceilimarcolinomoreira.pdf: 628590 bytes, checksum: 89404f2fdb6f6a266713327a91a21c05 (MD5) Previous issue date: 2014-03-27 / CAPES - Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / Neste trabalho, apresentamos métodos envolvendo sub e supersolução para estudar a existência de solução, no sentido fraco, para três classes de problemas elípticos de segunda ordem com condição de fronteira de Dirichlet homogênea. Nos dois primeiros casos encontramos solução em W1,2 0 (Ω) e no terceiro caso encontramos solução em L1(Ω) com algumas restrições. / This paper presents methods involving sub and supersolution in order to learn the existence of weak solutions of three classes of second order elliptic problems with homogeneous Dirichlet boundary conditions. In the first two cases we find solution in W1,2 0 (Ω) and in the third case we find solution in L1(Ω) with some restrictions.

La présente thèse est divisée en deux parties. La première partie concerne l'analyse mathématique et la contrôlabilité exacte à zéro pour une catégorie de systèmes structurés décrivant la dynamique d'une population d'insectes. La seconde partie est consacrée à l'étude de la stabilité de la conductivité d'un système de réaction diffusion modélisant l'activité électrique du coeur.Dans le chapitre 2, on considère que la population d'adultes se diffuse dans la vignoble,la fonction de la croissance des individus à chaque stade dépend des variations climatiques et de la variété des raisins. En utilisant la méthode de point fixe, on obtient l'existence et l'unicité des solutions du modèle. On démontre ensuite l'existence d'un attracteur global pour le système dynamique. Enfin, on utilise la théorie des opérateurs compacts et le théorème de point fixe de Krasnoselskii pour prouver l'existence des états stationnaires.Dans le chapitre 3, on traite le problème de contrôlabilité exacte du modèle de Lobesia Botrana, lorsque la fonction de croissance est égale à 1. On suppose que les quatre sous-catégories de ce système sont dans une phase statique. On obtient que la population d'oeufs peut être contrôlée à zéro. Ce résultat est basé sur des estimations à priori combinées avec un théorème de point fixe.Lorsque les papillons adultes se dispersent spatialement, on introduit un contrôle sur la population d'oeufs, de larves et de femelles dans une petite région du vignoble. On montre alors la contrôlabilité exacte à zéro pour les femelles.Dans la deuxième partie de cette thèse, on analyse la stabilité des coefficients de diffusion d'un système parabolique qui modélise l'activité électrique du coeur. On établit une estimation de Carleman pour le système de réaction-diffusion. En combinant cette estimation avec des estimations d'énergie avec poids on obtient le résultat de stabilité. / This thesis is divided into two parts.One is mainly devoted to make a qualitative analysis and exact null controlfor a class of structured population dynamical systems, and the other concernsstability of conductivities in an inverse problem of a reaction-diffusion systemarising in electrocardiology.In the first part, we study the dynamics ofEuropean grape moth, which has caused serious damages on thevineyards in Europe,North Africa, and even some Asian countries.To model this grapevine insect, physiologically structured multistage population systems are proposed.These systemshave nonlocal boundary conditions arising in nonlocal transition processes in ecosystem.We consider the questions of spatial spread of the populationunder physiological age and stage structures,and show global dynamical properties for the model.Furthermore, we investigate the control problem for this Lobesia botrana modelwhen the growth function is equal to $1$.For the case that four subclasses of this system are all in static station,we conclude that the population of eggs can be controlled to zero at acertain moment by acting on eggs.While the adult moths can disperse,we describe a control by a removal of egg and larvapopulation, and also on female moths in a small region of the vineyard.Then the null controllability for female mothsin a nonempty open sub-domain at a given time is obtained.In the second part, a reaction-diffusion system approximating a parabolic-elliptic systemwas proposed tomodel electrical activity in the heart. We are interested inthe stability analysis of an inverse problem for this model.Then we use the method of Carleman estimates and certain weight energyestimatesfor the identification of diffusion coefficients for the parabolicsystem to draw the conclusion.

L'objectif de ce travail de thèse est de développer une bibliothèque de modules IPs (Intellectual Properties) de simulateurs temps réel embarqués qui simulent différents éléments d'un système électrique. Ces modules ont été conçus pour être utiliser non seulement pour une validation HIL (Hardware-In-the-Loop) des commandes numériques mais aussi pour des applications de commande embarquées, où le module IP de simulateur et le contrôleur sont tous les deux implémentés et exécutés dans la même cible FPGA. Cette nouvelle classe de simulateurs temps réel devrait être de plus en plus incluse dans la prochaine génération de contrôleurs numériques. En effet, ces modules IPs de simulateurs temps réel embarqués peuvent être avantageusement intégrés dans les contrôleurs numériques pour assurer des fonctions comme l'observation, l'estimation, le diagnostic où la surveillance de la santé. Inversement aux cas de HIL, le principal défi lors de la conception de tels simulateurs est de faire face à leur complexité ayant à l'esprit que, dans le cas des systèmes embarqués, les ressources matérielles disponibles sont limitées en raison du coût. En outre, ce problème est renforcé par la nécessité des pas de simulation très petit. Ceci est généralement le cas lors de la simulation des convertisseurs de puissance.Pour développer ces modules IPs, des lignes directrices dédiés de conception ont été proposées pour être suivies pour gérer la complexité de ces simulateurs (solveur de modèle, solveur numérique, pas de simulation, conditionnement de données) tout en tenant compte des contraintes temporelles et matérielles/coût (temps de calcul limité, ressources matérielles limitées ...).Les modules IPs de simulateurs à développer ont été organisés en deux catégories principales: ceux qui sont consacrées aux éléments électromagnétiques d'un système électrique, et ceux dédiés à ses éléments commutés.La première catégorie regroupe les éléments où les phénomènes électriques, magnétiques sont modélisés en plus de phénomènes mécaniques (pour les parties mécaniques) et des phénomènes potentiellement thermiques. Trois cas sont traités: le simulateur temps réel embarqué d'une machine synchrone triphasée, celui d'une machine asynchrone triphasée et celui d'un alternateur synchrone à trois étages. En plus de cela, les avantages de l'utilisation de la transformation delta pour améliorer la stabilité du solveur numérique lorsque un petit pas de calcul et le codage virgule fixe (avec une précision de données limitée) sont utilisés, ont été étudiés.La deuxième catégorie concerne des éléments commutés tels que les convertisseurs de puissance où les événements de commutation sont considérés. Là encore, plusieurs topologies de convertisseurs ont été étudiées: un redresseur simple alternance, un hacheur série, un hacheur réversible en courant, un hacheur quatre quadrant, un onduleur monophasé, un onduleur triphasé, un redresseur à diodes triphasé et un redresseur MLI triphasé. Pour tous ces modules IPs de simulateurs, l'approche de modélisation ADC (Associated Discrete Circuit) est adoptée.Le module IP de simulateur temps réel embarqué du redresseur MLI a été appliqué dans un contexte d'une application embarquée. Cette dernière consiste en une commande tolérante aux défauts d'un convertisseur de tension coté réseau. Ainsi, ce module IP est associé à celui d'un simulateur temps réel d'un filtre RL triphasé et les deux sont embarqués dans le dispositif de commande du redresseur pour estimer les courants de lignes. Ces courants sont injectés dans le dispositif de commande dans le cas d'un défaut de capteur de courant. La capacité de cet estimateur de garantir la continuité de service en cas de défauts est validée par des tests HIL et expérimentalement. / The aim of this thesis work is to develop an IP-Library of FPGA-based embedded real-time simulator IPs (Intellectual Properties) that simulate different elements of an electrical system. These IPs have been designed to be used not only for Hardware-In-the-Loop (HIL) testing of digital controllers but also for low cost embedded control applications, where the simulator IP and the controller are both implemented and run altogether in the same FPGA device. This emerging class of real-time simulators is expected to be more and more included in the next generation of digital controllers. Indeed, such embedded real-time simulator IPs can be advantageously embedded within digital controllers to ensure functions like observation, estimation, diagnostic or health-monitoring. Conversely to the HIL case, the main challenge when designing such simulator IPs is to cope with their complexity having in mind that, in the case of embedded systems, the available hardware resources are limited due to the cost. Furthermore, this challenge is strengthened by the need of very short simulation time-steps which is typically the case when simulating power converters.To develop these IPs, dedicated design guidelines have been proposed to be followed to manage the complexity of these simulator IPs (model solver, numerical solver, time-step, data conditioning) with regards to the timing and the area/cost constraints (computation time limit, limited hardware resources …).The simulators IPs to be developed have been organized into two main categories: those dedicated to electromagnetic elements of an electrical system and those dedicated to their switching elements.The first category gathers elements where electric, magnetic phenomena are modelized in addition to mechanical phenomena (for moving systems) and potentially thermal phenomena. Three cases are dealt with: the embedded real-time simulator of a three-phase synchronous machine, the one of a three-phase induction machine and the one of a brushless synchronous generator. Also, the advantages of using delta transformation to improve the stability of the numerical solver when short simulation time-step and fixed-point (with limited data precision) are used, have been studied.The second category concerns switching elements such as power converters where switching events are considered. Here again, several converter topologies have been studied: a half-wave rectifier, a buck DC-DC converter, a bidirectional buck DC-DC converter, a H-bridge DC-DC converter, a single-phase H-bridge DC-AC converter, a three-phase voltage source inverter, a three-phase diode rectifier and a three-phase PWM rectifier. For all these IPs, the Associated Discrete Circuit (ADC) modeling approach is adopted.The embedded real-time simulator IP of the three-phase PWM rectifier has been applied in the context of an embedded application. The latter consists of a fault-tolerant control of a grid-connected voltage source rectifier. Thus, this simulator IP is associated with the one of a three-phase RL-filter and are both implemented within the rectifier controller to estimate the grid currents. These currents are injected in the controller in the case of a current sensor fault. The ability of this estimator to guarantee the service continuity in the case of faults is validated through HIL tests and experiments.

This work deals with the automatic control of calculations of specialized system. The reader is acquainted with the numerical solution of differential equations by Taylor series method and numerical integrators. The practical aim of this work is to analyze parallel characteristics of Taylor series method, specification of parallel math operations and design of control of this operations.

In this diploma thesis, the reader is introduced to artificial neural networks and convolutional neural networks. Based on that, the design and implementation of a new library for convolutional neural networks is described. The library is then evaluated on widely used datasets and compared to other publicly available libraries. The added benefit of the library, that makes it unique, is its independence on data types. Each layer may contain up to three independent data types - for weights, for inference and for training. For the purpose of evaluating this feature, a data type with fixed point representation is also part of the library. The effects of this representation on trained net accuracy are put to a test.

This thesis deals with the concepts of numerical integrator using floating point arithmetic for solving partial differential equations. The integrator uses Euler method and Taylor series. Thesis shows parallel and serial approach to computing with exponents and significands. There is also a comparison between modern parallel systems and the proposed concepts.

Tato diplomová práce se zabývá  aproximativní implementace aritmetických operací v obrazových filtrech. Zejména tedy využitím aproximativních technik pro úpravu způsobu násobení v netriviálním obrazovém filtru. K tomu je využito několik technik, jako použití převodu násobení s pohyblivou řadovou čárkou na násobení s pevnou řadovou čárkou, či využití evolučních algoritmů zejména kartézkého genetického programování pro vytvoření nových aproximovaných násobiček, které vykazují přijatelnou chybu, ale současně redukují výpočetní náročnost filtrace. Výsledkem jsou evolučně navržené aproximativní násobičky zohledňující distribuci dat v obrazovém filtru a jejich nasazení v obrazovém filtru a porovnání původního filtru s aproximovaným fitrem na sadě barevných obrázků.

This thesis describes the development of voice module, that can recognize simple speech commands by comparation of input sound with recorded templates. The first part of thesis contains a description of used algorithm and a verification of its functionality. The algorithm is based on Mel-frequency cepstral coefficients and dynamic time warping. Thereafter the hardware of voice module is designed, containing signal controller 56F805 from Freescale. The signal from microphone is conditioned by operational amplifiers and digital filter. The third part deals with the development of software for the controller and describes the fixed point implementation of the algorithm, respecting limited capabilities of the controller. Final test proves the usability of voice module in low-noise environment.