The conventional approach to validate the analog and mixed signal designs utilizes extensive SPICE-level simulations. The main challenge in this approach is to know when all important corner cases have been simulated. An alternate approach is to use the formal verification techniques. Formal verification techniques have gained wide spread popularity in the digital design domain; but in case of analog and mixed signal designs, a large number of test scenarios need to be designed to generate sufficient simulation traces to test out all the specified system behaviours. Analog and mixed signal designs can be formally modeled as hybrid systems and therefore techniques used for formal analysis and verification of hybrid systems can be applied to the analog and mixed signal designs. Generally, formal verification tools for hybrid systems work at the abstract level where we model the systems in terms of differential equations or algebraic equations. However the analog and mixed signal system designers are very comfortable in designing the circuits at the transistor level. To bridge the gap between abstraction level verification and the designs validation which has been implemented at the transistor level, the very important issue we need to address is: Can we formally verify the circuits at the transistor level itself? For this we have proposed a framework for doing the formal verification of analog and mixed signal designs using SPICE simulation traces in one of the hybrid systems formal verification tools (i.e. Checkmate from CMU). An extension to a formal verification approach of hybrid systems is proposed to verify analog and mixed signal (AMS) designs. AMS designs can be formally modeled as hybrid systems and therefore lend themselves to the formal analysis and verification techniques applied to hybrid systems. The proposed approach employs simulation traces obtained from an actual design implementation of AMS circuit blocks (for example, in the form of SPICE netlists) to carry out formal analysis and verification. This enables the same platform used for formally validating an abstract model of an AMS design to be also used for validating its different refinements and design implementation, thereby providing a simple route to formal verification at different levels of implementation. Our approach has been illustrated through the case studies using simulation traces form the different frameworks i.e. Simulink/Stateflow framework and the SPICE simulation traces. We demonstrate the feasibility of our approach around the Checkmate and the case studies for hybrid systems and the analog and mixed signal designs.

Les dommages oxydatifs de l’ADN sont impliqués dans les processus pathologiques que sont le cancer, les maladies neurodégénératives ou le vieillissement. Ces dommages résultent en partie de l’action des espèces réactives de l’oxygène (ERO), qui proviennent du métabolisme cellulaire ou d’agents exogènes (physiques ou chimiques), et qui conduisent à différents types de lésions parmi lesquelles l’oxydation des bases de l’ADN (8-oxoguanine, 8-oxoG) ou la formation de sites abasiques AP (apurique/apyrimidique). Ces lésions, qui si elles ne sont pas éliminées conduisent à des processus de mutagenèse ou de mort cellulaire, sont prises en charge spécifiquement par le système de réparation de l’ADN par excision de base ou BER. Le BER est initié par l’action d’une ADN glycosylase, telles que la 8-oxoG-ADN glycosylase (Ogg1) chargée d’éliminer la 8-oxoG, une lésion très abondante. Une étude par « double-hybride » initiatrice de ce projet a révélé l’existence d’une interaction in vivo chez S. cerevisiae entre la protéine yOgg1 et la sous-unité catalytique de l’ADN polymérase réplicative Polε (yPol2), également impliquée dans la voie BER chez la levure. Nos travaux démontrent que yOgg1 et yPol2 interagissent bien physiquement entre elles et de façon spécifique. Une étude par troncations et mutagenèse dirigée nous a permis d’identifier le domaine 3’→5’ exonucléase de yPol2 comme faisant partie de la forme tronquée minimale de yPol2 capable d’interagir avec yOgg1. La poche du site actif de yOgg1 et/ou son voisinage immédiat pourrait contenir pour partie le site d’interaction pour yPol2. Nous observons d’ailleurs une corrélation nette entre l’activité de yOgg1 et sa capacité à interagir avec yPol2 dans la levure. De même, l’activité 3’→5’ exonucléase de yPol2 pourrait être liée à son interaction avec yOgg1. D’un point de vue fonctionnel, yPol2 stimulerait l’activité AP lyase de yOgg1 et le couplage entre l’activité ADN glycosylase et AP lyase de l’enzyme, permettant ainsi une meilleure coordination de l’étape d’excision du nucléoside endommagé et l’étape de resynthèse de l’ADN dans la voie BER. / Oxidative DNA damages are involved in pathological processes such as cancer, neurodegenerative diseases and aging. Part of these damages results from the action of reactive oxygen species (ROS), which are produced by cellular metabolism or (physical or chemical) exogenous agents. They lead to different types of DNA lesions including DNA base oxidation (8-oxoguanine, 8-oxoG) and abasic site formation (AP, apuric/apyrimidic). If not removed, these lesions lead to mutagenesis or cell death. Most of base lesions are dealt specifically by the base excision repair (BER) pathway. BER is initiated by a DNA glycosylase, such as 8-oxoG-DNA glycosylase (Ogg1) which is responsible for the removal of 8-oxoG. In previous unpublished work, a yeast two-hybrid study revealed the existence in S. cerevisiae of an interaction between yOgg1 and the catalytic subunit of the replicative DNA polymerase Polε (yPol2), also involved in the BER pathway in eukaryotes. Our work shows that yOgg1 and yPol2 physically and specifically interact with each other. Truncation and site-directed mutagenesis studies allowed us to identify the 3 ' → 5' exonuclease activity domain of yPol2 as part of the minimal form of yPol2 still able to interact with yOgg1. The active site of yOgg1 and/or its immediate vicinity may contain part of its interaction domain with yPol2. Besides, we observe a clear correlation between yOgg1 catalytic activity and its ability to interact with yPol2 in vivo. Similarly, the 3'→5' exonuclease activity of yPol2 could be useful to its interaction with yOgg1. From a functional point of view, yPol2 stimulates in vitro the AP lyase activity of yOgg1 and the coupling of both DNA glycosylase and AP lyase enzyme activity. The interaction yOgg1/yPol2 could allow a better coordination of damaged nucleoside excision and DNA re-synthesis steps in BER.

The dissertation is an publication summary focused on the field of management processes in renewable energy systems, mathematical models and optimization possibilities for large and small scale photovoltaic systems. The articles were published in foreign impacted and reviewd journals and indexed proceedings of foreign and domestic conferences. The main results of the dissertation are the design, configuration and realization of the hybrid energy system with subsequent optimization. Using the data from the laboratory system, a mathematical model was compiled and subsequently validated in the Matlab/Simulink environment for a hybrid energy system with accumulation. The options for power production optimization with photovoltaic sources are based on both operational measurements (for commercial applications) and on the analysis of power flow controllers to optimize the~energy balance (for small scale applications in private buildings).

Master thesis deals with usage issues of autonomous, self-sufficient and decentralized systems. In the first part convectional and experimental sources for autonomous systems are disclosed. Second chapter deals with accumulation of electrical and thermal energy and possibilities of applications. 3rd part is focused on pilot project realized for autonomous and smart systems, which were built in last years. In the 4th chapter electrical and thermal energy consumption curves are made on daily and monthly basis for 4 type objects. In the fifth part issue of autonomy is explained, and for type buildings solutions are made with additional return on investment. The last chapter is focused on calculation of thermal accumulator and briefly discloses small district heating.

Rozptýlená výroba elektrické energie využívající obnovitelné zdroje, jako je sluneční energie, přispívá ke snížení emisí skleníkových plynů. Z hlediska provozu distribuční soustavy je také výhodné, aby energie byla primárně spotřebována v místě výroby. To je částečně možné přizpůsobením spotřeby, ale především využitím akumulačních systémů. V této práci je představen hybridní systém složený z fotovoltaické elektrárny, akumulátoru elektrické energie a akumulátoru tepelné energie. Výběr a parametry všech částí hybridního systému jsou popsány v práci. Akumulátor elektrické energie je navržen a sestaven z LiNiMnCoO2 článků a řídícího systému zajišťujícího bezpečný provoz. Řídicí systém akumulátoru (BMS) zajistí odpojení baterie, pokud je překročen některý z provozních parametrů baterie. Návrh baterie i sestavy je popsán v práci. Akumulátor tepelné energie sestává z výkonového spínače a nádrže na teplou vodu s topnou patronou pro odporový ohřev vody. Na základě rešerše komerčně používaných zařízení pro regulaci příkonu byly definovány jejich nedostatky a na základě nich bylo navrženo optimální řešení. Řešení spočívá v použití komerčního polovodičového spínacího prvku. Pro tento výkonový spínací prvek byla vytvořena zpětnovazební řídící smyčka s regulátorem výkonu, který byl implementován v prostředí softwaru LabVIEW. V práci je také uveden postup návrhu chladiče spínacího prvku a LCL filtru, který je klíčový pro splnění požadavků elektromagnetické kompatibility. V druhé části práce je popsán návrh nadřazeného řídícího algoritmu, jehož úkolem je řídit výkonové toky v hybridním systému tak, aby byly splněny požadavky definované jak uživatelem, tak i okamžitým stavem akumulátorů. Algoritmus byl implementován v prostředí LabVIEW. Funkčnost celého systému byla ověřena měřením v laboratorních podmínkách. Z výsledků plyne, že nadřazený řídící algoritmus funguje správně. Řídící smyčka tepelného akumulátoru je stabilní a reguluje zátěž na požadovanou hodnotu. Přidanou hodnotou je kratší reakční doba na změnu toku výkonu oproti hybridnímu měniči a díky tomu dochází k minimalizaci přetoků elektrické energie do distribuční sítě. Na práci je možné navázat rozšířením stávajícího algoritmu o možnost řízení/ovládání více typů akumulačních jednotek a generátorů nebo implementováním odlišných strategií řízení.

The master’s thesis deals with the principle of the photoelectric effect, the composition of the photovoltaic cell and different types of solar panels. Here is described the principle of converting wind energy into electricity. This master’s thesis describes reasons for using of the hybrid system. The next section describes the measurement system which is used to measure real operating statuses. The last section is an analysis of measured values and there are listed factors influencing the design of hybrid power system.

In contrast to constant operating states, particle and NOx emissions of internal combustion engines are significantly higher during transient operating states, which occur repeatedly at working cycles of mobile machines. This paper therefore deals with the conception, development and testing of hydraulic hybrid systems to reduce these emissions by phlegmatization of the engine. A wheel loader with its machine-typical working cycle serves as an example for the investigation of the benefits of such a system. Therefore, model based development techniques are used. In a holistic machine simulation, four different typical wheel loader cycles were carried out and the optimum size of the hydraulic accumulator for the hybrid system is identified by a parameter variation. The lowest emitted emissions and the smallest construction dimensions are the key elements for the accumulator selection. With an optimal hydraulic accumulator, a reduction in particle emissions of up to 29.4 % is achieved in one of the cycles investigated.

In a traditional relational database management system, queries can only be defined over attributes defined in the schema, but are guaranteed to give single, definitive answer structured exactly as specified in the query. In contrast, an information retrieval system allows the user to pose queries without knowledge of a schema, but the result will be a top-k list of possible answers, with no guarantees about the structure or content of the retrieved documents. In this paper, we present DrillBeyond, a novel IR/RDBMS hybrid system, in which the user seamlessly queries a relational database together with a large corpus of tables extracted from a web crawl. The system allows full SQL queries over the relational database, but additionally allows the user to use arbitrary additional attributes in the query that need not to be defined in the schema. The system then processes this semi-specified query by computing a top-k list of possible query evaluations, each based on different candidate web data sources, thus mixing properties of RDBMS and IR systems. We design a novel plan operator that encapsulates a web data retrieval and matching system and allows direct integration of such systems into relational query processing. We then present methods for efficiently processing multiple variants of a query, by producing plans that are optimized for large invariant intermediate results that can be reused between multiple query evaluations. We demonstrate the viability of the operator and our optimization strategies by implementing them in PostgreSQL and evaluating on a standard benchmark by adding arbitrary attributes to its queries.

This research argues that a diesel-based isolated electrical system can be optimized byintegrating a high share of solar photovoltaic (PV) generation and that the frequencystability of such system can be improved by including the PV participation in frequencyregulation. A case study is developed in order to explore an island’s expansion of theinstalled generating capacity and its optimization. This study uses the tool HOMER tosolve the optimization problem and PowerFactory to verify the frequency stability of theproposed system. The PV integration allows for a reduction of diesel fuel consumption,emissions and generation costs. Additionally, in high PV penetration scenarios, the reducedinertia in such systems can lead to high frequency deviations that may trip the systemprotection. The study demonstrates that the instantaneous frequency deviation after a loadand generation imbalance can be reduced by designing the PVs to operate with an allocatedreserve and a decentralized time-based secondary frequency control. The frequency stabilitywas achieved after different disturbance scenarios under high PV penetration and reducedavailable inertia, indicating that high PV integration is economically and technically feasiblein small island grids. / I detta examensarbete studeras hur ett dieselbaserat och isolerat elsystem kan optimeras genom att integrera en hög andel solceller (PV) i elproduktionen och att frekvensstabilitet kan förbättras när PV användas i regleringen. En fallstudie har utvecklats under denna forskning för att analysera en ökning av den installerade generationskapacitet vid en ö samt hur detta kan optimeras. I denna studie användas verktyget HOMER för modeloptimering och PowerFactory för att testa den optimerade systemfrekvens stabilitet. Med PV generation kan diesel konsumption, utsläpp och kostnader minskas för hela systemet. En hög andel PV i generationen reducerar elsystemet totala svängmassa vilket kan ledda till avvikelser i systemfrekvensen som kan ursaka att skyddsystem aktiveras. Studien demonstrerar att den momentana systemavvikelsen efter en obalans kan reduceras genom att designa PV i systemet med en allokerad reserv och en decentraliserad och tidsbaserad sekundär frekvensreglering. Frekvensstabiliteten nåddes i olika obalans scenarier med hög andel solcellgeneration och misnkat svängsmassa. Detta tyder på att en hög andel PV integration är både ekonomisk- och tekniskt möjligt i mindre elsystem.

Stop-and-Go Adaptive Cruise Control (ACC+) is an extension of Adaptive Cruise Control (ACC) that works at low speed as well as normal highway speeds to regulate the speed of the vehicle relative to the vehicle it is following. In this thesis, we design an ACC+ controller for a scale model electric vehicle that ensures the robust performance of the system under various models of uncertainty. We capture the operation of the hybrid system via a state-chart model that performs mode switching between different digital controllers with additional decision logic to guarantee the collision freedom of the system under normal operation. We apply different controller design methods such as Linear Quadratic Regulator (LQR) and H-infinity and perform multiple simulation runs in MATLAB/Simulink to validate the performance of the proposed designs. We compare the practicality of our design with existing formally verified ACC designs from the literature. The comparisons show that the other formally verified designs exhibit unacceptable behaviour in the form of mode thrashing that produces excessive acceleration and deceleration of the vehicle. While simulations provide some assurance of safe operation of the system design, they do not guarantee system safety under all possible cases. To increase confidence in the system, we use Differential Dynamic Logic (dL) to formally state environmental assumptions and prove safety goals, including collision freedom. The verification is done in two stages. First, we identify the invariant required to ensure the safe operation of the system and we formally verify that the invariant preserves the safety property of any system with similar dynamics. This procedure provides a high level abstraction of a class of safe solutions for ACC+ system designs. Second, we show that our ACC+ system design is a refinement of the abstract model. The safety of the closed loop ACC+ system is proven by verifying bounds on the system variables using the KeYmaera verification tool for hybrid systems. The thesis demonstrates how practical ACC+ controller designs optimized for fuel economy, passenger comfort, etc., can be verified by showing that they are a refinement of the abstract high level design. / Thesis / Master of Applied Science (MASc)