Cognitive strategies for reducing energy consumption in wireless sensor networks

El consumo energético de las Redes de Sensores Inalámbricas (WSNs por sus siglas en inglés) es un problema histórico que ha sido abordado desde diferentes niveles y visiones, ya que no solo afecta a la propia supervivencia de la red sino que el creciente uso de dispositivos inteligentes y el nuevo paradigma del Internet de las Cosas hace que las WSNs tengan cada vez una mayor influencia en la huella energética. Debido a la tendencia al alza en el uso de estas redes se añade un nuevo problema, la saturación espectral. Las WSNs operan habitualmente en bandas sin licencia como son las bandas Industrial, Científica y Médica (ISM por sus siglas en inglés). Estas bandas se comparten con otro tipo de redes como Wi-Fi o Bluetooth cuyo uso ha crecido exponencialmente en los últimos años. Para abordar este problema aparece el paradigma de la Radio Cognitiva (CR), una tecnología que permite el acceso oportunista al espectro. La introducción de capacidades cognitivas en las WSNs no solo permite optimizar su eficiencia espectral sino que también tiene un impacto positivo en parámetros como la calidad de servicio, la seguridad o el consumo energético. Sin embargo, por otra parte, este nuevo paradigma plantea algunos retos relacionados con el consumo energético. Concretamente, el sensado del espectro, la colaboración entre los nodos (que requiere comunicación adicional) y el cambio en los parámetros de transmisión aumentan el consumo respecto a las WSN clásicas. Teniendo en cuenta que la investigación en el campo del consumo energético ha sido ampliamente abordada puesto que se trata de una de sus principales limitaciones, asumimos que las nuevas estrategias deben surgir de las nuevas capacidades añadidas por las redes cognitivas. Por otro lado, a la hora de diseñar estrategias de optimización para CWSN hay que tener muy presentes las limitaciones de recursos de estas redes en cuanto a memoria, computación y consumo energético de los nodos. En esta tesis doctoral proponemos dos estrategias de reducción de consumo energético en CWSNs basadas en tres pilares fundamentales. El primero son las capacidades cognitivas añadidas a las WSNs que proporcionan la posibilidad de adaptar los parámetros de transmisión en función del espectro disponible. La segunda es la colaboración, como característica intrínseca de las CWSNs. Finalmente, el tercer pilar de este trabajo es teoría de juegos como algoritmo de soporte a la decisión, ampliamente utilizado en WSNs debido a su simplicidad. Como primer aporte de la tesis se presenta un análisis completo de las posibilidades introducidas por la radio cognitiva en materia de reducción de consumo para WSNs. Gracias a las conclusiones extraídas de este análisis, se han planteado las hipótesis de esta tesis relacionadas con la validez de usar capacidades cognitivas como herramienta para la reducción de consumo en CWSNs. Una vez presentada las hipótesis, pasamos a desarrollar las principales contribuciones de la tesis: las dos estrategias diseñadas para reducción de consumo basadas en teoría de juegos y CR. La primera de ellas hace uso de un juego no cooperativo que se juega mediante pares de jugadores. En la segunda estrategia, aunque el juego continúa siendo no cooperativo, se añade el concepto de colaboración. Para cada una de las estrategias se presenta el modelo del juego, el análisis formal de equilibrios y óptimos y la descripción de la estrategia completa donde se incluye la interacción entre nodos. Con el propósito de probar las estrategias mediante simulación e implementación en dispositivos reales hemos desarrollado un marco de pruebas compuesto por un simulador cognitivo y un banco de pruebas formado por nodos cognitivos capaces de comunicarse en tres bandas ISM desarrollados en el B105 Lab. Este marco de pruebas constituye otra de las aportaciones de la tesis que permitirá el avance en la investigación en el área de las CWSNs. Finalmente, se presentan y discuten los resultados derivados de la prueba de las estrategias desarrolladas. La primera estrategia proporciona ahorros de energía mayores al 65% comparados con una WSN sin capacidades cognitivas y alrededor del 25% si la comparamos con una estrategia cognitiva basada en el sensado periódico del espectro para el cambio de canal de acuerdo a un nivel de ruido fijado. Este algoritmo se comporta de forma similar independientemente del nivel de ruido siempre que éste sea espacialmente uniformemente. Esta estrategia, a pesar de su sencillez, nos asegura el comportamiento óptimo en cuanto a consumo energético debido a la utilización de teoría de juegos en la fase de diseño del comportamiento de los nodos. La estrategia colaborativa presenta mejoras respecto a la anterior en términos de protección frente al ruido en escenarios de ruido más complejos donde aporta una mejora del 50% comparada con la estrategia anterior. ABSTRACT Energy consumption in Wireless Sensor Networks (WSNs) is a known historical problem that has been addressed from different areas and on many levels. But this problem should not only be approached from the point of view of their own efficiency for survival. A major portion of communication traffic has migrated to mobile networks and systems. The increased use of smart devices and the introduction of the Internet of Things (IoT) give WSNs a great influence on the carbon footprint. Thus, optimizing the energy consumption of wireless networks could reduce their environmental impact considerably. In recent years, another problem has been added to the equation: spectrum saturation. Wireless Sensor Networks usually operate in unlicensed spectrum bands such as Industrial, Scientific, and Medical (ISM) bands shared with other networks (mainly Wi-Fi and Bluetooth). To address the efficient spectrum utilization problem, Cognitive Radio (CR) has emerged as the key technology that enables opportunistic access to the spectrum. Therefore, the introduction of cognitive capabilities to WSNs allows optimizing their spectral occupation. Cognitive Wireless Sensor Networks (CWSNs) do not only increase the reliability of communications, but they also have a positive impact on parameters such as the Quality of Service (QoS), network security, or energy consumption. These new opportunities introduced by CWSNs unveil a wide field in the energy consumption research area. However, this also implies some challenges. Specifically, the spectrum sensing stage, collaboration among devices (which requires extra communication), and changes in the transmission parameters increase the total energy consumption of the network. When designing CWSN optimization strategies, the fact that WSN nodes are very limited in terms of memory, computational power, or energy consumption has to be considered. Thus, light strategies that require a low computing capacity must be found. Since the field of energy conservation in WSNs has been widely explored, we assume that new strategies could emerge from the new opportunities presented by cognitive networks. In this PhD Thesis, we present two strategies for energy consumption reduction in CWSNs supported by three main pillars. The first pillar is that cognitive capabilities added to the WSN provide the ability to change the transmission parameters according to the spectrum. The second pillar is that the ability to collaborate is a basic characteristic of CWSNs. Finally, the third pillar for this work is the game theory as a decision-making algorithm, which has been widely used in WSNs due to its lightness and simplicity that make it valid to operate in CWSNs. For the development of these strategies, a complete analysis of the possibilities is first carried out by incorporating the cognitive abilities into the network. Once this analysis has been performed, we expose the hypotheses of this thesis related to the use of cognitive capabilities as a useful tool to reduce energy consumption in CWSNs. Once the analyses are exposed, we present the main contribution of this thesis: the two designed strategies for energy consumption reduction based on game theory and cognitive capabilities. The first one is based on a non-cooperative game played between two players in a simple and selfish way. In the second strategy, the concept of collaboration is introduced. Despite the fact that the game used is also a non-cooperative game, the decisions are taken through collaboration. For each strategy, we present the modeled game, the formal analysis of equilibrium and optimum, and the complete strategy describing the interaction between nodes. In order to test the strategies through simulation and implementation in real devices, we have developed a CWSN framework composed by a CWSN simulator based on Castalia and a testbed based on CWSN nodes able to communicate in three different ISM bands. We present and discuss the results derived by the energy optimization strategies. The first strategy brings energy improvement rates of over 65% compared to WSN without cognitive techniques. It also brings energy improvement rates of over 25% compared with sensing strategies for changing channels based on a decision threshold. We have also seen that the algorithm behaves similarly even with significant variations in the level of noise while working in a uniform noise scenario. The collaborative strategy presents improvements respecting the previous strategy in terms of noise protection when the noise scheme is more complex where this strategy shows improvement rates of over 50%.

La transformación de las grandes estaciones europeas con la llegada de la Alta Velocidad. El caso de Atocha

La aparición del tren de alta velocidad en Europa en las últimas décadas del siglo XX supuso el resurgir de un medio de transporte en progresivo declive desde la popularización del automóvil y del avión. La decadencia del ferrocarril había supuesto en muchos casos el abandono, o incluso la demolición, de estaciones históricas y el deterioro de su entorno urbano. Como reacción a esa desatención surgió, también en el último cuarto de siglo, una mayor conciencia social preocupada por la conservación del patrimonio construido del ferrocarril. La necesidad de adaptación de las grandes estaciones de ferrocarril para dar servicio al nuevo sistema de transporte, junto con el interés por poner en valor sus construcciones históricas y su céntrico entorno, ha dado como resultado la realización de importantes transformaciones. El objeto de la presente investigación es el estudio de las transformaciones que han sufrido las grandes estaciones europeas del siglo XIX con la llegada del tren de alta velocidad, profundizando de manera especial en el caso más significativo que tenemos en nuestro país: la estación de Atocha. En el ámbito europeo es donde se localizan los ejemplos más relevantes de estaciones que tuvieron gran trascendencia en el siglo XIX y que ahora, con la llegada de la Alta Velocidad, vuelven a recuperar su grandeza. En España, el crecimiento de la Alta Velocidad en los últimos años ha sido extraordinario, hasta situarse como el segundo país del mundo con más kilómetros de líneas de alta velocidad en operación y, en consecuencia, se ha construido un gran número de estaciones adaptadas a este servicio. El caso más notable es el de la estación de Atocha, que desde la llegada del AVE en 1992 hasta el día de hoy, se ha convertido en uno de los complejos ferroviarios más importantes del mundo. El trabajo parte del estudio de otros referentes europeos, como las Gares de París, la estación de St Pancras en Londres y de otras cinco estaciones del centro de Europa –Amsterdam Centraal, Antwerpen Centraal, Köln Hauptbahnhof, Frankfurt (Main) Hauptbahnhof y la Gare de Strasbourg–, para establecer el marco analítico sobre el que se profundiza con la estación de Atocha. El proceso de transformación de la estación de Atocha se ha gestado a través de una serie de proyectos que han ido configurando la estación hasta el momento actual y planteando la previsión de futuro: el proyecto del Plan General de Madrid, el concurso de ideas para el diseño de la estación, la estación de Cercanías, la estación de Alta Velocidad y Largo Recorrido, la ampliación de esta para separar los flujos por niveles, los Estudios Informativos del Nuevo Complejo Ferroviario de la Estación de Atocha y su primera fase de construcción. Estos siete proyectos son objeto de un análisis en tres niveles: análisis cronológico, análisis funcional y análisis formal. La estación de Atocha fue la primera estación histórica europea en sufrir una gran transformación vinculada a la llegada de la Alta Velocidad. Aporta el entendimiento de la estación como un todo y la intermodalidad como sus principales valores, además de la gran mejora urbana que supuso la «operación Atocha», y adolece de ciertas carencias en su desarrollo comercial, vinculadas en parte a la presencia del jardín tropical, y de un pobre espacio en las salas de embarque para los pasajeros de salidas. La estación de Atocha completa su transformación a partir de su renovación funcional, manteniendo la carga simbólica de su historia. De la confrontación del caso de Atocha con otras importantes estaciones europeas resulta la definición de las principales consecuencias de la llegada de la Alta Velocidad a las grandes terminales europeas y la identificación de los elementos clave en su transformación. Las consecuencias principales son: la potenciación de la intermodalidad con otros medios de transporte, el desarrollo comercial no necesariamente destinado a los usuarios de los servicios ferroviarios, y la puesta en valor de la antigua estación y de su entorno urbano. Por su parte, los elementos clave en la transformación de las grandes estaciones tienen que ver directamente con la separación de flujos, el entendimiento de la estación por niveles, la dotación de nuevos accesos laterales y la construcción de una nueva gran cubierta para los nuevos andenes. La preeminencia de unos elementos sobre otros depende del carácter propio de cada estación y de cada país, de la magnitud de la intervención y, también, de la estructura y composición de los equipos encargados del diseño de la nueva estación. En la actualidad, nos encontramos en un momento interesante respecto a las estaciones de Alta Velocidad. Tras el reciente atentado frustrado en el Thalys que viajaba de Ámsterdam a París, se ha acordado establecer controles de identidad y equipajes en todas las estaciones de la red europea de alta velocidad, lo que implicará modificaciones importantes en las grandes estaciones que, probablemente, tomarán el modelo de la estación de Atocha como referencia. ABSTRACT The emergence of the high speed train in Europe in the last few decades of the 20th century represented the resurgence of a means of transport in progressive decline since the popularization of the car and the airplane. The railway decay brought in many cases the abandonment, or even the demolition, of historical stations and the deterioration of its urban environment. In response to that neglect, a greater social awareness towards the preservation of the railway built heritage raised up, also in the last quarter-century. The need for adaptation of the great railway stations to serve the new transport system, along with the interest in enhancing the historical buildings and its central locations, had resulted in important transformations. The subject of current investigation is the study of the transformations that the great 19th century European stations have experienced with the arrival of the high speed rail, deepening in particular in the most significant case we have in Spain: Atocha railway station. At European level is where the most relevant examples of stations which have had a great significance in the 19th century and now, with the arrival of the high speed train, have regain their greatness, are located. In Spain, the growth of the high speed rail over the past few years has been outstanding. Today is the second country in the world with the longest high speed rail network in operation and, therefore, with a great number of new stations adapted to this service. The most remarkable case is Atocha station. Since the arrival of the AVE in 1992, the station has become one of the world's most important railway hub. The research starts with the study of other European reference points, as the Gares of Paris, St Pancras station in London and five other stations of Central Europe –Amsterdam Centraal, Antwerpen Centraal, Köln Hauptbahnhof, Frankfurt (Main) Hauptbahnhof y la Gare de Strasbourg–, to establish the analytical framework that will be deepen with Atocha station. The transformation process of Atocha station has been created through a number of projects that have forged the station to date and have raised the sights in the future: the project of the General Urban Development Plan, the ideas competition for the station design, the Suburban train station, the High Speed and Long Distance station, its enlargement in order to separate passenger flows in different levels, the 'Masterplans' for the new Atocha transport hub and its first phase of construction. These seven projects are under scrutiny at three levels: chronological analysis, functional analysis and formal analysis. Atocha station was the first European historical station to undergo a great transformation tied to the arrival of the high speed rail. It brings the understanding of the station as a whole and the intermodality as its greatest values, besides the great urban improvement of the 'Atocha operation', and suffers from certain shortcomings in its commercial development, partly linked to the presence of the tropical garden, and from a poor space in the departure lounges. Atocha station completes its transformation on the basis of its functional renewal, keeping the symbolic charge of its history. The confrontation of Atocha case with the great European stations results in the definition of the principal consequences of the high speed rail arrival to the great European terminals and the identification of the key elements in its transformation. The principal consequences are: the empowering of the intermodality with other means of transport, of the commercial development, not necessarily intended for railway services users, and the enhancement of the old station and its urban environment. On the other hand, the key elements in the transformation of the great stations are directly related with the separation of passenger flows, the understanding of the station in different levels, the placement of new lateral accesses and the construction of a new deck over the new platforms. The pre-eminence of some elements over the others depends on the particular nature of each station and each country, on the scale of the intervention and also in the structure and composition of the teams in charge of the new station design. Nowadays, this is an interesting time concerning the high speed rail stations. After the recent foiled terrorist attempt in the Thalys train travelling from Amsterdam to Paris, it was agreed to establish passenger and luggage controls in every European high speed rail station. This will mean important changes in these great stations, which probably will take Atocha station's model as a reference.

Casas de la oligarquía castellana en la Granada del siglo XVI : tipologías, adaptación y contexto urbano, fundamentos para su recuperación

El tema de estudio de esta tesis es el análisis morfológico y cronológico de diez ejemplares emblemáticos de la arquitectura doméstica señorial de la Granada del siglo XVI, analizados en comparación con otros casos de referencia construidos en el mismo período en la propia ciudad, conservados y desaparecidos. También se han tenido en cuenta las principales manifestaciones arquitectónicas de los mayores focos urbanos contemporáneos en el reino de Castilla. El trabajo se ha desarrollado partiendo de la realización de una planimetría precisa y completa de las diez casas documentadas, uniendo al trabajo in situ sobre los datos materiales el estudio de las fuentes de archivo y de la bibliografía especializada existente sobre la materia. El análisis formal de las unidades domésticas ha sido enfocado al estudio tipológico de lo construido, haciendo especial hincapié en las pervivencias andalusíes sobre las cuales los nuevos moradores edificaron o adaptaron sus casas solariegas. En apoyo a las hipótesis presentadas se aporta la documentación arqueológica derivada de las excavaciones realizadas en los solares de las viviendas objeto de análisis, además de los planos de los estados previos a las recientes reformas sufridas por muchos de estos edificios. El análisis comparativo con algunos edificios contemporáneos en los que se ha documentado y estudiado cronológicamente su evolución histórica, ha permitido afianzar las hipótesis de datación y de reconstrucción de la distribución espacial de las fábricas originarias de la época tratada. Los objetivos de la investigación han sido orientados a poner de manifiesto la delicada y compleja transición de la medina nazarí a la ciudad cristiana, tratando también ciertas características multiculturales propias de las técnicas constructivas y de sociedad de la época. Los resultados de este estudio multidisciplinar se han registrado en un mapa de datos creado con el Sistema de Información Geográfico, en el que se han incluido tanto los datos cronológicos como formales, individualizando los ambientes que constituyen las pervivencias medievales y los que se han construido después, aportando sus distintas dataciones. Se ha querido dar respuesta a varios interrogativos: ¿Cómo se adapta la arquitectura castellana al tejido urbano andalusí? ¿Reaprovecha las preexistencias o las elimina en cada momento? ¿De qué modo la ciudad ha ido modificándose hasta configurarse como una ciudad moderna? ¿Cuánto se ha mantenido este patrimonio de casas? ¿Cómo se debería conservar? Se ha tratado de resolver estas cuestiones formulando síntesis gráficas en las que se puede comprender la evolución histórica de las viviendas acontecida a lo largo del siglo XVI, junto con sus transformaciones recientes provocadas por las intervenciones contemporáneas. Asimismo se aporta el estudio de las principales características de las intervenciones acometidas sobre este patrimonio único de viviendas, que por su propia naturaleza es altamente perecedero y necesita que se formulen criterios eficaces y correctos para su mayor conservación. El punto de partida de este trabajo no ha sido solamente el análisis de campo sino también la recopilación y ordenación de los datos procedentes de la bibliografía existente para formular discursos coherentes y precisos sobre la evolución de este tipo de viviendas históricas, cuyos valores son tan expuestos a graves deterioros que su catalogación, documentación y valoración se hacen imprescindibles. Pese a que las diez viviendas incluidas en los capítulos de estudio detallado estén catalogadas en los Planes Especiales de Protección (Albaicín, 1990 y Centro, 2002), sus caracteres formales y sus elementos estructurales y decorativos de valor histórico han sufrido un evidente proceso de expolio o destrucción, hecho grave que esta Tesis quiere reflejar de cara a la deseable futura puesta en valor real de estos edificios así como, indirectamente, de sus ámbitos urbanísticos de pertenencia. ABSTRACT The purpose of this thesis is to study the morphological and chronological characteristics of ten emblematic mansions belonging to the architectural period of the 16th Century in Granada, Spain. These houses are compared with other similar outstanding constructions of the same period that are located in the city, which have either been preserved or disappeared. Also, this study has taken into account the main architectural expressions of greater contemporary urban areas of the Kingdom of Castile. The work carried out began, first of all, by drawing a precise and thorough planimetry of the ten surveyed houses, together with in situ tasks based on physical data, a study of archival data, and the specialized existing bibliography on the subject. The formal analysis of the home units is focused as a typological study of erected buildings, with a special attention on Al Andalus remains over which the new householders constructed or adapted their mansions. The hypotheses brought forward have been supported by the archaeological documentation that had been elaborated during the excavation works of the houses concerned in this study. Moreover, the drawings of the states of the sites, previously to the most recent renovation works many of these buildings have undergone, have been presented. The comparative analysis made with some contemporary buildings, which have been chronologically documented and studied in their historical evolution, has confirmed the dating hypotheses, and that of the reconstruction of the spatial distribution of the original factories the period discussed. The aims of this research have been oriented to bring to light the delicate and complex transition of the town, from the Nasrid period to Christian times. The research has also dealt with some special multicultural characteristics of the constructive techniques, as well as of the society of that period. The results of this multidisciplinary study have been registered on a data map created with the Geographical Information System, which includes both the chronological and formal data. The Medieval settings, and those of later constructions, have been individualised and dated. Several questions have been answered: how the Castilian architecture adapts to the Al Andalus urban design? Have the pre-existing structures been reused or eliminated at each stage? How has the town evolved until becoming a modern city? To which degree this heritage of houses has remained? How should it been preserved? These questions have been approached by means of graphical syntheses in an attempt to bring an understanding of the historical evolution of the houses throughout the 16th Century. But also, this work shows the more recent transformations these structures suffered over the contemporary period. Moreover, there is a study of the main characteristics of interventions over this unique patrimony of housing which by nature is perishable and needs a formulation of correct and efficient criteria for better conservation. The starting point of this work has not only been that of field analysis, but also the gathering and ordering of the existing bibliographical data, in order to formulate coherent and precise statements on the evolution of this type of historical housing. Its treasures are so exposed to severe deterioration that their cataloguing, documentation and appreciation are becoming crucial. Despite the fact that the ten houses considered in the chapters of this detailed study are listed in the special protection plans (Planes Especiales de Protección, Albaicín plan of 1990 and the town centre plan of 2002) their formal characteristics, as well as structural and decorative historical value, have suffered gradual plunders or destruction. This thesis tries to reflect how serious is that matter and the need in the future to give this heritage and the surrounding urban environment, a real value.

Complexity analysis of spontaneous brain activity: effects of depression and antidepressant treatment

Magnetoencephalography (MEG) allows the real-time recording of neural activity and oscillatory activity in distributed neural networks. We applied a non-linear complexity analysis to resting-state neural activity as measured using whole-head MEG. Recordings were obtained from 20 unmedicated patients with major depressive disorder and 19 matched healthy controls. Subsequently, after 6 months of pharmacological treatment with the antidepressant mirtazapine 30 mg/day, patients received a second MEG scan. A measure of the complexity of neural signals, the Lempel–Ziv Complexity (LZC), was derived from the MEG time series. We found that depressed patients showed higher pre-treatment complexity values compared with controls, and that complexity values decreased after 6 months of effective pharmacological treatment, although this effect was statistically significant only in younger patients. The main treatment effect was to recover the tendency observed in controls of a positive correlation between age and complexity values. Importantly, the reduction of complexity with treatment correlated with the degree of clinical symptom remission. We suggest that LZC, a formal measure of neural activity complexity, is sensitive to the dynamic physiological changes observed in depression and may potentially offer an objective marker of depression and its remission after treatment.

Advanced Topics in Resource Analysis: Certification, Incrementality, Concurrency and Array-Sensitivity

El Análisis de Consumo de Recursos o Análisis de Coste trata de aproximar el coste de ejecutar un programa como una función dependiente de sus datos de entrada. A pesar de que existen trabajos previos a esta tesis doctoral que desarrollan potentes marcos para el análisis de coste de programas orientados a objetos, algunos aspectos avanzados, como la eficiencia, la precisión y la fiabilidad de los resultados, todavía deben ser estudiados en profundidad. Esta tesis aborda estos aspectos desde cuatro perspectivas diferentes: (1) Las estructuras de datos compartidas en la memoria del programa son una pesadilla para el análisis estático de programas. Trabajos recientes proponen una serie de condiciones de localidad para poder mantener de forma consistente información sobre los atributos de los objetos almacenados en memoria compartida, reemplazando éstos por variables locales no almacenadas en la memoria compartida. En esta tesis presentamos dos extensiones a estos trabajos: la primera es considerar, no sólo los accesos a los atributos, sino también los accesos a los elementos almacenados en arrays; la segunda se centra en los casos en los que las condiciones de localidad no se cumplen de forma incondicional, para lo cual, proponemos una técnica para encontrar las precondiciones necesarias para garantizar la consistencia de la información acerca de los datos almacenados en memoria. (2) El objetivo del análisis incremental es, dado un programa, los resultados de su análisis y una serie de cambios sobre el programa, obtener los nuevos resultados del análisis de la forma más eficiente posible, evitando reanalizar aquellos fragmentos de código que no se hayan visto afectados por los cambios. Los analizadores actuales todavía leen y analizan el programa completo de forma no incremental. Esta tesis presenta un análisis de coste incremental, que, dado un cambio en el programa, reconstruye la información sobre el coste del programa de todos los métodos afectados por el cambio de forma incremental. Para esto, proponemos (i) un algoritmo multi-dominio y de punto fijo que puede ser utilizado en todos los análisis globales necesarios para inferir el coste, y (ii) una novedosa forma de almacenar las expresiones de coste que nos permite reconstruir de forma incremental únicamente las funciones de coste de aquellos componentes afectados por el cambio. (3) Las garantías de coste obtenidas de forma automática por herramientas de análisis estático no son consideradas totalmente fiables salvo que la implementación de la herramienta o los resultados obtenidos sean verificados formalmente. Llevar a cabo el análisis de estas herramientas es una tarea titánica, ya que se trata de herramientas de gran tamaño y complejidad. En esta tesis nos centramos en el desarrollo de un marco formal para la verificación de las garantías de coste obtenidas por los analizadores en lugar de analizar las herramientas. Hemos implementado esta idea mediante la herramienta COSTA, un analizador de coste para programas Java y KeY, una herramienta de verificación de programas Java. De esta forma, COSTA genera las garantías de coste, mientras que KeY prueba la validez formal de los resultados obtenidos, generando de esta forma garantías de coste verificadas. (4) Hoy en día la concurrencia y los programas distribuidos son clave en el desarrollo de software. Los objetos concurrentes son un modelo de concurrencia asentado para el desarrollo de sistemas concurrentes. En este modelo, los objetos son las unidades de concurrencia y se comunican entre ellos mediante llamadas asíncronas a sus métodos. La distribución de las tareas sugiere que el análisis de coste debe inferir el coste de los diferentes componentes distribuidos por separado. En esta tesis proponemos un análisis de coste sensible a objetos que, utilizando los resultados obtenidos mediante un análisis de apunta-a, mantiene el coste de los diferentes componentes de forma independiente. Abstract Resource Analysis (a.k.a. Cost Analysis) tries to approximate the cost of executing programs as functions on their input data sizes and without actually having to execute the programs. While a powerful resource analysis framework on object-oriented programs existed before this thesis, advanced aspects to improve the efficiency, the accuracy and the reliability of the results of the analysis still need to be further investigated. This thesis tackles this need from the following four different perspectives. (1) Shared mutable data structures are the bane of formal reasoning and static analysis. Analyses which keep track of heap-allocated data are referred to as heap-sensitive. Recent work proposes locality conditions for soundly tracking field accesses by means of ghost non-heap allocated variables. In this thesis we present two extensions to this approach: the first extension is to consider arrays accesses (in addition to object fields), while the second extension focuses on handling cases for which the locality conditions cannot be proven unconditionally by finding aliasing preconditions under which tracking such heap locations is feasible. (2) The aim of incremental analysis is, given a program, its analysis results and a series of changes to the program, to obtain the new analysis results as efficiently as possible and, ideally, without having to (re-)analyze fragments of code that are not affected by the changes. During software development, programs are permanently modified but most analyzers still read and analyze the entire program at once in a non-incremental way. This thesis presents an incremental resource usage analysis which, after a change in the program is made, is able to reconstruct the upper-bounds of all affected methods in an incremental way. To this purpose, we propose (i) a multi-domain incremental fixed-point algorithm which can be used by all global analyses required to infer the cost, and (ii) a novel form of cost summaries that allows us to incrementally reconstruct only those components of cost functions affected by the change. (3) Resource guarantees that are automatically inferred by static analysis tools are generally not considered completely trustworthy, unless the tool implementation or the results are formally verified. Performing full-blown verification of such tools is a daunting task, since they are large and complex. In this thesis we focus on the development of a formal framework for the verification of the resource guarantees obtained by the analyzers, instead of verifying the tools. We have implemented this idea using COSTA, a state-of-the-art cost analyzer for Java programs and KeY, a state-of-the-art verification tool for Java source code. COSTA is able to derive upper-bounds of Java programs while KeY proves the validity of these bounds and provides a certificate. The main contribution of our work is to show that the proposed tools cooperation can be used for automatically producing verified resource guarantees. (4) Distribution and concurrency are today mainstream. Concurrent objects form a well established model for distributed concurrent systems. In this model, objects are the concurrency units that communicate via asynchronous method calls. Distribution suggests that analysis must infer the cost of the diverse distributed components separately. In this thesis we propose a novel object-sensitive cost analysis which, by using the results gathered by a points-to analysis, can keep the cost of the diverse distributed components separate.

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.

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.

Garantía de calidad en Educación Virtual No Formal para Pueblos Indígenas

Este trabajo de investigación presenta un modelo de garantía de calidad en educación Alternativa en modalidad virtual para Pueblos Indígenas del departamento de La Paz, Bolivia. Se plantea el modelo teórico constituido por componentes que emergen de la problemática enunciada, complementado con un análisis comparativo de modelos de calidad en educación virtual y la selección de variables e indicadores. Se da también una descripción del modelo causal explicativo inicial, todo esto utilizando elementos adecuados a las características de Pueblos indígenas del Dpto. de La Paz. Más adelante, se detalla la experiencia de capacitación en TIC’s a dos poblaciones indígenas aplicando el modelo planteado, lo que ha permitido hacer una validación empírica de este. Asimismo, se da a conocer los resultados que arrojaron las encuestas de calidad provenientes de la aplicación del modelo y el llenado correspondiente de las mismas. A partir de estos datos se ha realizado los análisis estadísticos pertinentes para una validación formal del modelo, estructurando una base de datos con la que se logra validar el modelo a través del análisis confirmatorio que conduce a verificar el ajuste de los datos muestrales con el modelo propuesto. ABSTRACT This research presents a model of quality assurance in Alternative education in virtual mode for indigenous communities in the department of La Paz, Bolivia. The theoretical model consisting of components that emerge from the problem expressed, supplemented by a comparative analysis of quality models in virtual education and the selection of variables and indicators arise. It also gives a description of the initial causal explanatory model, all using suited to the characteristics of indigenous communities in the Department of La Paz. Later, the experience of ICT training in two indigenous peoples applying the detailed proposed model, which has allowed for an empirical validation of this. It also discloses the results yielded quality surveys from the application of the model and the corresponding filling them. From these data it was performed statistical analysis relevant to a formal model validation, structuring a database with that achieved validate the model through confirmatory analysis leading to check the setting of the sample data with the model proposed.

Configuración formal de los rosetones románicos de la ciudad de Zamora

La presente tesis estudia los rosetones románicos de la ciudad de Zamora. La elección del tema tiene como objetivo profundizar en el conocimiento de estos elementos ya que la información existente sobre ellos es muy escasa. El análisis de estos rosetones se ha realizado desde una perspectiva globalizadora que abarca aspectos tales como los geográficos, morfológicos, funcionales, compositivos, constructivos, geométricos, ornamentales, otros. Así mismo, para el desarrollo de esta investigación se ha considerado necesario el estudio de temas históricos, estilísticos, simbólicos, religiosos, culturales, etc., que aportan el marco contextual que permiten su mejor entendimiento. El estudio de cada rosetón ha permitido implementar y desarrollar un método de trabajo analítico basado en el estudio particular de una serie de aspectos como los anteriormente mencionados, así como plantear una estrategia que permite la reconstitución gráfica de los rosetones, basándose en un sistema de módulos que facilitan trabajar de acuerdo a las proporciones de los elementos; hecho que permite acercarnos con gran exactitud a la representación del objeto real cuando se carece de medidas. El desarrollo de esta investigación ha llevado a establecer entre otras cosas que la definición de “ventana circular” que se le atribuye a los rosetones románicos no es acertada, puesto que la función que cumplen en el edificio religioso es más bien de carácter simbólico. ABSTRACT This thesis studies the Romanesque rose windows of the Zamora city. The choice of topic is intended to deepen the knowledge of these elements as the existing information about them is very scarce. The analysis of these rose windows was made from a global perspective covering aspects such as geographic, morphological, functional, compositional, construction, geometric, ornamental, other. Also, for the development of this research it was considered necessary to study historical, stylistic, symbolic, religious, cultural issues, etc., that provide the contextual framework that allow for better understanding. The study of each rose windows has allowed implement and develop a method of analytical work based on the particular study a number of issues such as those mentioned above, as well as devise a strategy that allows the graphic reconstitution of the rose windows, based on a system of modules facilitate work according to the proportions of the elements; made with great precision approach allows the representation of the real thing when it lacks measures. The development of this research has led to establish among other things that the definition of "circular window" that is attributed to the Romanesque rose windows is not successful because the role in the religious building is rather symbolic.