Contribuições para o processo de verificação de satisfatibilidade módulo teoria em Event-B

Event-B is a formal method for modeling and verification of discrete transition systems. Event-B development yields proof obligations that must be verified (i.e. proved valid) in order to keep the produced models consistent. Satisfiability Modulo Theory solvers are automated theorem provers used to verify the satisfiability of logic formulas considering a background theory (or combination of theories). SMT solvers not only handle large firstorder formulas, but can also generate models and proofs, as well as identify unsatisfiable subsets of hypotheses (unsat-cores). Tool support for Event-B is provided by the Rodin platform: an extensible Eclipse based IDE that combines modeling and proving features. A SMT plug-in for Rodin has been developed intending to integrate alternative, efficient verification techniques to the platform. We implemented a series of complements to the SMT solver plug-in for Rodin, namely improvements to the user interface for when proof obligations are reported as invalid by the plug-in. Additionally, we modified some of the plug-in features, such as support for proof generation and unsat-core extraction, to comply with the SMT-LIB standard for SMT solvers. We undertook tests using applicable proof obligations to demonstrate the new features. The contributions described can potentially affect productivity in a positive manner.

An evaluation of home range models for marine fish tracking and fine scale habitat use and movement patterns of age 1 Greenland cod (Gadus macrocephalus ogac)

My thesis examines fine-scale habitat use and movement patterns of age 1 Greenland cod (Gadus macrocephalus ogac) tracked using acoustic telemetry. Recent advances in tracking technologies such as GPS and acoustic telemetry have led to increasingly large and detailed datasets that present new opportunities for researchers to address fine-scale ecological questions regarding animal movement and spatial distribution. There is a growing demand for home range models that will not only work with massive quantities of autocorrelated data, but that can also exploit the added detail inherent in these high-resolution datasets. Most published home range studies use radio-telemetry or satellite data from terrestrial mammals or avian species, and most studies that evaluate the relative performance of home range models use simulated data. In Chapter 2, I used actual field-collected data from age-1 Greenland cod tracked with acoustic telemetry to evaluate the accuracy and precision of six home range models: minimum convex polygons, kernel densities with plug-in bandwidth selection and the reference bandwidth, adaptive local convex hulls, Brownian bridges, and dynamic Brownian bridges. I then applied the most appropriate model to two years (2010-2012) of tracking data collected from 82 tagged Greenland cod tracked in Newman Sound, Newfoundland, Canada, to determine diel and seasonal differences in habitat use and movement patterns (Chapter 3). Little is known of juvenile cod ecology, so resolving these relationships will provide valuable insight into activity patterns, habitat use, and predator-prey dynamics, while filling a knowledge gap regarding the use of space by age 1 Greenland cod in a coastal nursery habitat. By doing so, my thesis demonstrates an appropriate technique for modelling the spatial use of fish from acoustic telemetry data that can be applied to high-resolution, high-frequency tracking datasets collected from mobile organisms in any environment.

On point estimation of the abnormality of a Mahalanobis index

Open Access funded by Medical Research Council Acknowledgment The work reported here was funded by a grant from the Medical Research Council, UK, grant number: MR/J013838/1.

Génération de squelettes des contrats de classes et des tests unitaires en Java

Le logiciel est devenu omniprésent dans nos vies de sorte qu'on le retrouve dans plusieurs domaines de la vie courante. Cependant cette omniprésence, n'est pas sans conséquences. Les bogues de logiciel peuvent causer de vrais désastres, économiques, écologiques voire sanitaires. Vu la forte omniprésente du logiciel dans nos vies, le fonctionnement de nos sociétés dépend fortement de sa qualité. La programmation par contrat a pour but de produire des logiciels fiables, c'est-à-dire corrects et robustes. En effet, ce paradigme de programmation vise à introduire des assertions qui sont des spécifications de services. Ces spécifications représentent une forme de contrat. Les contrats définissent les responsabilités entre le client et le fournisseur. Le respect des contrats permet de garantir que le logiciel ne fait ni plus ni moins que ce que l'on attend de lui qu'il fasse. Le test unitaire est un test qui permet de s'assurer du bon fonctionnement d'une partie précise d'un logiciel. C'est un test dont la vérification se fait en exécutant une petite unité de code. En somme, un test unitaire est un code qui exécute de manière indirecte le code d'une classe pour vérifier que le code fonctionne bien. L'outil Génération de Squelettes des Contrats de classes et des tests unitaires (GACTUS) permet la génération automatique de squelettes de contrats de classes et celles des classes des tests unitaires d'un projet Java. La génération automatique du code source permet d'obtenir un code uniforme. GACTUS est un plug-in pour l'environnement de développement Eclipse écrit en Java. L'objectif principal de GACTUS est de faciliter la réalisation de logiciel de qualité grâce à la génération automatique des squelettes de contrats de classe et celui des tests unitaires et aussi d'accroître la productivité des développeurs. Pour faciliter son utilisation, GACTUS dispose d'une interface graphique permettant de guider l'utilisateur.

Classificação de veículos híbridos - evolução crescente do grau de electrificação

Em resposta aos impactos ambientais e limitações dos combustíveis fósseis, assistiu-se nas últimas décadas a um acentuado desenvolvimento dos veículos híbridos elétricos convencionais. A sua proliferação encontra-se hoje bem disseminada, em praticamente todas as gamas, refletindo a confiança dos consumidores. Com vista a atenuar ainda mais o uso dos combustíveis fósseis, a tendência é de aumentar o nível de eletrificação nas versões híbridas mais recentes, bem como da oferta de versões puramente elétricas. No entanto, a evolução dos últimos anos, quer ao nível da aposta por parte dos fabricantes, quer ao nível do volume de vendas, parece indiciar uma nova fase de proliferação destes veículos, a qual se encontra ainda a dar os primeiros passos. Este artigo apresenta uma classificação dos veículos híbridos, em função do nível de eletrificação do sistema de propulsão. Após uma breve referência aos veículos puramente elétricos, fazem-se algumas considerações acerca do impacto mundial dos veículos híbridos Plug-in e puramente elétricos, nos últimos 5 anos.

Essays on mixed-frequency data : forecasting and unit root testing

Doutoramento em Economia

Hybrid Power System Intelligent Operation and Protection Involving Distributed Architectures and Pulsed Loads

Efficient and reliable techniques for power delivery and utilization are needed to account for the increased penetration of renewable energy sources in electric power systems. Such methods are also required for current and future demands of plug-in electric vehicles and high-power electronic loads. Distributed control and optimal power network architectures will lead to viable solutions to the energy management issue with high level of reliability and security. This dissertation is aimed at developing and verifying new techniques for distributed control by deploying DC microgrids, involving distributed renewable generation and energy storage, through the operating AC power system. To achieve the findings of this dissertation, an energy system architecture was developed involving AC and DC networks, both with distributed generations and demands. The various components of the DC microgrid were designed and built including DC-DC converters, voltage source inverters (VSI) and AC-DC rectifiers featuring novel designs developed by the candidate. New control techniques were developed and implemented to maximize the operating range of the power conditioning units used for integrating renewable energy into the DC bus. The control and operation of the DC microgrids in the hybrid AC/DC system involve intelligent energy management. Real-time energy management algorithms were developed and experimentally verified. These algorithms are based on intelligent decision-making elements along with an optimization process. This was aimed at enhancing the overall performance of the power system and mitigating the effect of heavy non-linear loads with variable intensity and duration. The developed algorithms were also used for managing the charging/discharging process of plug-in electric vehicle emulators. The protection of the proposed hybrid AC/DC power system was studied. Fault analysis and protection scheme and coordination, in addition to ideas on how to retrofit currently available protection concepts and devices for AC systems in a DC network, were presented. A study was also conducted on the effect of changing the distribution architecture and distributing the storage assets on the various zones of the network on the system’s dynamic security and stability. A practical shipboard power system was studied as an example of a hybrid AC/DC power system involving pulsed loads. Generally, the proposed hybrid AC/DC power system, besides most of the ideas, controls and algorithms presented in this dissertation, were experimentally verified at the Smart Grid Testbed, Energy Systems Research Laboratory. All the developments in this dissertation were experimentally verified at the Smart Grid Testbed.

A NOVEL MODELING AND STATE OF CHARGE ESTIMATION SCHEME FOR LITHIUM-ION BATTERIES

Lithium Ion (Li-Ion) batteries have got attention in recent decades because of their undisputable advantages over other types of batteries. They are used in so many our devices which we need in our daily life such as cell phones, lap top computers, cameras, and so many electronic devices. They also are being used in smart grids technology, stand-alone wind and solar systems, Hybrid Electric Vehicles (HEV), and Plug in Hybrid Electric Vehicles (PHEV). Despite the rapid increase in the use of Lit-ion batteries, the existence of limited battery models also inadequate and very complex models developed by chemists is the lack of useful models a significant matter. A battery management system (BMS) aims to optimize the use of the battery, making the whole system more reliable, durable and cost effective. Perhaps the most important function of the BMS is to provide an estimate of the State of Charge (SOC). SOC is the ratio of available ampere-hour (Ah) in the battery to the total Ah of a fully charged battery. The Open Circuit Voltage (OCV) of a fully relaxed battery has an approximate one-to-one relationship with the SOC. Therefore, if this voltage is known, the SOC can be found. However, the relaxed OCV can only be measured when the battery is relaxed and the internal battery chemistry has reached equilibrium. This thesis focuses on Li-ion battery cell modelling and SOC estimation. In particular, the thesis, introduces a simple but comprehensive model for the battery and a novel on-line, accurate and fast SOC estimation algorithm for the primary purpose of use in electric and hybrid-electric vehicles, and microgrid systems. The thesis aims to (i) form a baseline characterization for dynamic modeling; (ii) provide a tool for use in state-of-charge estimation. The proposed modelling and SOC estimation schemes are validated through comprehensive simulation and experimental results.

Diclofenaco comparado con ibuprofeno para el cierre de Ductus arterioso persistente, en recién nacidos prematuros

Introducción: El Ductus arterioso persistente (DAP), es uno de los defectos congénitos cardiacos más comunes, requiere manejo farmacológico y/o quirúrgico; presenta complicaciones hemodinámicas, respiratorias y muerte. Los medicamentos de elección para su manejo son indometacina e ibuprofeno, pero su costo y accesibilidad llevo al uso de diclofenaco como alternativa de manejo en algunos hospitales. Objetivo: Comparar respuesta al tratamiento con diclofenaco vs ibuprofeno en cierre de DAP. Materiales y Métodos: Estudio observacional analítico retrospectivo, que compara los resultados obtenidos al usar Diclofenaco e Ibuprofeno para el cierre del DAP en recién nacidos pretérmino. Se recolecto información de pacientes hospitalizados en la Unidad Neonatal de un Hospital II nivel de Bogotá. Se revisaron las historias clínicas de pacientes de edad gestacional entre 24 y 36 semanas por Ballard con los criterios para diagnóstico de DAP y recibieron tratamiento farmacológico con una de las siguientes opciones: Ibuprofeno 10 mg/Kg dosis inicial después 5mg/Kg a las 24 48 horas, o Diclofenaco 0.2 mg/Kg dosis cada 12 horas tres dosis. Se comparó el Diclofenaco y el Ibuprofeno para el tratamiento farmacológico de DAP en recién nacidos prematuros. Resultados: Fueron evaluados 103 pacientes, el diagnóstico de DAP se realizó con ecocardiograma transtorácico, el 66.6 % de los pacientes presentó cierre farmacológico con Diclofenaco y 69 % con Ibuprofeno, La mortalidad fue de 17.65 % con Diclofenaco y 11.54 % con ibuprofeno; en ambos casos asociadas a la prematurez. Conclusiones: El éxito farmacológico fue similar en ambos grupos, el diclofenaco es una alternativa interesante cuando la terapia convencional no esté disponible.

Evaluación técnica y económica para analizar la viabilidad del montacargas eléctrico en el sector productivo

Esta tesis pretende demostrar y describir las diferentes características de los montacargas que existen en el mercado, teniendo en cuenta sus ventajas y desventajas, logrando como objetivo analizar la viabilidad de la implementación de los montacargas eléctricos en la industria colombiana a partir de la información brindada sobre las características esenciales de los montacargas eléctricos que hay en el mercado. Así mismo, se quiere mostrar que los montacargas eléctricos generan un ahorro sustancial en comparación con los montacargas convencionales que hay hoy en día en el mercado, logrando así que la industria colombiana reduzca sus gastos en un porcentaje mediante la implementación de las nuevas referencias de montacargas eléctricos los cuales serian una alternativa para las compañías colombianas. Mediante una detallada revisión conceptual, se mostrara la viabilidad de los montacargas eléctricos frente a los otros tipos de montacargas, teniendo como premisa el conocimiento de lo que hoy en día requieren las industrias colombianas, y cumpliendo así con una detallada comparación en donde se enfatice la diferenciación de los montacargas eléctricos con otros tipos que existen y se logre brindar una clara percepción de estos junto con las ventajas de estos vehículos para lograr así brindar mayor información a la industria colombiana sobre las ventajas de la implementación de los montacargas eléctricos en la industria colombiana.

Using linear algebra for protein structural comparison and classification.

In this article, we describe a novel methodology to extract semantic characteristics from protein structures using linear algebra in order to compose structural signature vectors which may be used efficiently to compare and classify protein structures into fold families. These signatures are built from the pattern of hydrophobic intrachain interactions using Singular Value Decomposition (SVD) and Latent Semantic Indexing (LSI) techniques. Considering proteins as documents and contacts as terms, we have built a retrieval system which is able to find conserved contacts in samples of myoglobin fold family and to retrieve these proteins among proteins of varied folds with precision of up to 80%. The classifier is a web tool available at our laboratory website. Users can search for similar chains from a specific PDB, view and compare their contact maps and browse their structures using a JMol plug-in.

Modelling and Optimization of Energy Management Strategies for Hybrid Vehicles

In the last decades the automotive sector has seen a technological revolution, due mainly to the more restrictive regulation, the newly introduced technologies and, as last, to the poor resources of fossil fuels remaining on Earth. Promising solution in vehicles’ propulsion are represented by alternative architectures and energy sources, for example fuel-cells and pure electric vehicles. The automotive transition to new and green vehicles is passing through the development of hybrid vehicles, that usually combine positive aspects of each technology. To fully exploit the powerful of hybrid vehicles, however, it is important to manage the powertrain’s degrees of freedom in the smartest way possible, otherwise hybridization would be worthless. To this aim, this dissertation is focused on the development of energy management strategies and predictive control functions. Such algorithms have the goal of increasing the powertrain overall efficiency and contextually increasing the driver safety. Such control algorithms have been applied to an axle-split Plug-in Hybrid Electric Vehicle with a complex architecture that allows more than one driving modes, including the pure electric one. The different energy management strategies investigated are mainly three: the vehicle baseline heuristic controller, in the following mentioned as rule-based controller, a sub-optimal controller that can include also predictive functionalities, referred to as Equivalent Consumption Minimization Strategy, and a vehicle global optimum control technique, called Dynamic Programming, also including the high-voltage battery thermal management. During this project, different modelling approaches have been applied to the powertrain, including Hardware-in-the-loop, and diverse powertrain high-level controllers have been developed and implemented, increasing at each step their complexity. It has been proven the potential of using sophisticated powertrain control techniques, and that the gainable benefits in terms of fuel economy are largely influenced by the chose energy management strategy, even considering the powerful vehicle investigated.

Development of predictive energy management strategies for hybrid electric vehicles supported by connectivity

Nowadays, the spreading of the air pollution crisis enhanced by greenhouse gases emission is leading to the worsening of the global warming. In this context, the transportation sector plays a vital role, since it is responsible for a large part of carbon dioxide production. In order to address these issues, the present thesis deals with the development of advanced control strategies for the energy efficiency optimization of plug-in hybrid electric vehicles (PHEVs), supported by the prediction of future working conditions of the powertrain. In particular, a Dynamic Programming algorithm has been developed for the combined optimization of vehicle energy and battery thermal management. At this aim, the battery temperature and the battery cooling circuit control signal have been considered as an additional state and control variables, respectively. Moreover, an adaptive equivalent consumption minimization strategy (A-ECMS) has been modified to handle zero-emission zones, where engine propulsion is not allowed. Navigation data represent an essential element in the achievement of these tasks. With this aim, a novel simulation and testing environment has been developed during the PhD research activity, as an effective tool to retrieve routing information from map service providers via vehicle-to-everything connectivity. Comparisons between the developed and the reference strategies are made, as well, in order to assess their impact on the vehicle energy consumption. All the activities presented in this doctoral dissertation have been carried out at the Green Mobility Research Lab} (GMRL), a research center resulting from the partnership between the University of Bologna and FEV Italia s.r.l., which represents the industrial partner of the research project.

High performance battery chargers for full electric and hybrid cars

This Doctoral Thesis aims to study and develop advanced and high-efficient battery chargers for full electric and plug-in electric cars. The document is strictly industry-oriented and relies on automotive standards and regulations. In the first part a general overview about wireless power transfer battery chargers (WPTBCs) and a deep investigation about international standards are carried out. Then, due to the highly increasing attention given to WPTBCs by the automotive industry and considering the need of minimizing weight, size and number of components this work focuses on those architectures that realize a single stage for on-board power conversion avoiding the implementation of the DC/DC converter upstream the battery. Based on the results of the state-of-the-art, the following sections focus on two stages of the architecture: the resonant tank and the primary DC/AC inverter. To reach the maximum transfer efficiency while minimizing weight and size of the vehicle assembly a coordinated system level design procedure for resonant tank along with an innovative control algorithm for the DC/AC primary inverter is proposed. The presented solutions are generalized and adapted for the best trade-off topologies of compensation networks: Series-Series and Series-Parallel. To assess the effectiveness of the above-mentioned objectives, validation and testing are performed through a simulation environment, while experimental test benches are carried out by the collaboration of Delft University of Technology (TU Delft).

DS4H Image Alignment tool, allineamento multimodale automatico: sviluppo di modulo per ottimizzazione dei dati acquisiti ed estensione ad immagini a colori

Molti degli studi oncologici partono dalla analisi di provini istologici, cioè campioni di tessuto prelevati dal paziente. Grazie a marcatori specifici, ovvero coloranti selettivi applicati alla sezione da analizzare, vengono studiate specifiche parti del campione. Spesso per raccogliere più informazioni del campione si utilizzano più marcatori. Tuttavia, questi non sempre possono essere applicati in parallelo e spesso vengono utilizzati in serie dopo un lavaggio del campione. Le immagini così ottenute devono quindi essere allineate per poter procedere con studi di colocalizzazione simulando una acquisizione in parallelo dei vari segnali. Tuttavia, non esiste una procedura standard per allineare le immagini così ottenute. L’allineamento manuale è tempo-dispendioso ed oggetto di possibili errori. Un software potrebbe rendere il tutto più rapido e affidabile. In particolare, DS4H Image Alignment è un plug-in open source implementato per ImageJ/Fiji per allineare immagini multimodali in toni di grigio. Una prima versione del software è stata utilizzata per allineare manualmente una serie di immagini, chiedendo all’utente di definire punti di riferimento comuni a tutte le immagini. In una versione successiva, è stata aggiunta la possibilità di effettuare un allineamento automatico. Tuttavia, questo non era ottimizzato e comportava una perdita di informazione nelle aree non sovrapposte all’immagine definita come riferimento. In questo lavoro, è stato sviluppato un modulo ottimizzato di registrazione automatica di immagini che non assume nessuna immagine di riferimento e preserva tutti i pixel delle immagini originali creando uno stack di dimensioni idonee a contenere il tutto. Inoltre, l’architettura dell’intero software è stata estesa per poter registrare anche immagini a colori.