Distributed and synchronized measurements for the wide-area observation of electric power systems in distorted and low-inertia conditions

With the aim of heading towards a more sustainable future, there has been a noticeable increase in the installation of Renewable Energy Sources (RES) in power systems in the latest years. Besides the evident environmental benefits, RES pose several technological challenges in terms of scheduling, operation, and control of transmission and distribution power networks. Therefore, it raised the necessity of developing smart grids, relying on suitable distributed measurement infrastructure, for instance, based on Phasor Measurement Units (PMUs). Not only are such devices able to estimate a phasor, but they can also provide time information which is essential for real-time monitoring. This Thesis falls within this context by analyzing the uncertainty requirements of PMUs in distribution and transmission applications. Concerning the latter, the reliability of PMU measurements during severe power system events is examined, whereas for the first, typical configurations of distribution networks are studied for the development of target uncertainties. The second part of the Thesis, instead, is dedicated to the application of PMUs in low-inertia power grids. The replacement of traditional synchronous machines with inertia-less RES is progressively reducing the overall system inertia, resulting in faster and more severe events. In this scenario, PMUs may play a vital role in spite of the fact that no standard requirements nor target uncertainties are yet available. This Thesis deeply investigates PMU-based applications, by proposing a new inertia index relying only on local measurements and evaluating their reliability in low-inertia scenarios. It also develops possible uncertainty intervals based on the electrical instrumentation currently used in power systems and assesses the interoperability with other devices before and after contingency events.

User interaction widgets for interactive theorem proving

Matita (that means pencil in Italian) is a new interactive theorem prover under development at the University of Bologna. When compared with state-of-the-art proof assistants, Matita presents both traditional and innovative aspects. The underlying calculus of the system, namely the Calculus of (Co)Inductive Constructions (CIC for short), is well-known and is used as the basis of another mainstream proof assistant—Coq—with which Matita is to some extent compatible. In the same spirit of several other systems, proof authoring is conducted by the user as a goal directed proof search, using a script for storing textual commands for the system. In the tradition of LCF, the proof language of Matita is procedural and relies on tactic and tacticals to proceed toward proof completion. The interaction paradigm offered to the user is based on the script management technique at the basis of the popularity of the Proof General generic interface for interactive theorem provers: while editing a script the user can move forth the execution point to deliver commands to the system, or back to retract (or “undo”) past commands. Matita has been developed from scratch in the past 8 years by several members of the Helm research group, this thesis author is one of such members. Matita is now a full-fledged proof assistant with a library of about 1.000 concepts. Several innovative solutions spun-off from this development effort. This thesis is about the design and implementation of some of those solutions, in particular those relevant for the topic of user interaction with theorem provers, and of which this thesis author was a major contributor. Joint work with other members of the research group is pointed out where needed. The main topics discussed in this thesis are briefly summarized below. Disambiguation. Most activities connected with interactive proving require the user to input mathematical formulae. Being mathematical notation ambiguous, parsing formulae typeset as mathematicians like to write down on paper is a challenging task; a challenge neglected by several theorem provers which usually prefer to fix an unambiguous input syntax. Exploiting features of the underlying calculus, Matita offers an efficient disambiguation engine which permit to type formulae in the familiar mathematical notation. Step-by-step tacticals. Tacticals are higher-order constructs used in proof scripts to combine tactics together. With tacticals scripts can be made shorter, readable, and more resilient to changes. Unfortunately they are de facto incompatible with state-of-the-art user interfaces based on script management. Such interfaces indeed do not permit to position the execution point inside complex tacticals, thus introducing a trade-off between the usefulness of structuring scripts and a tedious big step execution behavior during script replaying. In Matita we break this trade-off with tinycals: an alternative to a subset of LCF tacticals which can be evaluated in a more fine-grained manner. Extensible yet meaningful notation. Proof assistant users often face the need of creating new mathematical notation in order to ease the use of new concepts. The framework used in Matita for dealing with extensible notation both accounts for high quality bidimensional rendering of formulae (with the expressivity of MathMLPresentation) and provides meaningful notation, where presentational fragments are kept synchronized with semantic representation of terms. Using our approach interoperability with other systems can be achieved at the content level, and direct manipulation of formulae acting on their rendered forms is possible too. Publish/subscribe hints. Automation plays an important role in interactive proving as users like to delegate tedious proving sub-tasks to decision procedures or external reasoners. Exploiting the Web-friendliness of Matita we experimented with a broker and a network of web services (called tutors) which can try independently to complete open sub-goals of a proof, currently being authored in Matita. The user receives hints from the tutors on how to complete sub-goals and can interactively or automatically apply them to the current proof. Another innovative aspect of Matita, only marginally touched by this thesis, is the embedded content-based search engine Whelp which is exploited to various ends, from automatic theorem proving to avoiding duplicate work for the user. We also discuss the (potential) reusability in other systems of the widgets presented in this thesis and how we envisage the evolution of user interfaces for interactive theorem provers in the Web 2.0 era.

Apnea e reflusso gastroesofageo nel neonato pretermine

Objective: To document the existence of a relationship between apnea of prematurity (AOP) and gastroesophageal reflux (GER) in preterm infants. Setting: One Neonatal Intensive Care Unit Patients: Twenty-six preterm infants (gestational age<32 weeks) with recurrent apneas. Intervention: Simultaneous and synchronized recording of polysomnography and pH-impedance monitoring (pH-MII). Polysomnography detects and characterizes apneas, by recording of breathing movement, nasal airflow, electrocardiogram, pulse oximeter saturation. pH-MII is the state-of-theart methodology for GER detection in preterm newborns. Main outcome measures: Relationship between AOP and GER, which were considered temporally related if both started within 30 seconds of each other. Results: One-hundred-fifty-four apneas out of 1136 were temporally related to GER. The frequency of apnea during the one-minute time around the onset of GER was significantly higher than the one detected in the GER-free period (p=0.03). Furthermore, the frequency of apnea in the 30 seconds after GER (GER-triggered apneas) was greater than that detected in the 30 seconds before (p=0.01). A great inter-individual variability was documented in the proportion of GERtriggered apneas. A strong correlation between total number of apneas and the difference between apneas detected 30 seconds after and before GER was found (p=0.034). Conclusions: Our data show that a variable rate of apneas can be triggered by GER in very preterm infant. Further studies are needed to recognise clinical features which identify those patients who are more susceptible to GER-triggered apneas.

Ruolo del Porcine Circovirus tipo 2 (PCV2) nella patologia riproduttiva del suino

La tesi è organizzata in 4 capitoli: -nel primo vengono brevemente riferite le patologie associate all’infezione da PCV2 con particolare riferimento all’iter diagnostico ed al ruolo rivestito dall’esame istologico e dalla identificazione dell’agente eziologico in situ contestualmente alle lesioni istologiche; -nel secondo viene presentato un iter diagnostico originale da applicare in condizioni di campo, qualora si voglia accertare la presenza del PCV2 nei tessuti dei prodotti di natimortalità/aborto del suino. In specifico si riferisce all’applicazione del protocollo in 2 aziende ed i risultati vengono analizzati per una revisione critica del protocollo impiegato; -nel terzo vengono presentati i risultati di un protocollo di infezione con PCV2 per via genitale tramite seme infetto. Scrofe convenzionali sono state sincronizzate per l’estro e fecondate con un’unica dose di seme PCV2 negativo alla PCR (gruppo controlli) o sperimentalmente esposto al PCV2 (gruppo infette). I risultati vengono analizzati in funzione delle ripercussioni che l’infezione precoce in gravidanza può produrre sulla scrofa (mancata gravidanza, ritorno in calore), sui feti e sugli invogli fetali. Viene stabilito il ruolo protettivo degli anticorpi circolanti al momento dell’infezione, stante l’evenienza che un basso titolo anticorpale si associa a viremia prolungata e maggiore numero di feti positivi al virus; -nel quarto viene presentato un esperimento sovrapponibile a quello riferito nel capitolo 3, però con la presenza anche di un gruppo di soggetti convenzionali vaccinati ed infettati con PCV2 durante la fecondazione artificiale usando seme sperimentalmente esposto al virus. Nella discussione dei risultati vengono enfatizzati 2 aspetti importanti nell’epidemiologia dell’infezione da PCV2: la eliminazione di virus è fortemente ridotta dalla vaccinazione, con conseguenze verosimilmente positive sulla circolazione del virus negli effettivi dell’allevamento; l’esposizione uterina è protetta dalla vaccinazione, stante la bassa percentuale di placente infette nel gruppo dei soggetti vaccinati rispetto a quelli non vaccinati e nei controlli.

The Effect of Metronome Pacing on Gait in Healthy Subjects

The complex process of gait is rendered partially automatic by central pattern generators (CPGs). To further our understanding of their role in gait control in healthy subjects, we applied a paradigm of anti-phase, or syncopated, movement to gait. To provide a context for our results, we reviewed the literature on in-phase, or synchronized, gait. The review results are as follows. Auditory cueing increased step/stride rate for older subjects, but not younger. Stride rate variability decreased for younger subjects, perhaps because the metronome’s cue acted as a temporal ‘anchor point’ for each step. Step width increased in half of the treadmill studies, but none of the overground ones, suggesting a cumulative effect of the attentional demands of synchronizing gait while on a treadmill. Time series analysis revealed that the α exponent was the most sensitive parameter reported, decreasing toward anti-persistence in almost all cued-gait studies. This project compares in-phase (IN) and anti-phase gait (ANTI) in young and old healthy subjects. We expected gait to be less disrupted during ANTI trials at preferred speed, when the facilitating effect of CPGs would be strongest. The measures step time variability, jerk index, and harmonic ratio quantified gait perturbation: none indicated that ANTI was easiest at preferred walking speed. Surprisingly, the gait of older subjects was no more perturbed than that of younger subjects. When they successfully matched the pace of the beat, they unwittingly synchronized to it. The temporal relationship of their steps to the beat was the same in the IN and ANTI conditions. Younger subjects, visibly struggling during ANTI trials, were able to walk in syncopation. This result suggests that cognitive resources available only to the younger group are required to resist synchronizing to the beat.

Modeling, Component Selection and Optimization of Servo-controlled Automatic Machinery

A servo-controlled automatic machine can perform tasks that involve synchronized actuation of a significant number of servo-axes, namely one degree-of-freedom (DoF) electromechanical actuators. Each servo-axis comprises a servo-motor, a mechanical transmission and an end-effector, and is responsible for generating the desired motion profile and providing the power required to achieve the overall task. The design of a such a machine must involve a detailed study from a mechatronic viewpoint, due to its electric and mechanical nature. The first objective of this thesis is the development of an overarching electromechanical model for a servo-axis. Every loss source is taken into account, be it mechanical or electrical. The mechanical transmission is modeled by means of a sequence of lumped-parameter blocks. The electric model of the motor and the inverter takes into account winding losses, iron losses and controller switching losses. No experimental characterizations are needed to implement the electric model, since the parameters are inferred from the data available in commercial catalogs. With the global model at disposal, a second objective of this work is to perform the optimization analysis, in particular, the selection of the motor-reducer unit. The optimal transmission ratios that minimize several objective functions are found. An optimization process is carried out and repeated for each candidate motor. Then, we present a novel method where the discrete set of available motor is extended to a continuous domain, by fitting manufacturer data. The problem becomes a two-dimensional nonlinear optimization subject to nonlinear constraints, and the solution gives the optimal choice for the motor-reducer system. The presented electromechanical model, along with the implementation of optimization algorithms, forms a complete and powerful simulation tool for servo-controlled automatic machines. The tool allows for determining a wide range of electric and mechanical parameters and the behavior of the system in different operating conditions.

Perceiving the 3d world from single images

Depth represents a crucial piece of information in many practical applications, such as obstacle avoidance and environment mapping. This information can be provided either by active sensors, such as LiDARs, or by passive devices like cameras. A popular passive device is the binocular rig, which allows triangulating the depth of the scene through two synchronized and aligned cameras. However, many devices that are already available in several infrastructures are monocular passive sensors, such as most of the surveillance cameras. The intrinsic ambiguity of the problem makes monocular depth estimation a challenging task. Nevertheless, the recent progress of deep learning strategies is paving the way towards a new class of algorithms able to handle this complexity. This work addresses many relevant topics related to the monocular depth estimation problem. It presents networks capable of predicting accurate depth values even on embedded devices and without the need of expensive ground-truth labels at training time. Moreover, it introduces strategies to estimate the uncertainty of these models, and it shows that monocular networks can easily generate training labels for different tasks at scale. Finally, it evaluates off-the-shelf monocular depth predictors for the relevant use case of social distance monitoring, and shows how this technology allows to overcome already existing strategies limitations.

Fattori che influenzano l'esame angio-TC del distretto addominale nel cane: una revisione sistematica

Lo scopo dell’AngioTC è quello di ottenere un’opacizzazione adeguata del comparto vascolare esaminato, sincronizzata all’acquisizione della scansione TC. La distribuzione del mezzo di contrasto (mdc) e l’opacizzazione dei distretti corporei, definita enhancement, è influenzata da diversi fattori: relativi al paziente, al mdc o allo scanner TC. In Medicina Veterinaria sono presenti pochi studi indirizzati a valutare l’influenza di diversi fattori sull’enhancement. La ricerca è stata condotta seguendo le linee guida PRISMA (Preferred Reporting Items for Systematic Reviews, 2020). Il database online di diversi motori di ricerca scientifici (Web of Science, PubMed, Scopus e CABAbstract) è stato esaminato mediante combinazione di diverse parole chiave. Sono stati individuati 20 studi che rispettavano i criteri di inclusione, inseriti nel corpo finale della revisione sistematica e raggruppati sulla base della categoria di appartenenza. Si è visto come la quantità di tessuto adiposo addominale sull’enhancement rappresenti un fattore che permette di ridurre la dose di mezzo di contrasto utilizzato, riducendo effetti avversi o tossicità sull’animale. Per quanto riguarda l’iniezione del mdc, un fattore in grado di influenzare maggiormente l’enhancement sembra essere la velocità di trasporto dello Iodio, piuttosto che la durata di iniezione, soprattutto a livello arterioso ed epatico. Con uno scanner lento o una durata di scansione lunga, è consigliato utilizzare una durata fissa di iniezione del mdc per l’acquisizione delle diverse fasi vascolari. Al contrario, con scanner più performanti la tecnica di bolus tracking garantisce una maggior qualità tra le varie fasi vascolari. È indicato, infine, eseguire un flush con soluzione fisiologica al termine della somministrazione di mdc per incrementare l’enhancement arterioso e ridurre la dose di mdc somministrata. Questa revisione sistematica mette in evidenza alcuni fattori e può fare da base per l’ulteriore approfondimento di alcuni di questi fattori o per la valutazione altri non ancora esaminati in Medicina Veterinaria.