Automated wordlength optimization framework for multi-source statistical interval-based analysis of nonlinear systems with control-flow structures

El uso de aritmética de punto fijo es una opción de diseño muy extendida en sistemas con fuertes restricciones de área, consumo o rendimiento. Para producir implementaciones donde los costes se minimicen sin impactar negativamente en la precisión de los resultados debemos llevar a cabo una asignación cuidadosa de anchuras de palabra. Encontrar la combinación óptima de anchuras de palabra en coma fija para un sistema dado es un problema combinatorio NP-hard al que los diseñadores dedican entre el 25 y el 50 % del ciclo de diseño. Las plataformas hardware reconfigurables, como son las FPGAs, también se benefician de las ventajas que ofrece la aritmética de coma fija, ya que éstas compensan las frecuencias de reloj más bajas y el uso más ineficiente del hardware que hacen estas plataformas respecto a los ASICs. A medida que las FPGAs se popularizan para su uso en computación científica los diseños aumentan de tamaño y complejidad hasta llegar al punto en que no pueden ser manejados eficientemente por las técnicas actuales de modelado de señal y ruido de cuantificación y de optimización de anchura de palabra. En esta Tesis Doctoral exploramos distintos aspectos del problema de la cuantificación y presentamos nuevas metodologías para cada uno de ellos: Las técnicas basadas en extensiones de intervalos han permitido obtener modelos de propagación de señal y ruido de cuantificación muy precisos en sistemas con operaciones no lineales. Nosotros llevamos esta aproximación un paso más allá introduciendo elementos de Multi-Element Generalized Polynomial Chaos (ME-gPC) y combinándolos con una técnica moderna basada en Modified Affine Arithmetic (MAA) estadístico para así modelar sistemas que contienen estructuras de control de flujo. Nuestra metodología genera los distintos caminos de ejecución automáticamente, determina las regiones del dominio de entrada que ejercitarán cada uno de ellos y extrae los momentos estadísticos del sistema a partir de dichas soluciones parciales. Utilizamos esta técnica para estimar tanto el rango dinámico como el ruido de redondeo en sistemas con las ya mencionadas estructuras de control de flujo y mostramos la precisión de nuestra aproximación, que en determinados casos de uso con operadores no lineales llega a tener tan solo una desviación del 0.04% con respecto a los valores de referencia obtenidos mediante simulación. Un inconveniente conocido de las técnicas basadas en extensiones de intervalos es la explosión combinacional de términos a medida que el tamaño de los sistemas a estudiar crece, lo cual conlleva problemas de escalabilidad. Para afrontar este problema presen tamos una técnica de inyección de ruidos agrupados que hace grupos con las señales del sistema, introduce las fuentes de ruido para cada uno de los grupos por separado y finalmente combina los resultados de cada uno de ellos. De esta forma, el número de fuentes de ruido queda controlado en cada momento y, debido a ello, la explosión combinatoria se minimiza. También presentamos un algoritmo de particionado multi-vía destinado a minimizar la desviación de los resultados a causa de la pérdida de correlación entre términos de ruido con el objetivo de mantener los resultados tan precisos como sea posible. La presente Tesis Doctoral también aborda el desarrollo de metodologías de optimización de anchura de palabra basadas en simulaciones de Monte-Cario que se ejecuten en tiempos razonables. Para ello presentamos dos nuevas técnicas que exploran la reducción del tiempo de ejecución desde distintos ángulos: En primer lugar, el método interpolativo aplica un interpolador sencillo pero preciso para estimar la sensibilidad de cada señal, y que es usado después durante la etapa de optimización. En segundo lugar, el método incremental gira en torno al hecho de que, aunque es estrictamente necesario mantener un intervalo de confianza dado para los resultados finales de nuestra búsqueda, podemos emplear niveles de confianza más relajados, lo cual deriva en un menor número de pruebas por simulación, en las etapas iniciales de la búsqueda, cuando todavía estamos lejos de las soluciones optimizadas. Mediante estas dos aproximaciones demostramos que podemos acelerar el tiempo de ejecución de los algoritmos clásicos de búsqueda voraz en factores de hasta x240 para problemas de tamaño pequeño/mediano. Finalmente, este libro presenta HOPLITE, una infraestructura de cuantificación automatizada, flexible y modular que incluye la implementación de las técnicas anteriores y se proporciona de forma pública. Su objetivo es ofrecer a desabolladores e investigadores un entorno común para prototipar y verificar nuevas metodologías de cuantificación de forma sencilla. Describimos el flujo de trabajo, justificamos las decisiones de diseño tomadas, explicamos su API pública y hacemos una demostración paso a paso de su funcionamiento. Además mostramos, a través de un ejemplo sencillo, la forma en que conectar nuevas extensiones a la herramienta con las interfaces ya existentes para poder así expandir y mejorar las capacidades de HOPLITE. ABSTRACT Using fixed-point arithmetic is one of the most common design choices for systems where area, power or throughput are heavily constrained. In order to produce implementations where the cost is minimized without negatively impacting the accuracy of the results, a careful assignment of word-lengths is required. The problem of finding the optimal combination of fixed-point word-lengths for a given system is a combinatorial NP-hard problem to which developers devote between 25 and 50% of the design-cycle time. Reconfigurable hardware platforms such as FPGAs also benefit of the advantages of fixed-point arithmetic, as it compensates for the slower clock frequencies and less efficient area utilization of the hardware platform with respect to ASICs. As FPGAs become commonly used for scientific computation, designs constantly grow larger and more complex, up to the point where they cannot be handled efficiently by current signal and quantization noise modelling and word-length optimization methodologies. In this Ph.D. Thesis we explore different aspects of the quantization problem and we present new methodologies for each of them: The techniques based on extensions of intervals have allowed to obtain accurate models of the signal and quantization noise propagation in systems with non-linear operations. We take this approach a step further by introducing elements of MultiElement Generalized Polynomial Chaos (ME-gPC) and combining them with an stateof- the-art Statistical Modified Affine Arithmetic (MAA) based methodology in order to model systems that contain control-flow structures. Our methodology produces the different execution paths automatically, determines the regions of the input domain that will exercise them, and extracts the system statistical moments from the partial results. We use this technique to estimate both the dynamic range and the round-off noise in systems with the aforementioned control-flow structures. We show the good accuracy of our approach, which in some case studies with non-linear operators shows a 0.04 % deviation respect to the simulation-based reference values. A known drawback of the techniques based on extensions of intervals is the combinatorial explosion of terms as the size of the targeted systems grows, which leads to scalability problems. To address this issue we present a clustered noise injection technique that groups the signals in the system, introduces the noise terms in each group independently and then combines the results at the end. In this way, the number of noise sources in the system at a given time is controlled and, because of this, the combinato rial explosion is minimized. We also present a multi-way partitioning algorithm aimed at minimizing the deviation of the results due to the loss of correlation between noise terms, in order to keep the results as accurate as possible. This Ph.D. Thesis also covers the development of methodologies for word-length optimization based on Monte-Carlo simulations in reasonable times. We do so by presenting two novel techniques that explore the reduction of the execution times approaching the problem in two different ways: First, the interpolative method applies a simple but precise interpolator to estimate the sensitivity of each signal, which is later used to guide the optimization effort. Second, the incremental method revolves on the fact that, although we strictly need to guarantee a certain confidence level in the simulations for the final results of the optimization process, we can do it with more relaxed levels, which in turn implies using a considerably smaller amount of samples, in the initial stages of the process, when we are still far from the optimized solution. Through these two approaches we demonstrate that the execution time of classical greedy techniques can be accelerated by factors of up to ×240 for small/medium sized problems. Finally, this book introduces HOPLITE, an automated, flexible and modular framework for quantization that includes the implementation of the previous techniques and is provided for public access. The aim is to offer a common ground for developers and researches for prototyping and verifying new techniques for system modelling and word-length optimization easily. We describe its work flow, justifying the taken design decisions, explain its public API and we do a step-by-step demonstration of its execution. We also show, through an example, the way new extensions to the flow should be connected to the existing interfaces in order to expand and improve the capabilities of HOPLITE.

A flexible (C)LP-based approach to the analysis of object-oriented programs

Static analyses of object-oriented programs usually rely on intermediate representations that respect the original semantics while having a more uniform and basic syntax. Most of the work involving object-oriented languages and abstract interpretation usually omits the description of that language or just refers to the Control Flow Graph(CFG) it represents. However, this lack of formalization on one hand results in an absence of assurances regarding the correctness of the transformation and on the other it typically strongly couples the analysis to the source language. In this work we present a framework for analysis of object-oriented languages in which in a first phase we transform the input program into a representation based on Horn clauses. This allows on one hand proving the transformation correct attending to a simple condition and on the other being able to apply an existing analyzer for (constraint) logic programming to automatically derive a safe approximation of the semantics of the original program. The approach is flexible in the sense that the first phase decouples the analyzer from most languagedependent features, and correct because the set of Horn clauses returned by the transformation phase safely approximates the standard semantics of the input program. The resulting analysis is also reasonably scalable due to the use of mature, modular (C)LP-based analyzers. The overall approach allows us to report results for medium-sized programs.

A generic, context sensitive analysis framework for object oriented programs

Abstract interpreters rely on the existence of a nxpoint algorithm that calculates a least upper bound approximation of the semantics of the program. Usually, that algorithm is described in terms of the particular language in study and therefore it is not directly applicable to programs written in a different source language. In this paper we introduce a generic, block-based, and uniform representation of the program control flow graph and a language-independent nxpoint algorithm that can be applied to a variety of languages and, in particular, Java. Two major characteristics of our approach are accuracy (obtained through a topdown, context sensitive approach) and reasonable efficiency (achieved by means of memoization and dependency tracking techniques). We have also implemented the proposed framework and show some initial experimental results for standard benchmarks, which further support the feasibility of the solution adopted.

Effectiveness for Ddtecting faults within and outside the scope of testing techniques: an independent replication

The verification and validation activity plays a fundamental role in improving software quality. Determining which the most effective techniques for carrying out this activity are has been an aspiration of experimental software engineering researchers for years. This paper reports a controlled experiment evaluating the effectiveness of two unit testing techniques (the functional testing technique known as equivalence partitioning (EP) and the control-flow structural testing technique known as branch testing (BT)). This experiment is a literal replication of Juristo et al. (2013).Both experiments serve the purpose of determining whether the effectiveness of BT and EP varies depending on whether or not the faults are visible for the technique (InScope or OutScope, respectively). We have used the materials, design and procedures of the original experiment, but in order to adapt the experiment to the context we have: (1) reduced the number of studied techniques from 3 to 2; (2) assigned subjects to experimental groups by means of stratified randomization to balance the influence of programming experience; (3) localized the experimental materials and (4) adapted the training duration. We ran the replication at the Escuela Politécnica del Ejército Sede Latacunga (ESPEL) as part of a software verification & validation course. The experimental subjects were 23 master?s degree students. EP is more effective than BT at detecting InScope faults. The session/program andgroup variables are found to have significant effects. BT is more effective than EP at detecting OutScope faults. The session/program and group variables have no effect in this case. The results of the replication and the original experiment are similar with respect to testing techniques. There are some inconsistencies with respect to the group factor. They can be explained by small sample effects. The results for the session/program factor are inconsistent for InScope faults.We believe that these differences are due to a combination of the fatigue effect and a technique x program interaction. Although we were able to reproduce the main effects, the changes to the design of the original experiment make it impossible to identify the causes of the discrepancies for sure. We believe that further replications closely resembling the original experiment should be conducted to improve our understanding of the phenomena under study.

A formalism and method for representing and reasoning with process models authored by subject matter experts

Enabling Subject Matter Experts (SMEs) to formulate knowledge without the intervention of Knowledge Engineers (KEs) requires providing SMEs with methods and tools that abstract the underlying knowledge representation and allow them to focus on modeling activities. Bridging the gap between SME-authored models and their representation is challenging, especially in the case of complex knowledge types like processes, where aspects like frame management, data, and control flow need to be addressed. In this paper, we describe how SME-authored process models can be provided with an operational semantics and grounded in a knowledge representation language like F-logic in order to support process-related reasoning. The main results of this work include a formalism for process representation and a mechanism for automatically translating process diagrams into executable code following such formalism. From all the process models authored by SMEs during evaluation 82% were well-formed, all of which executed correctly. Additionally, the two optimizations applied to the code generation mechanism produced a performance improvement at reasoning time of 25% and 30% with respect to the base case, respectively.

Effectiveness for detecting faults within and outside the scope of testing techniques: an independent replication

The verification and validation activity plays a fundamental role in improving software quality. Determining which the most effective techniques for carrying out this activity are has been an aspiration of experimental software engineering researchers for years. This paper reports a controlled experiment evaluating the effectiveness of two unit testing techniques (the functional testing technique known as equivalence partitioning (EP) and the control-flow structural testing technique known as branch testing (BT)). This experiment is a literal replication of Juristo et al. (2013). Both experiments serve the purpose of determining whether the effectiveness of BT and EP varies depending on whether or not the faults are visible for the technique (InScope or OutScope, respectively). We have used the materials, design and procedures of the original experiment, but in order to adapt the experiment to the context we have: (1) reduced the number of studied techniques from 3 to 2; (2) assigned subjects to experimental groups by means of stratified randomization to balance the influence of programming experience; (3) localized the experimental materials and (4) adapted the training duration. We ran the replication at the Escuela Polite?cnica del Eje?rcito Sede Latacunga (ESPEL) as part of a software verification & validation course. The experimental subjects were 23 master?s degree students. EP is more effective than BT at detecting InScope faults. The session/program and group variables are found to have significant effects. BT is more effective than EP at detecting OutScope faults. The session/program and group variables have no effect in this case. The results of the replication and the original experiment are similar with respect to testing techniques. There are some inconsistencies with respect to the group factor. They can be explained by small sample effects. The results for the session/program factor are inconsistent for InScope faults. We believe that these differences are due to a combination of the fatigue effect and a technique x program interaction. Although we were able to reproduce the main effects, the changes to the design of the original experiment make it impossible to identify the causes of the discrepancies for sure. We believe that further replications closely resembling the original experiment should be conducted to improve our understanding of the phenomena under study.

Formal Verification of Temporal Properties for Parametrized Concurrent Programs and Concurrent Data Structures

Los tipos de datos concurrentes son implementaciones concurrentes de las abstracciones de datos clásicas, con la diferencia de que han sido específicamente diseñados para aprovechar el gran paralelismo disponible en las modernas arquitecturas multiprocesador y multinúcleo. La correcta manipulación de los tipos de datos concurrentes resulta esencial para demostrar la completa corrección de los sistemas de software que los utilizan. Una de las mayores dificultades a la hora de diseñar y verificar tipos de datos concurrentes surge de la necesidad de tener que razonar acerca de un número arbitrario de procesos que invocan estos tipos de datos de manera concurrente. Esto requiere considerar sistemas parametrizados. En este trabajo estudiamos la verificación formal de propiedades temporales de sistemas concurrentes parametrizados, poniendo especial énfasis en programas que manipulan estructuras de datos concurrentes. La principal dificultad a la hora de razonar acerca de sistemas concurrentes parametrizados proviene de la interacción entre el gran nivel de concurrencia que éstos poseen y la necesidad de razonar al mismo tiempo acerca de la memoria dinámica. La verificación de sistemas parametrizados resulta en sí un problema desafiante debido a que requiere razonar acerca de estructuras de datos complejas que son accedidas y modificadas por un numero ilimitado de procesos que manipulan de manera simultánea el contenido de la memoria dinámica empleando métodos de sincronización poco estructurados. En este trabajo, presentamos un marco formal basado en métodos deductivos capaz de ocuparse de la verificación de propiedades de safety y liveness de sistemas concurrentes parametrizados que manejan estructuras de datos complejas. Nuestro marco formal incluye reglas de prueba y técnicas especialmente adaptadas para sistemas parametrizados, las cuales trabajan en colaboración con procedimientos de decisión especialmente diseñados para analizar complejas estructuras de datos concurrentes. Un aspecto novedoso de nuestro marco formal es que efectúa una clara diferenciación entre el análisis del flujo de control del programa y el análisis de los datos que se manejan. El flujo de control del programa se analiza utilizando reglas de prueba y técnicas de verificación deductivas especialmente diseñadas para lidiar con sistemas parametrizados. Comenzando a partir de un programa concurrente y la especificación de una propiedad temporal, nuestras técnicas deductivas son capaces de generar un conjunto finito de condiciones de verificación cuya validez implican la satisfacción de dicha especificación temporal por parte de cualquier sistema, sin importar el número de procesos que formen parte del sistema. Las condiciones de verificación generadas se corresponden con los datos manipulados. Estudiamos el diseño de procedimientos de decisión especializados capaces de lidiar con estas condiciones de verificación de manera completamente automática. Investigamos teorías decidibles capaces de describir propiedades de tipos de datos complejos que manipulan punteros, tales como implementaciones imperativas de pilas, colas, listas y skiplists. Para cada una de estas teorías presentamos un procedimiento de decisión y una implementación práctica construida sobre SMT solvers. Estos procedimientos de decisión son finalmente utilizados para verificar de manera automática las condiciones de verificación generadas por nuestras técnicas de verificación parametrizada. Para concluir, demostramos como utilizando nuestro marco formal es posible probar no solo propiedades de safety sino además de liveness en algunas versiones de protocolos de exclusión mutua y programas que manipulan estructuras de datos concurrentes. El enfoque que presentamos en este trabajo resulta ser muy general y puede ser aplicado para verificar un amplio rango de tipos de datos concurrentes similares. Abstract Concurrent data types are concurrent implementations of classical data abstractions, specifically designed to exploit the great deal of parallelism available in modern multiprocessor and multi-core architectures. The correct manipulation of concurrent data types is essential for the overall correctness of the software system built using them. A major difficulty in designing and verifying concurrent data types arises by the need to reason about any number of threads invoking the data type simultaneously, which requires considering parametrized systems. In this work we study the formal verification of temporal properties of parametrized concurrent systems, with a special focus on programs that manipulate concurrent data structures. The main difficulty to reason about concurrent parametrized systems comes from the combination of their inherently high concurrency and the manipulation of dynamic memory. This parametrized verification problem is very challenging, because it requires to reason about complex concurrent data structures being accessed and modified by threads which simultaneously manipulate the heap using unstructured synchronization methods. In this work, we present a formal framework based on deductive methods which is capable of dealing with the verification of safety and liveness properties of concurrent parametrized systems that manipulate complex data structures. Our framework includes special proof rules and techniques adapted for parametrized systems which work in collaboration with specialized decision procedures for complex data structures. A novel aspect of our framework is that it cleanly differentiates the analysis of the program control flow from the analysis of the data being manipulated. The program control flow is analyzed using deductive proof rules and verification techniques specifically designed for coping with parametrized systems. Starting from a concurrent program and a temporal specification, our techniques generate a finite collection of verification conditions whose validity entails the satisfaction of the temporal specification by any client system, in spite of the number of threads. The verification conditions correspond to the data manipulation. We study the design of specialized decision procedures to deal with these verification conditions fully automatically. We investigate decidable theories capable of describing rich properties of complex pointer based data types such as stacks, queues, lists and skiplists. For each of these theories we present a decision procedure, and its practical implementation on top of existing SMT solvers. These decision procedures are ultimately used for automatically verifying the verification conditions generated by our specialized parametrized verification techniques. Finally, we show how using our framework it is possible to prove not only safety but also liveness properties of concurrent versions of some mutual exclusion protocols and programs that manipulate concurrent data structures. The approach we present in this work is very general, and can be applied to verify a wide range of similar concurrent data types.

Performance of pressure control valves and flow meters precision in operational irrigation-water balance accuracy

In pressure irrigation-water distribution networks, pressure regulating devices for controlling the discharged flow rate by irrigation units are needed due to the variability of flow rate. In addition, applied water volume is used controlled operating the valve during a calculated time interval, and assuming constant flow rate. In general, a pressure regulating valve PRV is the commonly used pressure regulating device in a hydrant, which, also, executes the open and close function. A hydrant feeds several irrigation units, requiring a wide range in flow rate. In addition, some flow meters are also available, one as a component of the hydrant and the rest are placed downstream. Every land owner has one flow meter for each group of field plots downstream the hydrant. Its lecture could be used for refining the water balance but its accuracy must be taken into account. Ideal PRV performance would maintain a constant downstream pressure. However, the true performance depends on both upstream pressure and the discharged flow rate. The objective of this work is to asses the influence of the performance on the applied volume during the whole irrigation events in a year. The results of the study have been obtained introducing the flow rate into a PRV model. Variations on flow rate are simulated by taking into account the consequences of variations on climate conditions and also decisions in irrigation operation, such us duration and frequency application. The model comprises continuity, dynamic and energy equations of the components of the PRV.

On the role of global flow instability analysis in closed loop flow control

Control of linear flow instabilities has been demonstrated to be an effective theoretical flow control methodology, capable of modifying transitional flows on canonical geometries such as the plane channel and the flat-plate boundary layer. Extending the well-developed theoretical flow control techniques to flows over or through complex geometries requires addressing the issue of efficient capturing of the leading members of the global eigenspectrum pertinent to such flows. The present contribution describes state-of-the-art modal global instability analysis methodologies recently developed in our group, based on matrix formation and time-stepping, respectively. The relative performance of these algorithms is assessed on the recovery of BiGlobal and TriGlobal eigenspectra in the spanwise periodic and the cubic lid-driven cavity, respectively; the adjoint eigenspectrum in the latter flow is recovered for the first time. For three-dimensional flows without any homogeneous spatial direction, the time-stepping methodology was found to outperform the matrix-forming approach and permit recovering the leading TriGlobal eigenmodes in an three-dimensional open cavity of aspect ratio L : D : W = 5 : 1 : 1; theoretical flow control of this configuration is underway.

On the role of global flow instability analysis in closed loop flow control

Control of linear flow instabilities has been demonstrated to be an effective theoretical flow control methodology, capable of modifying transitional flow on canonical geometries such as the plane channel and the flat-plate boundary layer.

Global instability analysis and control of three-dimensional long open cavity flow

The three-dimensional wall-bounded open cavity may be considered as a simplified geometry found in industrial applications such as leading gear or slotted flats on the airplane. Understanding the three-dimensional complex flow structure that surrounds this particular geometry is therefore of major industrial interest. At the light of the remarkable former investigations in this kind of flows, enough evidences suggest that the lateral walls have a great influence on the flow features and hence on their instability modes. Nevertheless, even though there is a large body of literature on cavity flows, most of them are based on the assumption that the flow is two-dimensional and spanwise-periodic. The flow over realistic open cavity should be considered. This thesis presents an investigation of three-dimensional wall-bounded open cavity with geometric ratio 6:2:1. To this aim, three-dimensional Direct Numerical Simulation (DNS) and global linear instability have been performed. Linear instability analysis reveals that the onset of the first instability in this open cavity is around Recr 1080. The three-dimensional shear layer mode with a complex structure is shown to be the most unstable mode. I t is noteworthy that the flow pattern of this high-frequency shear layer mode is similar to the observed unstable oscillations in supercritical unstable case. DNS of the cavity flow carried out at different Reynolds number from steady state until a nonlinear saturated state is obtained. The comparison of time histories of kinetic energy presents a clearly dominant energetic mode which shifts between low-frequency and highfrequency oscillation. A complete flow patterns from subcritical cases to supercritical case has been put in evidence. The flow structure at the supercritical case Re=1100 resembles typical wake-shedding instability oscillations with a lateral motion existed in the subcritical cases. Also, This flow pattern is similar to the observations in experiments. In order to validate the linear instability analysis results, the topology of the composite flow fields reconstructed by linear superposition of a three-dimensional base flow and its leading three-dimensional global eigenmodes has been studied. The instantaneous wall streamlines of those composited flows display distinguish influence region of each eigenmode. Attention has been focused on the leading high-frequency shear layer mode; the composite flow fields have been fully recognized with respect to the downstream wave shedding. The three-dimensional shear layer mode is shown to give rise to a typical wake-shedding instability with a lateral motions occurring downstream which is in good agreement with the experiment results. Moreover, the spanwise-periodic, open cavity with the same length to depth ratio has been also studied. The most unstable linear mode is different from the real three-dimensional cavity flow, because of the existence of the side walls. Structure sensitivity of the unstable global mode is analyzed in the flow control context. The adjoint-based sensitivity analysis has been employed to localized the receptivity region, where the flow is more sensible to momentum forcing and mass injection. Because of the non-normality of the linearized Navier-Stokes equations, the direct and adjoint field has a large spatial separation. The strongest sensitivity region is locate in the upstream lip of the three-dimensional cavity. This numerical finding is in agreement with experimental observations. Finally, a prototype of passive flow control strategy is applied.

Sistemas de control de roturas en presas y caracterización de sistemas hidráulicos

Este proyecto nace de la necesidad de automatizar el estudio de sistemas hidráulicos y de control de roturas en presas. Para realizar el estudio de sistemas hidráulicos se usarán un número indeterminado de sensores de nivel, presión y caudal. El número de sensores que se pueden utilizar viene determinado por el material disponible. Estos sensores se conectarán a unas tarjetas de National Instruments modelo NI 9208 y éstas a su vez a un chasis modelo CompactDAQ NI-9174 con cuatro ranuras. Conectando este chasis al ordenador podremos obtener los datos provenientes de los sensores. También se podrá controlar una válvula para determinar la cantidad de agua que fluye en nuestro experimento. Está válvula está conectada a una tarjeta NI-9264 que se conectará al chasis en su última posición Para detectar y estudiar posibles roturas en presas se dispone de un motor y un láser con los cuales se puede barrer la superficie de una presa y obtener una imagen en tres dimensiones de la misma procesando los datos provenientes del laser. Para recoger los datos de los sensores y controlar una válvula se ha desarrollado una aplicación utilizando LabVIEW, un programa creado por National Instruments. Para poder controlar el motor y el láser se parte de una aplicación que ya estaba realizada en LabVIEW. El objetivo ha sido detectar y corregir una serie de errores en la misma. Dentro del proyecto, además de la explicación detallada de la aplicación para los sensores y la válvula, y las pruebas realizadas para detectar y corregir los errores de la aplicación del láser y el motor, existe: una breve introducción a la programación en LabVIEW, la descripción de los pasos realizados para el conexionado de los sensores con las tarjetas, los manuales de usuario de las aplicaciones y la descripción de los equipos utilizados. This project stars from the need to automate the study of hydraulic systems and control dam breaks. For the study of hydraulic systems it will be used an unspecified number of level, pressure and flow sensors. The number of sensors that can be used is determined by the available material. These sensors are connected to a NI 9208 National Instruments target and these cards to a NI-9174 CompactDAQ chassis with four slots. Connecting the chassis to a computer we will obtain data from the sensors. We also can control a valve to determine the amount of water flowing in our experiment. This valve is connected to a NI-9264 card and this card to the last position of the chassis. To detect and study dams breakage it used a motor and a laser. With these two devices we can scan the surface of a dam and obtain a three-dimensional image processing data from the laser. To collect data from the sensors and control the valve it has developed an application using LabVIEW, a program created by National Instruments. To control the motor and the laser it is used an application that was already created using LabVIEW. The aim of this part has been detect and correct a number of errors in this application. Within the project, in addition to the detailed explanation of the application for sensors and valve, and tests to detect and correct errors in the application of lasers and the motor, there is: a brief introduction to programming in LabVIEW, the description of the steps taken for connecting the sensors with cards, user manuals and application description of the equipment used.

LED backlight designs with the flow-line method

An LED backlight has been designed using the flow-line design method. This method allows a very efficient control of the light extraction. The light is confined inside the guide by total internal reflection, being extracted only by specially calculated surfaces: the ejectors. Backlight designs presented here have a total optical efficiency of up to 80% (including Fresnel and absorption losses) with an FWHM below 30 degrees. The experimental results of the first prototype are shown.

Comportamiento estructural de tuberías forzadas y blindajes en saltos hidroeléctricos : propuestas de diseño y cálculo

En los últimos años ha aumentado el interés en el desarrollo de proyectos en el ámbito de las centrales hidroeléctricas y en concreto en las centrales reversibles. Estas centrales están diseñadas para grandes caudales y saltos, lo cual conlleva túneles de gran diámetro y alta presión y a menudo son esquemas subterráneos. Por ello, los estudios relativos a revestimientos de túneles en presión y los referentes a los blindajes de acero han cobrado una mayor relevancia. En las décadas de los 60 y 70 se realizó una importante labor de investigación coincidiendo con el desarrollo hidroeléctrico en Europa y Norteamérica, que sin embargo ha quedado sin continuidad hasta esta década, en la que se ha experimentado un impulso debido al desarrollo de nuevos proyectos hidroeléctricos de gran magnitud. La adecuación de los métodos de cálculo de blindajes supone una herramienta imprescindible en el correcto desarrollo técnico de los nuevos proyectos hidroeléctricos, así como para la evaluación de la seguridad de los saltos hidroeléctricos existentes en operación. En la presente Tesis se realiza un análisis del comportamiento estructural de las galerías en presión de saltos hidroeléctricos, así como una discusión y revisión de los métodos de cálculo existentes. En concreto se analizan los siguientes aspectos: •Descripción y comparación de las formulaciones existentes para el cálculo de blindajes tanto a presión exterior como interior. •Aplicación del Método de Elementos Finitos para la modelización y cálculo resistente y frente a inestabilidad de blindajes sometidos a presión exterior. •Análisis de un caso real, en el que se ha producido un fallo estructural en un blindaje sometido a presión exterior. Discusión sobre el comportamiento de blindajes con rigidizadores. Estudio paramétrico de la capacidad resistente y de la estabilidad de los blindajes con rigidizadores. •Estudio del comportamiento diferenciado entre un rigidizador y un conector. •Detalles constructivos y de durabilidad de las galerías en presión. •Desarrollo de una metodología para el cálculo de blindajes y tuberías forzadas a fatiga derivada de las variaciones de presión de la conducción. •Análisis de un caso real de una tubería forzada sometida a procesos de variación de carga, evaluando su seguridad frente a la fatiga. El cálculo de blindajes en galerías forzadas presenta una serie de aspectos complejos, y que no permiten la definición del problema con exactitud, tales como las características del macizo rocoso y su permeabilidad, la determinación del nivel freático, la holgura existente entre el blindaje y el revestimiento del trasdós y sus posibles defectos geométricos. Por estas incertidumbres, el cálculo de blindajes supone una materia compleja y que debe ser abordada desde la cautela y el análisis de otros trabajos y/o análisis realizados con anterioridad. En cualquier caso, debe realizarse un análisis de sensibilidad de los diversos parámetros que intervienen en el cálculo. En esta tesis se han descrito las principales formulaciones de cálculo de blindajes de galerías forzadas sometidas a presión interior y exterior; se ha constatado que existe una gran diversidad y que de su aplicación no se llega a resultados concluyentes. Las formulaciones clásicas utilizadas en el cálculo de blindajes lisos y con rigidizadores sometidos a presión exterior (Amstutz y Jacobsen) no resultan del todo adecuadas ni son de aplicación general. Además, pueden arrojar resultados no conservadores o conducir a un sobredimensionamiento del blindaje en otros casos. En las formulaciones tradicionales de diseño se han tenido en cuenta como imperfecciones la holgura del blindaje y la ovalidad del mismo. En la presente tesis, se han analizado imperfecciones de tipo ondulatorio derivadas de los procesos de soldadura y la existencia de espesores reducidos en zonas de corrosión. En el caso práctico analizado sometido a presión exterior, se ha comprobado el funcionamiento real del blindaje mediante los modelos realizados con elementos finitos. Se desprende que los rigidizadores no han funcionado como tales, puesto que para blindajes lisos se obtienen presiones más bajas de pandeo y para el caso de funcionamiento correcto de los rigidizadores se habría obtenido un coeficiente de seguridad suficiente. Por este motivo, se ha analizado el posible funcionamiento de los rigidizadores, que en determinados casos pueden actuar como conectores. En estos casos deben dimensionarse de forma adecuada las soldaduras para soportar las tensiones entre chapa y conector. Por otra parte, tradicionalmente no se han tenido en cuenta los efectos de fatiga que pueden ocasionar los golpes de ariete y las pulsaciones de presión debidas a la regulación secundaria de la red. En esta tesis se ha establecido un procedimiento de comprobación de tuberías forzadas y blindajes sometidos a procesos de fatiga. Adicionalmente, se ha estudiado el caso real de las tuberías forzadas de una central reversible real (Bolarque II) en funcionamiento de regulación secundaria. Se ha concluido, como en otros casos analizados en la bibliografía, que las pulsaciones derivadas de la regulación secundaria no son significativas como para tener en cuenta la fatiga del acero. Por otra parte, las maniobras de arranque y parada (golpe de ariete) suponen una variación importante de la presión en la conducción. Sin embargo, el moderado número de ciclos permite asegurar la integridad de la tubería frente a fenómenos de fatiga. Nowadays, there is a significant concern in the development of projects in the field of hydroelectric power plants, particularly in the pump-storage projects. These plants are designed for high flow rates and heads, which entails large-diameter tunnels and high pressure ratios), and often as underground schemes. Therefore, this concern has reactivated studies about penstocks and in particular those related to steel liners. During the 1960s and 1970s due to hydropower-engineering development in Europe and North America, a major research effort was done. However, the increasing development of new large-scale hydropower projects has involved a renewed research effort during this decade. The adequacy of steel liner calculation methods is a very important issue in the proper technical development of new hydroelectric projects, and for the safety assessment of existing hydroelectric power plants in operation. In this work, an analysis of the structural behavior of pressure galleries in hydroelectric schemes was carried out. Also, a discussion and a review of existing calculation methods are included. In particular, the following issues have been considered: •Description and comparison of existing formulations for calculating the liner response to both external and internal pressure. •Analysis of an actual case study of a steel liner which failed due to external pressure. •Application of the Finite Element Method to liner modeling and analysis subjected to external pressure. •A parametric study of the shielding with stiffeners and discussion about the behavior of liner with stiffeners. •Constructive aspects and durability of pressure galleries. •Development of a methodology for estimating fatigue effects on penstocks and liners sue to pressure changes. •Analysis of an actual case study of a penstock under varying load and assessment of its safety against fatigue. The project of a hydropower penstock is a complex issue, due to the uncertainties in the definition of the problem data, such as the characteristics of the rock mass and its permeability, the determination of the water table, the existing gap between the steel liner and the concrete of the backfill, the geometric imperfections... Hence, the design and analysis of a steel liner must be addressed cautiously and take into account a review of previous studies performed. Ever, a sensitivity analysis of the various parameters involved in the calculation should be performed. In this work, some of the most relevant formulations for liner design subjected to inside and outside pressure have been studied. As a whole, there is a wide variety and its application does not lead to conclusive results. The classical formulations used in the steel liner calculation either with or without stiffeners under external pressure (Amstutz and Jacobsen) are not entirely adequate Also, those can yield both conservative and non-conservative results in large ranges of application. Traditionally design approaches only considered initial gap and ovality as the most relevant geometric imperfections. Thus, little attention was paid to those caused either by welding or by thickness loss in corroded areas. In the case study analyzed in this thesis, the actual working of the liner under external pressure has been simulated by the Finite Element Method. Results show that the stiffeners have not performed as such, since for unstiffened liner lower buckling pressures are obtained and for proper performance of the stiffeners would give a sufficient safety factor. Hence, it must be pointed out that stiffeners may perform either as such or as connectors. For the latter, welding must be designed to properly withstand stresses between the shell and the stiffener. Likewise, the potential fatigue effects due to both water hammer and pressure pulsations due to secondary regulation of the network have not been considered in many studies. It has been included in this work a procedure for checking penstocks and liners under fatigue processes. Additionally, the penstock fatigue response of an actual pump storage project (Bolarque II, Spain) subjected to secondary control operation has been assessed. As in other cases discussed in the literature, pulsations derived from the secondary control are not significant to account for fatigue of steel. Moreover, the start and stop manoeuvres (water hammer) cause a significant change in penstock pressure. However, the moderate number of cycles ensures the integrity of the penstock against fatigue phenomena.

Home automation controller for a water-flow window

Facing the EU energy efficiency and legal scenarios related to buildings (2010/31 EU directive), new sustainable advanced concepts for envelopes are required. These innovative designs must be able to offer an elevated level of energy efficiency based on a high performance architecture. According to this, smart glazings, and particularly active water-flow glazings, represent a promising alternative to other solar control glazings, since they can reduce the building energy demand avoiding well known drawbacks as high cost, glare problems and high response time that affect to other smart glazings. This kind of glazing, as any other active one, needs to be operated by a control system. In order to operate a water-flow based window, a new controller based on an inexpensive microcontroller board has been developed