Contextualización teórica del acto pedagógico en la enseñanza y el aprendizaje del proyecto arquitectónico: el caso de la E.T.S.A.M.

El taller de proyectos constituye el núcleo de la enseñanza arquitectónica. Estudiar sus procesos educativos en la actualidad implica la contextualización teórica del acto educativo y la revisión histórica de la evolución de su estructura social. Esta estructura, es heredera de la larga tradición del taller donde los maestros de obra, artesanos, arquitectos y artistas, se ocupaban desde siempre de la enseñanza de la construcción, de la artesanía, del diseño arquitectónico y del arte. Los aprendices se sometían a la autoridad de sus maestros y pasaban horas practicando, produciendo y aprendiendo junto a ellos. Con la aparición de las primeras Academias de arte y posteriormente de arquitectura, se evidenció un progresivo interés de los Estados hacía los productos artísticos y arquitectónicos. La consideración de las artes y de la arquitectura como proyecto estatal, supuso la construcción lenta, pero consolidable, de un proyecto educativo paralelo, coexistiendo simultáneamente con los talleres de los maestros, pero sin posibilidad de integración, hasta mucho más tarde. La “teoría”, que es de lo que se ocupaba la academia, con la “práctica” que es lo que se desarrollaba en el taller, no encontraban fácilmente la manera de encajarse y complementarse mutuamente en un proyecto educativo común. Las concepciones educativas de ambos, afrontaban la enseñanza y el aprendizaje desde puntos de vista también diferentes; mientras la Academia representaba el conocimiento validado y explicitado, en el taller se trabajaba con un conocimiento tácito e implícito. En la práctica artística del taller era donde se producía el aprendizaje mientras que en la Academia es donde se validaba. Esta estructura llegó en muchas ocasiones a situaciones extremas, no siendo casual que las más grandes crisis registradas en la historia de la enseñanza de las artes, coincidieran con un aumento de la distancia entre estas dos “instituciones”, talleres y academias. Por otra parte, parece que cualquier proyecto o concepto innovador, se ha fundado sobre la redistribución de estos equilibrios perdidos. En dicho contexto, en el campo de la educación y especialmente en el siglo XX, surge un debate que se estructura en base a los fines de la educación, contemplando dos posturas bien diferenciadas. Una de ellas sostiene como fin primordial de la educación, el desarrollo de la conciencia y la reciprocidad social del individuo. La otra, fija como fin el desarrollo de su singularidad. La búsqueda del equilibrio entre ambas, parte del interés por fomentar el crecimiento de lo que cada ser humano posee de individual, armonizándolo con la unidad orgánica del grupo social al que pertenece (Read 2010, 33). Sobre esta tensión se han basado muchos de los discursos pedagógicos y especialmente los aquí usados. La estructura social en los talleres de proyectos arquitectónicos, presenta hoy día una máxima integración entre las dos instituciones, el taller y la Academia, tanto a nivel del espacio, donde tiene lugar la enseñanza, como a nivel conceptual y pedagógico. Los talleres de proyectos poseen un formato de enseñanza y aprendizaje que constituye un paradigma (Schön, 2008) no solo dentro, sino también fuera del campo arquitectónico. Bajo este formato se complementa el aprendizaje práctico con el teórico y la producción, con la validación del conocimiento. Aunque tal estructura pedagógica presenta importantes variaciones entre unas escuelas de arquitectura y otras, los principales procesos que tienen lugar, son lo suficientemente similares, como para poder ser examinados desde una perspectiva común. Esta investigación, estudia el taller de proyectos desde un aspecto pedagógico, que contempla tanto los discursos educativos, como la historia de la evolución del taller como constructo social. El análisis se estructura sobre los elementos fundantes del acto didáctico: un sujeto que aprende, un sujeto que enseña, un método, la estrategia o procedimiento a través del que se enseña, un contenido y el propio acto docente (Sánchez Cerezo, 1994, 530). Además, se han añadido otros dos elementos que se consideran fundamentales para llevar a cabo el estudio: el contexto de la enseñanza, tanto el tangible como el intangible y la evaluación de la enseñanza y del aprendizaje. El caso de estudio de la presente investigación se sitúa en la Escuela de Arquitectura de Madrid en la actualidad. Sin embargo, no se pretende generar un retrato exacto de esta institución sino utilizarla como ejemplo principal en el desarrollo de los capítulos del método, contenido, acto docente y contexto, en los que también se introducen ejemplos de otras escuelas de arquitectura que amplían los argumentos presentados que constituyen la contextualización teórica del acto pedagógico en los talleres de proyectos arquitectónicos. ABSTRACT Design studio constitutes the core of architectural education. To study its current educational processes involves a theoretical approach of its educational praxis and an historic revision of how its social structure evolved. This structure is inherited from the long tradition of the workshop in which master masons, craftsmen, architects and artists have always been in charge of teaching construction, crafts, architectural design and art. Apprentices were subjected to the authority of their teachers and spent hours practicing, producing and learning along with them. With the establishment of the first Academies of Art and later of Architecture, the interest of the State in artistic and architectural products started growing. The understanding of arts and architecture as a state project entailed the slow, but robust development of a parallel education project. This project coexisted with the masters’ workshops, without the possibility of integration between two, until much later. It was difficult to find a way to synthesize academic “theory” with workshop “practice”. The workshops’ and the Academy's conception about teaching and learning differed significantly. While the Academy represented a verified and explicit knowledge, the workshop worked with a tacit and implicit knowledge. The workshops produced education through artistic practice, while the the Academy organized and verified knowledge. This dual framework has on occasions reached extremes. It is no accident that the biggest known crises in the history of arts education coincide with an increase in the distance between these two "institutions", the workshops and Academies. Furthermore, it seems that most innovative concepts or projects have been founded on restoring the lost balance between the two. In this context, in the field of education, and especially during the 20th century, a debate that contemplated the purpose of education and resulted in two quite differentiated approaches, emerged,. One position claims as the primary purpose of education the development of social awareness and mutuality in individuals. The other approach sets as a purpose developing each student's uniqueness. The quest for the right balance between these two positions is based on the assumption that the general purpose of education is to foster the growth of what is individual in each human being, at the same time harmonizing the individuality thus educed with the organic unity of the social group to which the individual belongs (Read, 2010, 33). This tension forms the basis for many pedagogical discourses, especially the ones utilized in this dissertation. The social structure of architecture studios today demonstrates a very high level of integration between the two institutions, the workshop and the Academy, both in terms of space —where the teaching takes place— as well as on a conceptual and pedagogical level. Architecture studios today have developed a format for teaching and learning that has established a paradigm (Schön, 2008) , not only in architecture, but also in other fields. Under this paradigm, practical and theoretical learning, as well as production and verification of knowledge, complement each other. And although this pedagogical structure presents important variations among different schools of architecture, the principal processes that take place in the studio are sufficiently similar so as to be examined from a common perspective. This research examines the architecture studio from a pedagogical point of view, that takes into account both the educational discourses, as well as the historical evolution of the workshop as a social structure. The analysis presented here is structured on the fundamentals of the teaching act: an individual learning, an individual teaching, a method, strategy or procedure for teaching and learning, the content and the teaching act itself (Sánchez Cerezo, 1994, 530). Two extra elements that were considered essential for carrying out this study have also been added: the context in which teaching takes place, tangible as well as intangible, and the evaluation of teaching and learning. The Madrid School of Architecture in the present day served as a case study. However the aim is not to generate an accurate portrayal of this school but to use it as the principal example for the development of the chapters of method, content, teaching act and context. In addition to that, examples from other schools of architecture are introduced in order to further the presented arguments that constitute the theoretical contextualization of the pedagogical act in architecture studios.

Improved static analysis and verification of energy consumption and other resources via abstract interpretation

Resource analysis aims at inferring the cost of executing programs for any possible input, in terms of a given resource, such as the traditional execution steps, time ormemory, and, more recently energy consumption or user defined resources (e.g., number of bits sent over a socket, number of database accesses, number of calls to particular procedures, etc.). This is performed statically, i.e., without actually running the programs. Resource usage information is useful for a variety of optimization and verification applications, as well as for guiding software design. For example, programmers can use such information to choose different algorithmic solutions to a problem; program transformation systems can use cost information to choose between alternative transformations; parallelizing compilers can use cost estimates for granularity control, which tries to balance the overheads of task creation and manipulation against the benefits of parallelization. In this thesis we have significatively improved an existing prototype implementation for resource usage analysis based on abstract interpretation, addressing a number of relevant challenges and overcoming many limitations it presented. The goal of that prototype was to show the viability of casting the resource analysis as an abstract domain, and howit could overcome important limitations of the state-of-the-art resource usage analysis tools. For this purpose, it was implemented as an abstract domain in the abstract interpretation framework of the CiaoPP system, PLAI.We have improved both the design and implementation of the prototype, for eventually allowing an evolution of the tool to the industrial application level. The abstract operations of such tool heavily depend on the setting up and finding closed-form solutions of recurrence relations representing the resource usage behavior of program components and the whole program as well. While there exist many tools, such as Computer Algebra Systems (CAS) and libraries able to find closed-form solutions for some types of recurrences, none of them alone is able to handle all the types of recurrences arising during program analysis. In addition, there are some types of recurrences that cannot be solved by any existing tool. This clearly constitutes a bottleneck for this kind of resource usage analysis. Thus, one of the major challenges we have addressed in this thesis is the design and development of a novel modular framework for solving recurrence relations, able to combine and take advantage of the results of existing solvers. Additionally, we have developed and integrated into our novel solver a technique for finding upper-bound closed-form solutions of a special class of recurrence relations that arise during the analysis of programs with accumulating parameters. Finally, we have integrated the improved resource analysis into the CiaoPP general framework for resource usage verification, and specialized the framework for verifying energy consumption specifications of embedded imperative programs in a real application, showing the usefulness and practicality of the resulting tool.---ABSTRACT---El Análisis de recursos tiene como objetivo inferir el coste de la ejecución de programas para cualquier entrada posible, en términos de algún recurso determinado, como pasos de ejecución, tiempo o memoria, y, más recientemente, el consumo de energía o recursos definidos por el usuario (por ejemplo, número de bits enviados a través de un socket, el número de accesos a una base de datos, cantidad de llamadas a determinados procedimientos, etc.). Ello se realiza estáticamente, es decir, sin necesidad de ejecutar los programas. La información sobre el uso de recursos resulta muy útil para una gran variedad de aplicaciones de optimización y verificación de programas, así como para asistir en el diseño de los mismos. Por ejemplo, los programadores pueden utilizar dicha información para elegir diferentes soluciones algorítmicas a un problema; los sistemas de transformación de programas pueden utilizar la información de coste para elegir entre transformaciones alternativas; los compiladores paralelizantes pueden utilizar las estimaciones de coste para realizar control de granularidad, el cual trata de equilibrar el coste debido a la creación y gestión de tareas, con los beneficios de la paralelización. En esta tesis hemos mejorado de manera significativa la implementación de un prototipo existente para el análisis del uso de recursos basado en interpretación abstracta, abordando diversos desafíos relevantes y superando numerosas limitaciones que éste presentaba. El objetivo de dicho prototipo era mostrar la viabilidad de definir el análisis de recursos como un dominio abstracto, y cómo se podían superar las limitaciones de otras herramientas similares que constituyen el estado del arte. Para ello, se implementó como un dominio abstracto en el marco de interpretación abstracta presente en el sistema CiaoPP, PLAI. Hemos mejorado tanto el diseño como la implementación del mencionado prototipo para posibilitar su evolución hacia una herramienta utilizable en el ámbito industrial. Las operaciones abstractas de dicha herramienta dependen en gran medida de la generación, y posterior búsqueda de soluciones en forma cerrada, de relaciones recurrentes, las cuales modelizan el comportamiento, respecto al consumo de recursos, de los componentes del programa y del programa completo. Si bien existen actualmente muchas herramientas capaces de encontrar soluciones en forma cerrada para ciertos tipos de recurrencias, tales como Sistemas de Computación Algebraicos (CAS) y librerías de programación, ninguna de dichas herramientas es capaz de tratar, por sí sola, todos los tipos de recurrencias que surgen durante el análisis de recursos. Existen incluso recurrencias que no las puede resolver ninguna herramienta actual. Esto constituye claramente un cuello de botella para este tipo de análisis del uso de recursos. Por lo tanto, uno de los principales desafíos que hemos abordado en esta tesis es el diseño y desarrollo de un novedoso marco modular para la resolución de relaciones recurrentes, combinando y aprovechando los resultados de resolutores existentes. Además de ello, hemos desarrollado e integrado en nuestro nuevo resolutor una técnica para la obtención de cotas superiores en forma cerrada de una clase característica de relaciones recurrentes que surgen durante el análisis de programas lógicos con parámetros de acumulación. Finalmente, hemos integrado el nuevo análisis de recursos con el marco general para verificación de recursos de CiaoPP, y hemos instanciado dicho marco para la verificación de especificaciones sobre el consumo de energía de programas imperativas embarcados, mostrando la viabilidad y utilidad de la herramienta resultante en una aplicación real.

Robust Image Registration with Global Intensity Transformation

This paper presents a registration method for images with global illumination variations. The method is based on a joint iterative optimization (geometric and photometric) of the L1 norm of the intensity error. Two strategies are compared to directly find the appropriate intensity transformation within each iteration: histogram specification and the solution obtained by analyzing the necessary optimality conditions. Such strategies reduce the search space of the joint optimization to that of the geometric transformation between the images.

New experiments on speaker diarization for unsupervised speaking style voice building for speech synthesis

El uso universal de síntesis de voz en diferentes aplicaciones requeriría un desarrollo sencillo de las nuevas voces con poca intervención manual. Teniendo en cuenta la cantidad de datos multimedia disponibles en Internet y los medios de comunicación, un objetivo interesante es el desarrollo de herramientas y métodos para construir automáticamente las voces de estilo de varios de ellos. En un trabajo anterior se esbozó una metodología para la construcción de este tipo de herramientas, y se presentaron experimentos preliminares con una base de datos multiestilo. En este artículo investigamos más a fondo esta tarea y proponemos varias mejoras basadas en la selección del número apropiado de hablantes iniciales, el uso o no de filtros de reducción de ruido, el uso de la F0 y el uso de un algoritmo de detección de música. Hemos demostrado que el mejor sistema usando un algoritmo de detección de música disminuye el error de precisión 22,36% relativo para el conjunto de desarrollo y 39,64% relativo para el montaje de ensayo en comparación con el sistema base, sin degradar el factor de mérito. La precisión media para el conjunto de prueba es 90.62% desde 76.18% para los reportajes de 99,93% para los informes meteorológicos.

Development of a genre-dependent TTS system with cross-speaker speaking-style transplantation

One of the biggest challenges in speech synthesis is the production of contextually-appropriate naturally sounding synthetic voices. This means that a Text-To-Speech system must be able to analyze a text beyond the sentence limits in order to select, or even modulate, the speaking style according to a broader context. Our current architecture is based on a two-step approach: text genre identification and speaking style synthesis according to the detected discourse genre. For the final implementation, a set of four genres and their corresponding speaking styles were considered: broadcast news, live sport commentaries, interviews and political speeches. In the final TTS evaluation, the four speaking styles were transplanted to the neutral voices of other speakers not included in the training database. When the transplanted styles were compared to the neutral voices, transplantation was significantly preferred and the similarity to the target speaker was as high as 78%.

Histograms of oriented gradients for fast on-board vehicle verification

Histograms of Oriented Gradients (HoGs) provide excellent results in object detection and verification. However, their demanding processing requirements bound their applicability in some critical real-time scenarios, such as for video-based on-board vehicle detection systems. In this work, an efficient HOG configuration for pose-based on-board vehicle verification is proposed, which alleviates both the processing requirements and required feature vector length without reducing classification performance. The impact on classification of some critical configuration and processing parameters is in depth analyzed to propose a baseline efficient descriptor. Based on the analysis of its cells contribution to classification, new view-dependent cell-configuration patterns are proposed, resulting in reduced descriptors which provide an excellent balance between performance and computational requirements, rendering higher verification rates than other works in the literature.

Optimized HOG for on-road video based vehicle verification

Vision-based object detection from a moving platform becomes particularly challenging in the field of advanced driver assistance systems (ADAS). In this context, onboard vision-based vehicle verification strategies become critical, facing challenges derived from the variability of vehicles appearance, illumination, and vehicle speed. In this paper, an optimized HOG configuration for onboard vehicle verification is proposed which not only considers its spatial and orientation resolution, but descriptor processing strategies and classification. An in-depth analysis of the optimal settings for HOG for onboard vehicle verification is presented, in the context of SVM classification with different kernels. In contrast to many existing approaches, the evaluation is realized in a public and heterogeneous database of vehicle and non-vehicle images in different areas of the road, rendering excellent verification rates that outperform other similar approaches in the literature.

Online Learning-based Robust Visual Tracking for Autonomous Landing of Unmanned Aerial Vehicles

Autonomous landing is a challenging and important technology for both military and civilian applications of Unmanned Aerial Vehicles (UAVs). In this paper, we present a novel online adaptive visual tracking algorithm for UAVs to land on an arbitrary field (that can be used as the helipad) autonomously at real-time frame rates of more than twenty frames per second. The integration of low-dimensional subspace representation method, online incremental learning approach and hierarchical tracking strategy allows the autolanding task to overcome the problems generated by the challenging situations such as significant appearance change, variant surrounding illumination, partial helipad occlusion, rapid pose variation, onboard mechanical vibration (no video stabilization), low computational capacity and delayed information communication between UAV and Ground Control Station (GCS). The tracking performance of this presented algorithm is evaluated with aerial images from real autolanding flights using manually- labelled ground truth database. The evaluation results show that this new algorithm is highly robust to track the helipad and accurate enough for closing the vision-based control loop.

Robust Real-time Vision-based Aircraft Tracking From Unmanned Aerial Vehicles.

Aircraft tracking plays a key and important role in the Sense-and-Avoid system of Unmanned Aerial Vehicles (UAVs). This paper presents a novel robust visual tracking algorithm for UAVs in the midair to track an arbitrary aircraft at real-time frame rates, together with a unique evaluation system. This visual algorithm mainly consists of adaptive discriminative visual tracking method, Multiple-Instance (MI) learning approach, Multiple-Classifier (MC) voting mechanism and Multiple-Resolution (MR) representation strategy, that is called Adaptive M3 tracker, i.e. AM3. In this tracker, the importance of test sample has been integrated to improve the tracking stability, accuracy and real-time performances. The experimental results show that this algorithm is more robust, efficient and accurate against the existing state-of-art trackers, overcoming the problems generated by the challenging situations such as obvious appearance change, variant surrounding illumination, partial aircraft occlusion, blur motion, rapid pose variation and onboard mechanical vibration, low computation capacity and delayed information communication between UAVs and Ground Station (GS). To our best knowledge, this is the first work to present this tracker for solving online learning and tracking freewill aircraft/intruder in the UAVs.

Online Learning-based Robust Visual Tracking for Autonomous Landing of Unmanned Aerial Vehicles

Autonomous landing is a challenging and important technology for both military and civilian applications of Unmanned Aerial Vehicles (UAVs). In this paper, we present a novel online adaptive visual tracking algorithm for UAVs to land on an arbitrary field (that can be used as the helipad) autonomously at real-time frame rates of more than twenty frames per second. The integration of low-dimensional subspace representation method, online incremental learning approach and hierarchical tracking strategy allows the autolanding task to overcome the problems generated by the challenging situations such as significant appearance change, variant surrounding illumination, partial helipad occlusion, rapid pose variation, onboard mechanical vibration (no video stabilization), low computational capacity and delayed information communication between UAV and Ground Control Station (GCS). The tracking performance of this presented algorithm is evaluated with aerial images from real autolanding flights using manually- labelled ground truth database. The evaluation results show that this new algorithm is highly robust to track the helipad and accurate enough for closing the vision-based control loop.

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.

A methodology to analyze, design and implement very fast and robust controls of Buck-type converters

La electrónica digital moderna presenta un desafío a los diseñadores de sistemas de potencia. El creciente alto rendimiento de microprocesadores, FPGAs y ASICs necesitan sistemas de alimentación que cumplan con requirimientos dinámicos y estáticos muy estrictos. Específicamente, estas alimentaciones son convertidores DC-DC de baja tensión y alta corriente que necesitan ser diseñados para tener un pequeño rizado de tensión y una pequeña desviación de tensión de salida bajo transitorios de carga de una alta pendiente. Además, dependiendo de la aplicación, se necesita cumplir con otros requerimientos tal y como proveer a la carga con ”Escalado dinámico de tensión”, donde el convertidor necesitar cambiar su tensión de salida tan rápidamente posible sin sobreoscilaciones, o ”Posicionado Adaptativo de la Tensión” donde la tensión de salida se reduce ligeramente cuanto más grande sea la potencia de salida. Por supuesto, desde el punto de vista de la industria, las figuras de mérito de estos convertidores son el coste, la eficiencia y el tamaño/peso. Idealmente, la industria necesita un convertidor que es más barato, más eficiente, más pequeño y que aún así cumpla con los requerimienos dinámicos de la aplicación. En este contexto, varios enfoques para mejorar la figuras de mérito de estos convertidores se han seguido por la industria y la academia tales como mejorar la topología del convertidor, mejorar la tecnología de semiconducores y mejorar el control. En efecto, el control es una parte fundamental en estas aplicaciones ya que un control muy rápido hace que sea más fácil que una determinada topología cumpla con los estrictos requerimientos dinámicos y, consecuentemente, le da al diseñador un margen de libertar más amplio para mejorar el coste, la eficiencia y/o el tamaño del sistema de potencia. En esta tesis, se investiga cómo diseñar e implementar controles muy rápidos para el convertidor tipo Buck. En esta tesis se demuestra que medir la tensión de salida es todo lo que se necesita para lograr una respuesta casi óptima y se propone una guía de diseño unificada para controles que sólo miden la tensión de salida Luego, para asegurar robustez en controles muy rápidos, se proponen un modelado y un análisis de estabilidad muy precisos de convertidores DC-DC que tienen en cuenta circuitería para sensado y elementos parásitos críticos. También, usando este modelado, se propone una algoritmo de optimización que tiene en cuenta las tolerancias de los componentes y sensados distorsionados. Us ando este algoritmo, se comparan controles muy rápidos del estado del arte y su capacidad para lograr una rápida respuesta dinámica se posiciona según el condensador de salida utilizado. Además, se propone una técnica para mejorar la respuesta dinámica de los controladores. Todas las propuestas se han corroborado por extensas simulaciones y prototipos experimentales. Con todo, esta tesis sirve como una metodología para ingenieros para diseñar e implementar controles rápidos y robustos de convertidores tipo Buck. ABSTRACT Modern digital electronics present a challenge to designers of power systems. The increasingly high-performance of microprocessors, FPGAs (Field Programmable Gate Array) and ASICs (Application-Specific Integrated Circuit) require power supplies to comply with very demanding static and dynamic requirements. Specifically, these power supplies are low-voltage/high-current DC-DC converters that need to be designed to exhibit low voltage ripple and low voltage deviation under high slew-rate load transients. Additionally, depending on the application, other requirements need to be met such as to provide to the load ”Dynamic Voltage Scaling” (DVS), where the converter needs to change the output voltage as fast as possible without underdamping, or ”Adaptive Voltage Positioning” (AVP) where the output voltage is slightly reduced the greater the output power. Of course, from the point of view of the industry, the figures of merit of these converters are the cost, efficiency and size/weight. Ideally, the industry needs a converter that is cheaper, more efficient, smaller and that can still meet the dynamic requirements of the application. In this context, several approaches to improve the figures of merit of these power supplies are followed in the industry and academia such as improving the topology of the converter, improving the semiconductor technology and improving the control. Indeed, the control is a fundamental part in these applications as a very fast control makes it easier for the topology to comply with the strict dynamic requirements and, consequently, gives the designer a larger margin of freedom to improve the cost, efficiency and/or size of the power supply. In this thesis, how to design and implement very fast controls for the Buck converter is investigated. This thesis proves that sensing the output voltage is all that is needed to achieve an almost time-optimal response and a unified design guideline for controls that only sense the output voltage is proposed. Then, in order to assure robustness in very fast controls, a very accurate modeling and stability analysis of DC-DC converters is proposed that takes into account sensing networks and critical parasitic elements. Also, using this modeling approach, an optimization algorithm that takes into account tolerances of components and distorted measurements is proposed. With the use of the algorithm, very fast analog controls of the state-of-the-art are compared and their capabilities to achieve a fast dynamic response are positioned de pending on the output capacitor. Additionally, a technique to improve the dynamic response of controllers is also proposed. All the proposals are corroborated by extensive simulations and experimental prototypes. Overall, this thesis serves as a methodology for engineers to design and implement fast and robust controls for Buck-type converters.

Descripción de parámetros glóticos basados en el modelado de los pliegues vocales para la detección de patología de la voz

Las patologías de la voz se han transformado en los últimos tiempos en una problemática social con cierto calado. La contaminación de las ciudades, hábitos como el de fumar, el uso de aparatos de aire acondicionado, etcétera, contribuyen a ello. Esto alcanza más relevancia en profesionales que utilizan su voz de manera frecuente, como, por ejemplo, locutores, cantantes, profesores o teleoperadores. Por todo ello resultan de especial interés las técnicas de ayuda al diagnóstico que son capaces de extraer conclusiones clínicas a partir de una muestra de la voz grabada con un micrófono, frente a otras invasivas que implican la exploración utilizando laringoscopios, fibroscopios o videoendoscopios, técnicas en cualquier caso mucho más molestas para los pacientes al exigir la introducción parcial del instrumental citado por la garganta, en actuaciones consideradas de tipo quirúrgico. Dentro de aquellas técnicas se ha avanzado mucho en un período de tiempo relativamente corto. En lo que se refiere al diagnóstico de patologías, hemos pasado en los últimos quince años de trabajar principalmente con parámetros extraídos de la señal de voz –tanto en el dominio del tiempo como en el de la frecuencia– y con escalas elaboradas con valoraciones subjetivas realizadas por expertos a hacerlo también con parámetros procedentes de estimaciones de la fuente glótica. La importancia de utilizar la fuente glótica reside, a grandes rasgos, en que se trata de una señal vinculada directamente al estado de la estructura laríngea del locutor y también en que está generalmente menos influida por el tracto vocal que la señal de voz. Es conocido que el tracto vocal guarda más relación con el mensaje hablado, y su presencia dificulta el proceso de detección de patología vocal. Estas estimaciones de la fuente glótica han sido obtenidas a través de técnicas de filtrado inverso desarrolladas por nuestro grupo de investigación. Hemos conseguido, además, profundizar en la naturaleza de la señal glótica: somos capaces de descomponerla y relacionarla con parámetros biomecánicos de los propios pliegues vocales, obteniendo estimaciones de elementos como la masa, la pérdida de energía o la elasticidad del cuerpo y de la cubierta del pliegue, entre otros. De las componentes de la fuente glótica surgen también los denominados parámetros biométricos, relacionados con la forma de la señal, que constituyen por sí mismos una firma biométrica del individuo. También trabajaremos con parámetros temporales, relacionados con las diferentes etapas que se observan dentro de la señal glótica durante un ciclo de fonación. Por último, consideraremos parámetros clásicos de perturbación y energía de la señal. En definitiva, contamos ahora con una considerable cantidad de parámetros glóticos que conforman una base estadística multidimensional, destinada a ser capaz de discriminar personas con voces patológicas o disfónicas de aquellas que no presentan patología en la voz o con voces sanas o normofónicas. Esta tesis doctoral se ocupa de varias cuestiones: en primer lugar, es necesario analizar cuidadosamente estos nuevos parámetros, por lo que ofreceremos una completa descripción estadística de los mismos. También estudiaremos cuestiones como la distribución de los parámetros atendiendo a criterios como el de normalidad estadística de los mismos, ocupándonos especialmente de la diferencia entre las distribuciones que presentan sujetos sanos y sujetos con patología vocal. Para todo ello emplearemos diferentes técnicas estadísticas: generación de elementos y diagramas descriptivos, pruebas de normalidad y diversos contrastes de hipótesis, tanto paramétricos como no paramétricos, que considerarán la diferencia entre los grupos de personas sanas y los grupos de personas con alguna patología relacionada con la voz. Además, nos interesa encontrar relaciones estadísticas entre los parámetros, de cara a eliminar posibles redundancias presentes en el modelo, a reducir la dimensionalidad del problema y a establecer un criterio de importancia relativa en los parámetros en cuanto a su capacidad discriminante para el criterio patológico/sano. Para ello se aplicarán técnicas estadísticas como la Correlación Lineal Bivariada y el Análisis Factorial basado en Componentes Principales. Por último, utilizaremos la conocida técnica de clasificación Análisis Discriminante, aplicada a diferentes combinaciones de parámetros y de factores, para determinar cuáles de ellas son las que ofrecen tasas de acierto más prometedoras. Para llevar a cabo la experimentación se ha utilizado una base de datos equilibrada y robusta formada por doscientos sujetos, cien de ellos pertenecientes al género femenino y los restantes cien al género masculino, con una proporción también equilibrada entre los sujetos que presentan patología vocal y aquellos que no la presentan. Una de las aplicaciones informáticas diseñada para llevar a cabo la recogida de muestras también es presentada en esta tesis. Los distintos estudios estadísticos realizados nos permitirán identificar aquellos parámetros que tienen una mayor contribución a la hora de detectar la presencia de patología vocal. Alguno de los estudios, además, nos permitirá presentar una ordenación de los parámetros en base a su importancia para realizar la detección. Por otra parte, también concluiremos que en ocasiones es conveniente realizar una reducción de la dimensionalidad de los parámetros para mejorar las tasas de detección. Por fin, las propias tasas de detección constituyen quizá la conclusión más importante del trabajo. Todos los análisis presentes en el trabajo serán realizados para cada uno de los dos géneros, de acuerdo con diversos estudios previos que demuestran que los géneros masculino y femenino deben tratarse de forma independiente debido a las diferencias orgánicas observadas entre ambos. Sin embargo, en lo referente a la detección de patología vocal contemplaremos también la posibilidad de trabajar con la base de datos unificada, comprobando que las tasas de acierto son también elevadas. Abstract Voice pathologies have become recently in a social problem that has reached a certain concern. Pollution in cities, smoking habits, air conditioning, etc. contributes to it. This problem is more relevant for professionals who use their voice frequently: speakers, singers, teachers, actors, telemarketers, etc. Therefore techniques that are capable of drawing conclusions from a sample of the recorded voice are of particular interest for the diagnosis as opposed to other invasive ones, involving exploration by laryngoscopes, fiber scopes or video endoscopes, which are techniques much less comfortable for patients. Voice quality analysis has come a long way in a relatively short period of time. In regard to the diagnosis of diseases, we have gone in the last fifteen years from working primarily with parameters extracted from the voice signal (both in time and frequency domains) and with scales drawn from subjective assessments by experts to produce more accurate evaluations with estimates derived from the glottal source. The importance of using the glottal source resides broadly in that this signal is linked to the state of the speaker's laryngeal structure. Unlike the voice signal (phonated speech) the glottal source, if conveniently reconstructed using adaptive lattices, may be less influenced by the vocal tract. As it is well known the vocal tract is related to the articulation of the spoken message and its influence complicates the process of voice pathology detection, unlike when using the reconstructed glottal source, where vocal tract influence has been almost completely removed. The estimates of the glottal source have been obtained through inverse filtering techniques developed by our research group. We have also deepened into the nature of the glottal signal, dissecting it and relating it to the biomechanical parameters of the vocal folds, obtaining several estimates of items such as mass, loss or elasticity of cover and body of the vocal fold, among others. From the components of the glottal source also arise the so-called biometric parameters, related to the shape of the signal, which are themselves a biometric signature of the individual. We will also work with temporal parameters related to the different stages that are observed in the glottal signal during a cycle of phonation. Finally, we will take into consideration classical perturbation and energy parameters. In short, we have now a considerable amount of glottal parameters in a multidimensional statistical basis, designed to be able to discriminate people with pathologic or dysphonic voices from those who do not show pathology. This thesis addresses several issues: first, a careful analysis of these new parameters is required, so we will offer a complete statistical description of them. We will also discuss issues such as distribution of the parameters, considering criteria such as their statistical normality. We will take special care in the analysis of the difference between distributions from healthy subjects and the distributions from pathological subjects. To reach these goals we will use different statistical techniques such as: generation of descriptive items and diagramas, tests for normality and hypothesis testing, both parametric and nonparametric. These latter techniques consider the difference between the groups of healthy subjects and groups of people with an illness related to voice. In addition, we are interested in finding statistical relationships between parameters. There are various reasons behind that: eliminate possible redundancies in the model, reduce the dimensionality of the problem and establish a criterion of relative importance in the parameters. The latter reason will be done in terms of discriminatory power for the criterion pathological/healthy. To this end, statistical techniques such as Bivariate Linear Correlation and Factor Analysis based on Principal Components will be applied. Finally, we will use the well-known technique of Discriminant Analysis classification applied to different combinations of parameters and factors to determine which of these combinations offers more promising success rates. To perform the experiments we have used a balanced and robust database, consisting of two hundred speakers, one hundred of them males and one hundred females. We have also used a well-balanced proportion where subjects with vocal pathology as well as subjects who don´t have a vocal pathology are equally represented. A computer application designed to carry out the collection of samples is also presented in this thesis. The different statistical analyses performed will allow us to determine which parameters contribute in a more decisive way in the detection of vocal pathology. Therefore, some of the analyses will even allow us to present a ranking of the parameters based on their importance for the detection of vocal pathology. On the other hand, we will also conclude that it is sometimes desirable to perform a dimensionality reduction in order to improve the detection rates. Finally, detection rates themselves are perhaps the most important conclusion of the work. All the analyses presented in this work have been performed for each of the two genders in agreement with previous studies showing that male and female genders should be treated independently, due to the observed functional differences between them. However, with regard to the detection of vocal pathology we will consider the possibility of working with the unified database, ensuring that the success rates obtained are also high.

Desarrollo de un método estadístico para la generación de escenarios climáticos de alta resolución a partir de simulaciones de baja resolución de Modelos de Circulación General: aplicación a España

Esta tesis doctoral presenta el desarrollo, verificación y aplicación de un método original de regionalización estadística para generar escenarios locales de clima futuro de temperatura y precipitación diarias, que combina dos pasos. El primer paso es un método de análogos: los "n" días cuya configuración atmosférica de baja resolución es más parecida a la del día problema, se seleccionan de un banco de datos de referencia del pasado. En el segundo paso, se realiza un análisis de regresión múltiple sobre los "n" días más análogos para la temperatura, mientras que para la precipitación se utiliza la distribución de probabilidad de esos "n" días análogos para obtener la estima de precipitación. La verificación de este método se ha llevado a cabo para la España peninsular y las Islas Baleares. Los resultados muestran unas buenas prestaciones para temperatura (BIAS cerca de 0.1ºC y media de errores absolutos alrededor de 1.9ºC); y unas prestaciones aceptables para la precipitación (BIAS razonablemente bajo con una media de -18%; error medio absoluto menor que para una simulación de referencia (la persistencia); y una distribución de probabilidad simulada similar a la observada según dos test no-paramétricos de similitud). Para mostrar la aplicabilidad de la metodología desarrollada, se ha aplicado en detalle en un caso de estudio. El método se aplicó a cuatro modelos climáticos bajo diferentes escenarios futuros de emisiones de gases de efecto invernadero, para la región de Aragón, produciendo así proyecciones futuras de precipitación y temperaturas máximas y mínimas diarias. La fiabilidad de la técnica de regionalización fue evaluada de nuevo para el caso de estudio mediante un proceso de verificación. Para determinar la capacidad de los modelos climáticos para simular el clima real, sus simulaciones del pasado (la denominada salida 20C3M) se regionalizaron y luego se compararon con el clima observado (los resultados son bastante robustos para la temperatura y menos concluyentes para la precipitación). Las proyecciones futuras a escala local presentan un aumento significativo durante todo el siglo XXI de las temperaturas máximas y mínimas para todos los futuros escenarios de emisiones considerados. Las simulaciones de precipitación presentan mayores incertidumbres. Además, la aplicabilidad práctica del método se demostró también mediante su utilización para producir escenarios climáticos futuros para otros casos de estudio en los distintos sectores y regiones del mundo. Se ha prestado especial atención a una aplicación en Centroamérica, una región que ya está sufriendo importantes impactos del cambio climático y que tiene un clima muy diferente. ABSTRACT This doctoral thesis presents the development, verification and application of an original downscaling method for daily temperature and precipitation, which combines two statistical approaches. The first step is an analogue approach: the “n” days most similar to the day to be downscaled are selected. In the second step, a multiple regression analysis using the “n” most analogous days is performed for temperature, whereas for precipitation the probability distribution of the “n” analogous days is used to obtain the amount of precipitation. Verification of this method has been carried out for the Spanish Iberian Peninsula and the Balearic Islands. Results show good performance for temperature (BIAS close to 0.1ºC and Mean Absolute Errors around 1.9ºC); and an acceptable skill for precipitation (reasonably low BIAS with a mean of - 18%, Mean Absolute Error lower than for a reference simulation, i.e. persistence, and a well-simulated probability distribution according to two non-parametric tests of similarity). To show the applicability of the method, a study case has been analyzed. The method was applied to four climate models under different future emission scenarios for the region of Aragón, thus producing future projections of daily precipitation and maximum and minimum temperatures. The reliability of the downscaling technique was re-assessed for the study case by a verification process. To determine the ability of the climate models to simulate the real climate, their simulations of the past (the 20C3M output) were downscaled and then compared with the observed climate – the results are quite robust for temperature and less conclusive for the precipitation. The downscaled future projections exhibit a significant increase during the entire 21st century of the maximum and minimum temperatures for all the considered future emission scenarios. Precipitation simulations exhibit greater uncertainties. Furthermore, the practical applicability of the method was demonstrated also by using it to produce future climate scenarios for some other study cases in different sectors and regions of the world. Special attention was paid to an application of the method in Central America, a region that is already suffering from significant climate change impacts and that has a very different climate from others where the method was previously applied.

An Evening with Dr. Venus Opal Reese, Motivational Speaker, Business Woman, and Author

This Droppin' Knowledge Lecture Series will challenge the audience to "defy the impossible". Dr. Venus Opal Reese will offer insight on how to achieve success on Thursday, September 17, at 6:30pm in Martin Luther King Hall-Thomas Pawley Theature, 812 E. Dunklin Street. Reese, an inspirational speaker, business mentor and marketing strategist, offers training to professionals, particularly entrepreneurs and executives, on how to "defy their impossible" to reach million-dollar success. Reese has consulted for O Magazines, and appeared on ABC and CBS News. For more information on Dr. Venus Opal Reese, please visit http://defyimpossible.com.