[pt] Os sistemas de potência são projetados para operar com rígidos requisitos de qualidade, de modo que, as usinas hidrelétricas devem gerar energia, mantendo tensão e freqüência elétrica constantes. No método clássico de geração, a freqüência é controlada pelo sistema regulador de velocidade de turbina, que tende a manter a rotação da turbina fixa na velocidade síncrona. Como durante a operação da usina, as condições físicas como, por exemplo, altura de queda e vazão, não reproduzem as de projeto durante todo o tempo, o ponto de operação da turbina pode afastar-se da região de máxima eficiência por longos períodos, reduzindo seu rendimento total. Este trabalho aborda a utilização da máquina de dupla alimentação com conversor estático em seu rotórico para geração hidrelétrica em regime de velocidade ajustável, com desacoplamento entre a velocidade da turbina e a freqüência do sistema, apresentando os benefícios obtidos através do uso desta tecnologia. / [en] Power systems are designed to operate under strong quality requirements, so that hydroelectric plants have to produce energy with constant voltage and frequency. According to classical generation schemes, frequency is controlled by the speed governors, which tend to maintain the turbine rotating speed fixed at a synchronous speed. During the plant life the basic variables, such as water head and flow, are not the same as those assumed for the design, the turbine s operating point can go out of the region for maximal efficiency for long periods of time, decreasing than the plant total efficiency. This dissertation brings up the use of a double-fed machine with a static converter connected to the rotor s circuit for adjustable speed generation, with the decoupling of the turbine speed and the system frequency. This work does also show the improvements of the use of this technology.

Nous cherchons à améliorer l'état de l'art des implémentations de contrôle de flux d'information dans les systèmes Linux. Le contrôle de flux d'information vise à surveiller la façon dont l'information se dissémine dans le système une fois hors de son conteneur d'origine, contrairement au contrôle d'accès qui ne peut permettre d'appliquer des règles que sur la manière dont les conteneurs sont accédés. Plusieurs défis scientifiques et techniques se sont présentés. Premièrement, la base de code Linux est particulièrement grande, avec quinze millions de lignes de code réparties dans trente-mille fichiers. La première contribution de cette thèse a été un plugin pour le compilateur GCC permettant d'extraire et visualiser aisément les graphes de flot de contrôle des fonctions du noyau. Ensuite, le framework des Linux Security Modules qui est utilisé pour implémenter les moniteurs de flux d'information que nous avons étudiés (Laminar [1], KBlare [2] et Weir [3]) a été conçu en premier lieu pour le contrôle d'accès, et non de flux. La question se pose donc de savoir si le framework est implémenté de telle sorte à permettre la capture de tous les flux produits par les appels système. Nous avons créé et implémenté une analyse statique permettant de répondre à ce problème. Cette analyse statique est implémenté en tant que plugin GCC et nous a permis d'améliorer le framework LSM pour capturer tous les flux. Enfin, nous avons constaté que les moniteurs de flux actuels n'étaient pas résistants aux conditions de concurrence entre les flux et ne pouvaient pas traiter certains canaux ouverts tels que les projections de fichiers en mémoire et les segments de mémoire partagée entre processus. Nous avons implémenté Rfblare, un nouvel algorithme de suivi de flux, pour KBlare, dont nous avons prouvé la correction avec Coq. Nous avons ainsi montré que LSM pouvait être utilisé avec succès pour implémenter le contrôle de flux d'information, et que seules les méthodes formelles, permettant la mise en œuvre de méthodologie, d'analyses ou d'outils réutilisables, permettaient de s'attaquer à la complexité et aux rapides évolutions du noyau Linux. / We look forward to improving the implementations of information flow control mechanisms in Linux Operating Systems. Information Flow Control aims at monitoring how information disseminates in a system once it is out of its original container, unlike access control which can merely apply rule on how the containers are accessed. We met several scientific and technical challenges. First of all, the Linux codebase is big, over fifteen millions lines of code spread over thirty three thousand files. The first contribution of this thesis is a plugin for the GCC compiler able to extract and let a user easily visualize the control flow graphs of the Linux kernel functions. Secondly, the Linux Security Modules framework which is used to implement the information flow trackers we have reviewed (Laminar, KBlare, and Weir) was designed in the first place to implement access control, rather than information flow control. One issue is thus left open: is the framework implemented in such a way that all flows generated by system calls can be captured? We have created and implemented static analysis to address this problem and proved its correction with the Coq proof assistant system. This analysis is implemented as a GCC plugin and have allowed us to improve the LSM framework in order to capture all flows. Finally, we have noted that current information flow trackers are vulnerable to race conditions between flows and are unable to cover some overt channels of information such as files mapping to memory and shared memory segments between processes. We have implemented Rfblare, a new algorithm of flow tracking, for KBlare. The correction of this algorithm has been proved with Coq. We have showed that LSM can be used successfully to implement information flow control, and that only formal methods, leading to reusable methodology, analysis, tools, etc., are a match for the complexity and the fast-paced evolution of the Linux kernel.

Trees are one of the most fundamental structures in computer science. Standard pointer-based representations consume a significant amount of space while only supporting a small set of navigational operations. Succinct data structures have been developed to overcome these difficulties. A succinct data structure for an object from a given class of objects occupies space close to the information-theoretic lower-bound for representing an object from the class, while supporting the required operations on the object efficiently. In this thesis we consider representing trees succinctly. Various succinct representations have been designed for representing different classes of trees, namely, ordinal trees, cardinal trees and labelled trees. Barring a few, most of these representations are static in that they do not support inserting and deleting nodes. We consider succinct representations for cardinal trees that also support updates (insertions and deletions), i.e., dynamic cardinal trees. A cardinal tree of degree k, also referred to as a k-ary cardinal tree or simply a k-ary tree is a tree where each node has place for up to k children with labels from 1 to k. The information-theoretic lower bound for representing a k-ary cardinal tree on n nodes is roughly (2n+n log k) bits. Representations that take (2n+n log k+ o(n log k ) ) bits have been designed that support basic navigations operations like finding the parent, i-th child, child-labeled j, size of a subtree etc. in constant time. But these could not support updates efficiently. The only known succinct dynamic representation was given by Diego, who gave a structure that still uses (2n+n log k+o(n log k ) ) bits and supports basic navigational operations in O((log k+log log n) ) time, and updates in O((log k + log log n)(1+log k /log (log k + log log n))) amortized time. We improve the times for the operations without increasing the space complexity, for the case when k is reasonably small compared to n. In particular, when k=(O(√(log n ))) our representation supports all the navigational operations in constant time while supporting updates in O(√(log log n )) amortized time.

The primary objective of this thesis is to evaluate how grid computing works with their infrastructure. It also provides study to recognize the cases in which dynamic scheduler is preferable, how can the static recovery schemes play an effective role in large distributed system where load balancing is a key element and how can we get optimality in maximum number of crash computers using dynamic or static recovery schemes. This thesis consists of two parts: construction of Golomb and Trapezium modules, and performance comparison of Golomb and Trapezium recovery schemes with dynamic recovery scheme. In the first part we construct two modules that generate the recovery list of n computers, one for Golomb and one for Trapezium. In second part we make three schedulers, two for static recovery scheme and one for dynamic recovery scheme. In static recovery scheme we compare the performance of Golomb and Trapezium recovery scheme then we compare this performance with dynamic recovery scheme by using GridSim. / 0046735991980, 0046766503096

La vérification de logiciels repose le plus souvent sur une spécification formelle encodant les propriétés du programme à vérifier. La tâche de spécification et de vérification déductive des programmes est longue et difficile et nécessite une connaissance des outils de preuve de programmes. En effet, un échec de preuve de programme peut être dû à une non-conformité du code par rapport à sa spécification, à un contrat de boucle ou de fonction appelée trop faible pour prouver une autre propriété, ou à une incapacité du prouveur. Il est souvent difficile pour l’utilisateur de décider laquelle de ces trois raisons est la cause de l’échec de la preuve car cette information n’est pas (ou rarement) donnée par le prouveur et requiert donc une revue approfondie du code et de la spécification. L’objectif de cette thèse est de fournir une méthode de diagnostic automatique des échecs de preuve afin d’améliorer le processus de spécification et de preuve des programmes C. Nous nous plaçons dans le cadre de la plate-forme d’analyse des programmes C FRAMA-C, qui fournit un langage de spécification unique ACSL, un greffon de vérification déductive WP et un générateur de tests structurels PATHCRAWLER. La méthode que nous proposons consiste à diagnostiquer les échecs de preuve en utilisant la génération de tests structurels sur une version instrumentée du programme d’origine / Software verification often relies on a formal specification encoding the program properties to check. Formally specifying and deductively verifying programs is difficult and time consuming and requires some knowledge about theorem provers. Indeed, a proof failure for a program can be due to a noncompliance between the code and its specification, a loop or callee contrat being insufficient to prove another property, or a prover incapacity. It is often difficult for the user to decide which one of these three reasons causes a given proof failure. Indeed, this feedback is not (or rarely) provided by the theorem prover thus requires a thorough review of the code and the specification. This thesis develops a method to automatically diagnose proof failures and facilitate the specification and verification task. This work takes place within the analysis framework for C programs FRAMAC, that provides the specification language ACSL, the deductive verification plugin WP, and the structural test generator PATHCRAWLER. The proposed method consists in diagnosing proof failures using structural test generation on an instrumented version of the program under verification.

The report handles the transmission of signals from piezoresistive pressuresensors and thermocouple from a rotating object. This report also evaluates the possibility to collect data in a datalogger that rotates with the object. Telemetrics was previously used for signaltransmission in Finspång, therefore there has been no tests considering preassure measuring. One transmitting method handled in this report is transmission through a slipring connection. One test with a slipring connection was performed for transmitting signals from a piezoresistive preassuresensor. All parts were mounted on a disc which rotated at 4000 rpm. Measurements were made of static and dynamic preassure. The report also contains a description of the equipment used for the test, and how it was constructed. / Rapporten tar upp överföring av signaler från piezoresistiva tryckgivare samt termoelement från ett roterande objekt. I rapporten redovisas också om det är möjligt att samla in mätdata i en datalogger som roterar med objektet. Eftersom man, i Finspång, tidigare har använt telemetri för signalöverföring från termoelement så har tryckmätning inte provats. Därför har denna metod inte tagits med i rapporten. En överföringsmetod som tas upp i rapporten är överföring med släpring. Ett prov genomfördes med en släpring för överföring av signaler från en piezoresistiv tryckgivare. Allt monterades på en skiva som roterades upp till 4 000 varv/min. Det som mättes var statiskt och dynamiskt tryck. I rapporten finns det beskrivet vilken utrustning som använts vid provet och hur den är konstruerad.

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / This work presents a new energy conditioning system for application in stand-alone photovoltaic systems with battery bank. Firstly, the characteristics of solar photovoltaic energy, the modeling of a photovoltaic cell and the equivalent electrical circuit are presented. In a second moment, the photovoltaic generation systems and a review of the static converters applied to stand-alone photovoltaic systems with battery bank are presented. From this study it is proposed a new photovoltaic generation system, with distributed energy processing based on series-connected DC-DC converters. The proposed system presents better utilization of the energy generated by the panels through the employment of more than one array of photovoltaic panels and a static power converter for each subsystem. Thereby, the losses through shading are reduced, and also the reliability of the system is increased, once even if one of the subsystems fails, the system will keep on generating electricity to the loads of higher priority. Posteriorly, the analyses of the operation of the system and simulation results are presented. Finally, it is presented experimental results, comparing the efficiency of the utilization of the energy generated by the input stage of the proposed system and by a system traditionally employed in stand-alone photovoltaic systems, showing an energy gain of 16% with the utilization of the proposed system for situations in which at least one panel is shaded. / Esta dissertação de mestrado apresenta um novo sistema de condicionamento de energia para aplicação em sistemas fotovoltaicos autônomos com banco de baterias. Inicialmente são apresentadas as características da energia solar fotovoltaica, a modelagem de uma célula fotovoltaica e um circuito elétrico equivalente. Em um segundo momento são apresentados os sistemas de geração fotovoltaica e uma revisão dos conversores estáticos aplicados a sistemas fotovoltaicos autônomos com banco de baterias. A partir deste estudo é proposto um novo sistema de geração fotovoltaica, com processamento distribuído de energia baseada em conversores CC-CC conectados em série. O sistema proposto apresenta um melhor aproveitamento da energia gerada pelos painéis através da utilização de mais de um arranjo de painéis fotovoltaicos e o emprego de um conversor estático de potência para cada subsistema. Assim, as perdas por sombreamento são reduzidas bem como é aumentada a confiabilidade do sistema, pois mesmo com a falha de um dos subsistemas o sistema continuará garantindo energia elétrica para as cargas de maior interesse. Posteriormente, são apresentadas as análises do funcionamento do sistema e resultados de simulação. Por fim, resultados experimentais são apresentados, comparando a eficiência no aproveitamento da energia gerada pelo estágio de entrada do sistema proposto e de um sistema tradicionalmente empregado em sistemas fotovoltaicos autônomos, demonstrando um ganho de energia de 16% com a utilização do sistema proposto para situações em que pelo menos um painel está sombreado.

Testning av flygkontroller på en verklig kvadrokopter är en farlig och utmanande process eftersom kvadrokoptern kan krascha om flygkontrollern inte fungerar eller ifall operatören saknar flygerfarenheter. Den nuvarande lösningen är att montera kvadrokoptern i en mekanisk anordning som möjliggör testning av flygkontroller i säkra miljöer. Problemet med de befintliga testanordningarna är att de inte kan ge realistiska simuleringsförhållanden eftersom de i viss mån påverkar kvadrokopterns rörelse med följden att flygkontroller som utvecklas har begränsad grad av kontroll på kvadrokoptern. Syftet är att utforma en mekanisk anordning som ska ge möjlighet att både testa samt övningsflyga kvadrokoptern utan risk för personliga och materiella skador. Målet är att ta fram ritningar som ska kunna utgöra underlag för framtagning av en testprototyp. En litteraturstudie på befintliga testanordningar genomfördes som användes som underlag tillsammans med kvalitetshuset för att ta fram en kravspecifikation. Därefter genererades ett antal koncept som utvärderades med hjälp av beslutsmatris. Det valda konceptet modellerades sedan i CAD-programmet och utifrån den virtuella modellen konstruerades en verklig modell i trä som testades för att verifiera dess funktion. Resultatet är en fjäderbalanserad testanordning med sex frihetsgrader. Det är en konstruktion i aluminium innehållande en mekanisk arm som ger tre translationsfrihetsgrader, ett kulledsfäste som ger tre rotationsfrihetsgrader samt dragfjädrar för att tyngdkraftskompensera systemet. Testning av trä-modellen uppvisar att kvadrakoptern måste framföras i full fart för att styras tillsammans med armen eftersom friktionen mellan testanordningens leder är hög. Under förutsättning att friktionen mellan lederna kan hanteras verkar det att testanordningen uppfyller de ställda teoretiska förutsättningarna för att inte ha någon väsentlig påverkan på kvadrokoptern. Ändå kravs det kvalificerade tester innan något påstående att testanordningen inte påverkar kvadrokopterns rörelse och därmed kan ge realistiska flygsimuleringsförhållanden, ska kunna anges. / Testing of autonomous flight controllers on a real quadrocopter is a dangerous and challenging process because the quadrocopter can crash in case the flight controller does not function properly or in case the operator has no flight experience. The current solution is to mount the quadrocopter on a teststand, which allow the testing of flight controller in safe environments. The problem with the existing teststands is that they cannot provide realistic free flight conditions as they, to some extent, affect quadrocopter’s movement. Consequently, the developed flight controller is partially able to control the quadrocopter. The purpose with this study is to design a mechanical device for use in testing and learning to fly a quadrocopter without the risk of crashing the flying model or harming the people involved. The goal is to provide drawings for developing a test prototype.In order to understand the problem a literature review of previous test devices was carried out. The findings from the literature review were used in combination with Quality Function Deployment technique to create a House of Quality and thus develop a set of engineering specifications. After that, a number of concepts was generated and then evaluated by Pugh’s method. The selected concept was modeled in the CAD-software and based on the virtual model, a real model made of wood was constructed and tested in order to verify the function of the testbed. The final result is a spring-balanced test device with six degrees of freedom. It is a structure consisting of a mechanical arm providing three translational degrees of freedom, a swivel joint with three rotational degrees of freedom and a set of extension springs to achieve gravity balancing. The experimental results from the wooden model shows that the quadrocopter is required to fly at full speed in order for it to operate with the arm due to the high friction between the joints. Under the condition that the friction between the joints can be managed, the test device seems to fulfill the theoretical requirements for simulating free flight condition. Nevertheless, it requires specialized and advanced testing before any assertion that the test device does not affect the dynamics of quadrocopter and thus it can provide completely realistic flight conditions, can be made.

Title: 3D analysis of immediate effect on posture of shoe with postural insoles based on Rašev and with proceptor insoles PodoAktiv® Objectives: The thesis aims to show the immediate effect of application of custom-made insole on postural hold of chosen body segments and we would like to determine whether it is possible to use PodoAktiv® or insole based on Rašev to correct body posture. Methodology: In this thesis we examined 9 participants who agreed joining the study. We used the Balance®4D device made by Paromed company. The selected body segments were marked by white spheric stickers. To compare postural hold of selected body segments we examined the participants in altogether 4 situations. Barefoot stand, stand in shoes without insoles, stand in shoes with postural insoles based on Rašev and stand in shoes with proceptor insoles PodoAktiv®. Results: The results of this study show that there is a slight immeadiate effect of the custom- made insoles on postural hold of body segments. Larger effect was observed in the participants who already had a bad postural barefoot hold. Of all 6 parameters, the biggest effect was observed in the shift of overall body axis after application of PodoAktiv® insoles. Keywords: Shoe insoles, proprioceptors, somatosensory system, 3D static analysis, postural hold

This paper analyses a panel data of 198 Czech municipalities for the period 2003-2015. The aim is to define determinants of municipalities' tax revenue budgeting errors using static panel data models with fixed and random effect. Czech municipalities have a tendency to underestimate both total and tax revenues. On average, budgeted tax revenues are about 7 % lower than collected revenues during the period under examination. Such action could entail less transparency in budgeting process. Results indicate that structure of tax revenues also plays a role in explaining forecast errors. Further, the analysis shows the impact of electoral cycle and macroeconomic variables on budget deviations.