Análisis de los efectos de un programa nutricional y de ejercicio físico sobre el perfil lipídico en personas con sobrepeso y obesidad

Introducción. Las enfermedades cardiovasculares (ECV) son la principal causa de muerte en nuestro país. Entre los factores independientes más importantes para el desarrollo de ECV se encuentran en primer lugar las alteraciones del perfil lipídico como el aumento del colesterol total (TC), las lipoproteínas de baja densidad (LDL) y los triglicéridos (TG) y/o la disminución de las lipoproteínas de alta densidad (HDL). Entre las diferentes formas de abordar el problema para prevenir y tratar estas patologías se encuentra la modificación de los hábitos de vida a través de un programa combinado de dieta y ejercicio. La evidencia confirma la efectividad de la primera variable, sin embargo, en el empleo del ejercicio se encuentran discrepancias acerca de cuál es el modo más eficaz para mejorar el perfil lipídico. Objetivo. Estudiar los cambios en las variables del perfil lipídico y los índices lipoproteicos comparando cuatro tipos de intervención que combinan dieta y diferentes modos de ejercicio, así como, analizar otras variables independientes (género, edad y genotipo ApoE) que pueden tener influencia sobre estos cambios. Diseño de la investigación. Los datos analizados en esta tesis forman parte del estudio “PROgramas de Nutrición y Actividad Física para el tratamiento de la obesidad” (PRONAF). Se trata de un estudio clínico desarrollado en España entre el 2008 y el 2011. La metodología del estudio nos permite comparar cuatro tipos de intervención para la pérdida de peso y evaluar su impacto sobre el perfil lipídico. El diseño fue experimental aleatorizado donde a todos los participantes se les sometió a un programa de dieta equilibrada hipocalórica junto a uno de los tres modos de ejercicio (grupo de entrenamiento de fuerza, grupo de entrenamiento de resistencia y grupo de entrenamiento combinado de los modos anteriores; los cuales fueron igualados en volumen e intensidad) o grupo de recomendaciones de actividad física. Las principales variables analizadas en los estudios que comprende esta tesis doctoral fueron: HDL, LDL, TG y TC, los índices derivados de estas y variables de la composición corporal y del entrenamiento. Conclusiones. Los cuatro tipos de intervención mostraron ser favorables para mejorar las variables del perfil lipídico y los índices lipoproteicos, sin diferencias significativas entre ellos. Tras la intervención, los varones mostraron una respuesta más favorable en los cambios del perfil lipídico. El genotipo ApoE2 obtuvo una reducción mayor en la concentración de TG y TC que el genotipo ApoE3 y ApoE4. Por último, los índices lipoproteicos mejoraron tras un programa de pérdida de peso, obteniéndose mayores cambios en el grupo de dieta más entrenamiento aeróbico para los índices ApoB/ApoA-1, TG/HDL y LDL/ApoB. ABSTRACT Introduction. The main cause of death in our country is cardiovascular disease (CVD). The most important independent factors for the development of CVD are the lipid profile alterations: increased total cholesterol (TC), low density lipoprotein (LDL) and triglycerides (TG) and/or decreased high-density lipoprotein (HDL). Among the different approaches to prevent and treat these diseases is modifying the lifestyle combining a diet and exercise program. The evidence confirms the effectiveness of the first variable, however, there is still controversy about the most effective mode of exercise combined with diet to achieve improvements. Objective. To study changes in lipoprotein profile comparing four types of intervention combining diet with different modes of exercise, and to analyze the independent variables (gender, age, and ApoE genotype) that can influence these changes. Research design. The data analized in this thesis are part of the study Nutrition and Physical Activity Programs for Obesity Treatments (the PRONAF study according to its Spanish initials). This is a clinical research carried out in Spain between 2008 and 2011. The aim of this study was to compare four types of intervention to weight loss with diet combining exercise. The design was experimental randomized where all participants were subjected to follow a hypocaloric balanced diet along one of the three modes of exercise (strength training group, resistance training group and combined training group of the above modes, which were matched by volume and intensity) or physical activity recommendations group. The main variables under investigation in this thesis were: HDL, LDL, TG and TC, the lipoprotein ratios, body composition and training variables. Main outcomes. The four types of interventions shown to be favorable to improve the lipid profile and lipoprotein level, with no significant differences between intervention groups. After the intervention, the men showed a more favorable respond in lipid profile changes. The genotype ApoE2 obtained more positive changes in the concentration of TG and TC than ApoE3 and ApoE4 genotype. Last, the lipoprotein ratios improve after weight loss treatment with diet combined different modes exercise. Our results reflected greater changes for E group in apoB/ApoA1, TG/HDL and LDL/ApoB compared within different intervention groups.

El programa ERHIN y la gestión de embalses en áreas con alta precipitación nival = The ERHIN programme and reservoir management in areas of high nival precipitation

El programa de Evaluación Recursos Hídricos procedentes de la Innivación (ERHIN) ha desarrollado un modelo hidrológico con subrutinas que contemplan el proceso de acumulación/fusión de nieve que permite el seguimiento del manto de nieve y su fusión , esencial para la previsión de avenidas en embalses cuyas cuencas vertientes recogen altos porcentajes de precipitación solida. En determinados sectores del territorio español (Pirineos, Cordilleras Cantábrica e Ibérica, Sistema Central y Sierra Nevada) la precipitación nival alcanza valores significativos durante el invierno, que conducen a espesores de nieve persistentes en las cuencas alimentadoras de numerosos embalses y a la fusión rápida de esta nieve en períodos cortos de tiempo, directamente relacionados con la elevación de la isoterma de cero grados en primavera. Estos procesos condicionan la gestión de los mencionados embalses.

Validación de un marco abierto accesible de tercera generación para la integración nativa de productos de apoyo en tecnologías de la información y la comunicación

Las personas con discapacidad a menudo se encuentran con problemas de acceso a las Tecnologías de la Información y la Comunicación (TIC), debido a diseños y desarrollos que no tienen en cuenta sus diferencias funcionales, y en consecuencia se encuentran en riesgo de exclusión social. Cada vez es más común encontrar productos de apoyo que permitan utilizar diferentes tecnologías (ordenadores, Internet, dispositivos móviles), pero muchos de ellos no se encuentran integrados debido a que funcionan esencialmente modificando la plataforma donde están instalados, siendo soluciones de acceso de segunda generación. Más allá del desarrollo de los productos de apoyo, que sin duda ha evolucionado positivamente en los últimos años, cabe resaltar que existe una falta de herramientas y de aproximación holística que ayuden a los desarrolladores y diseñadores hacer las TIC accesibles. Esta tesis doctoral pretende validar la hipótesis de que una metodología holística de desarrollo de aplicaciones y productos de apoyo TIC, llamada Marco Abierto Accesible, facilita el desarrollo y la integración de modo nativo de la accesibilidad en las aplicaciones y productos apoyo, independientemente de la tecnología utilizada, dando lugar a soluciones de acceso de tercera generación que permitan mejorar la utilización de dichas aplicaciones por parte de personas con discapacidad. Este trabajo se ha desarrollado en el marco del proyecto AEGIS (del inglés, open Accessibility Everywhere: Groundwork, Infrastructure, Standards), que fue parcialmente financiado por la Comisión Europea (CE) bajo el VII Programa Marco y tuvo una duración de cuatro años. La metodología para el diseño, desarrollo y validación seguida en esta tesis es una adaptación de dos metodologías de diseño existentes (el Diseño Centrado en el Usuario y el Diseño Orientado a Metas), la implementación del Marco Abierto Accesible y el uso de diferentes técnicas de validación. Además se ha desarrollado un marco metodológico de entrenamiento para minimizar el efecto que tiene la curva de aprendizaje cuando los usuarios prueban por primera vez las soluciones desarrolladas. En esta tesis se presenta el Marco Abierto Accesible aplicado a las TIC en las tres áreas en las que se desarrolla este trabajo: ordenadores, Internet y dispositivos móviles, partiendo de las necesidades y problemas que tienen los usuarios con discapacidad en el uso de las TIC. Diferentes instanciaciones del Marco Abierto Accesible se definen en las tres áreas TIC mencionadas anteriormente y se describen varios ejemplos de sus implementaciones particulares. Los resultados de las evaluaciones de las implementaciones particulares con usuarios finales y expertos, una vez discutidos y contrastados con las hipótesis, sirven para probar la validez del Marco Abierto Accesible para la integración nativa de productos de apoyo en Tecnologías de la Información y la Comunicación. Finalmente, se presentan las líneas de investigación y trabajo futuro en el área de la accesibilidad en las TIC. ABSTRACT People with disabilities often encounter problems of access to Information and Communications Technology (ICT), due to design and developments that do not take into account their functional differences and therefore put them at risk of social exclusion. It is increasingly common to find assistive products that allow to use different technologies (computers, Internet, mobile devices), but many of them are not well integrated because they work essentially modifying the platform where they are installed, beeing the second-generation access solutions. Beyond the assistive product development, which has certainly evolved positively in recent years, it is notable that there is a lack of tools and holistic approach to help developers and designers make accessible ICT. This doctoral thesis aims to validate the hypothesis that a holistic approach to application development and assistive ICT products, called Open Accessibility Framework, facilitates the development and integration of native accessible applications and assistive products, regardless of the technology used, resulting in third-generation access solutions that improve the use of such applications by people with disabilities. This work was developed under the AEGIS project (open Accessibility Everywhere: Groundwork, Infrastructure, Standards), which was partially funded by the European Commission (EC) under the Seventh Framework Programme and lasted four years. The methodology for the design, development and validation followed in this thesis is an adaptation of two existing design methodologies (User Centered Design and Goal Oriented Design), the implementation of the Open Accessibility Framework and the usage of different validation techniques. A training methodological framework ha also been developed to minimize the effect of the learning curve when users first try the solutions developed. This thesis presents the Open Accessibility Framework applied to ICT in three areas in which this work is developed: computers, Internet and mobile devices, based on the needs and problems of the disabled users in the use of ICT. Different instantiations of the Open Accessibility Framework are defined in the three aforementioned ICT areas and various examples of its particular implementations are described. The results of the evaluations of the particular implementations which have been carried with end users and experts, once discussed and contrasted with the hypotheses, have been used to test the validity of the Open Accessibility Framework for the native integration of assistive products in Information and Communications Technology. Finally, the future research lines and future work in the area of ICT accessibility are presented.

Lo material depende de lo ambiental

El artículo profundiza en una serie de aspectos que influyen en la construcción del espacio arquitectónico contemporáneo, desde la sostenibilidad, el uso de la energía verde y las fuentes renovables, hasta el concepto de equilibrio y el balance entre el orden y el desorden asociados con las leyes de la termodinámica y la analogía con la simetría y la asimetría en la naturaleza. La energía y sus flujos podrían determinar diversas formas arquitectónicas. Podría ser interpretada como lugar, contexto o paisaje, también como programa, estructura y material. Su estudio y asociación con el espacio arquitectónico, como se propone en este escrito, permite un mayor entendimiento de los aspectos inmateriales e intangibles que aún permaneciendo ocultos son esenciales en cualquier proceso de diseño. Nociones vinculadas a la teoría de la evolución como es la adaptación al medio pueden abrir un debate sobre la modificación del medio y la fijación de los nuevos límites entre el territorio y la ciudad. Este concepto puede ser también útil para proponer nuevas formas de desarrollo urbano y paisaje. La sostenibilidad se puede asociar con el equilibrio, el balance, y la adaptación al medio y la ecología con el uso de tecnologías de bajo consumo de energía, -Low-Tech-, y el reciclaje, de manera que se pueda fijar de una manera mas eficaz el ciclo de vida de los materiales y los sistemas que aseguren además la flexibilidad en el uso futuro del espacio.

Representación de isostáticas para la mejora del mallado de elementos finitos en sólidos elásticos planos

Uno de los problemas primordiales en el cálculo por elementos finitos ha sido la obtención del mallado óptimo tal que se minimice el error obtenido, pudiendo distinguirse los siguientes procedimientos: - Aumento del número de nudos de la malla, fundamentalmente en las zonas del modelo donde aparece un error mayor. - Incrementando el grado de los polinomios de interpolación en los elementos donde el modelo presenta un error mayor. - Una combinación entre el primer y el segundo procedimiento. Según los trabajos realizados en la tesis doctoral de D. Rubén Martínez Marín1, se llega a la conclusión de que, tras medir el error del mallado por dos procedimientos distintos; los nudos de la malla óptima se sitúan a lo largo de las líneas isostáticas. Lo destacable de este resultado es que se obtiene sin variar el número de nudos iniciales, y sin incrementar el grado de los polinomios de interpolación; es decir, únicamente buscando la posición óptima de los nudos. Así, en el presente documento se plantea la realización de dos cálculos por elementos finitos; uno con un mallado convencional formado por elementos rectangulares, y otro con un mallado isostático, y la comparación de su error. Los dos mallados tendrán un número similar de nudos. Como modelo se utiliza una viga en ménsula de 6 m de longitud y 2 m de canto con una carga puntual vertical en su extremo. Todos los algoritmos utilizados se encuentran programados en MATLAB. El presente documento se estructura en las siguientes partes: - Capítulo 1.- Descripción de los trabajos. Donde se realiza un resumen de los trabajos realizados en la creación del presente documento. - Capítulo 2.- Trabajos previos. En el que se resumen los trabajos realizados por otros autores antecedentes del presente documento. - Capítulo 3.- Fundamentos teóricos. Donde se explican las bases teóricas que se van a aplicar en la creación del algoritmo y en su análisis. - Capítulo 4.- Descripción del algoritmo implementado en este trabajo. En este capítulo se analiza la estructura del algoritmo empleado. Incluye diagramas de proceso del programa base y de las principales subrutinas. - Capítulo 5.- Resultados y discusión. Donde se realiza la comparación del error del mallado convencional y del mallado isostático; por un lado comparando las flechas obtenidas en el extremo de la viga en voladizo con el valor exacto de la flecha, y por otro lado utilizando el Error Cuadrático Medio de las tensiones medias. Se termina con un análisis crítico de los resultados. - Capítulo 6.- Conclusiones y futuras líneas de investigación.

Curso básico de programación del método de los elementos finitos

Estas notas que se publican a continuación corresponden a un curso de postgrado impartido durante el primer semestre del año 1983. El interés mostrado por los asistentes a dicho curso nos ha animado a escribir un resumen de las clases. Este libro supone un conocimiento te6rico de las ideas básicas del método de los elementos finitos. No obstante en una primera lección se resumen y ordenan aquellos aspectos mas importantes, que serán utilizados en lecciones sucesivas. En estas se desarrolla un programa de computador muy sencillo -sin complicaciones informáticas que obscurezcan la simplicidad del método- y se analiza de un modo detallado -en forma de organigramas y listados comentados- las distintas rutinas en lenguaje FORTRAN de este programa. Asimismo, y respetando el carácter elemental de la exposición se abren algunas posibilidades de ampliación y nuevos desarrollos del método. Algunos ejercicios y ejemplos al final de cada capítulo se espera permitan clarificar los puntos mas conflictivos del método. Finalmente se reúne en un apéndice, los distintos programas que se han mostrado en las sucesivas lecciones y que con objeto de que puedan ser procesados en microcomputadores se han traducido al lenguaje BASIC. Creemos y la experiencia del curso así nos la ha confirmado, que el método de elementos finitos se debe enseñar y aprender mediante la praxis y presentar los sucesivos desarrollos del método de un modo motivado como solución a problemas numéricos e informáticos que aparecen en su desarrollo. Si las lecciones que aquí se presentan permiten transmitir mejor estas ideas, los autores se sentirán más que recompensados por el trabajo que ha supuesto dar a luz a esta publicación.

Transformación del espacio cinemático Laban para la evaluación del movimiento

Este proyecto tiene como objetivo la implementación de un sistema capaz de analizar el movimiento corporal a partir de unos puntos cinemáticos. Estos puntos cinemáticos se obtienen con un programa previo y se captan con la cámara kinect. Para ello el primer paso es realizar un estudio sobre las técnicas y conocimientos existentes relacionados con el movimiento de las personas. Se sabe que Rudolph Laban fue uno de sus mayores exponentes y gracias a sus observaciones se establece una relación entre la personalidad, el estado anímico y la forma de moverse de un individuo. Laban acuñó el término esfuerzo, que hace referencia al modo en que se administra la energía que genera el movimiento y de qué manera se modula en las secuencias, es una manera de describir la intención de las expresiones internas. El esfuerzo se divide en 4 categorías: peso, espacio, tiempo y flujo, y cada una de estas categorías tiene una polaridad denominada elemento de esfuerzo. Con estos 8 elementos de esfuerzo un movimiento queda caracterizado. Para poder cuantificar los citados elementos de esfuerzo se buscan movimientos que representen a alguno de ellos. Los movimientos se graban con la cámara kinect y se guardan sus valores en un archivo csv. Para el procesado de estos datos se establece que el sistema más adecuado es una red neuronal debido a su flexibilidad y capacidad a la hora de procesar entradas no lineales. Para la implementación de la misma se requiere un amplio estudio que incluye: topologías, funciones de activación, tipos de aprendizaje, algoritmos de entrenamiento entre otros. Se decide que la red tenga dos capas ocultas, para mejor procesado de los datos, que sea estática, siga un proceso de cálculo hacia delante (Feedforward) y el algoritmo por el que se rija su aprendizaje sea el de retropropagación (Backpropagation) En una red estática las entradas han de ser valores fijos, es decir, no pueden variar en el tiempo por lo que habrá que implementar un programa intermedio que haga una media aritmética de los valores. Una segunda prueba con la misma red trata de comprobar si sería capaz de reconocer movimientos que estuvieran caracterizados por más de un elemento de esfuerzo. Para ello se vuelven a grabar los movimientos, esta vez en parejas de dos, y el resto del proceso es igual. ABSTRACT. The aim of this project is the implementation of a system able to analyze body movement from cinematic data. This cinematic data was obtained with a previous program. The first step is carrying out a study about the techniques and knowledge existing nowadays related to people movement. It is known that Rudolf Laban was one the greatest exponents of this field and thanks to his observations a relation between personality, mood and the way the person moves was made. Laban coined the term effort, that refers to the way energy generated from a movement is managed and how it is modulated in the sequence, this is a method of describing the inner intention of the person. The effort is divided into 4 categories: weight, space, time and flow, and each of these categories have 2 polarities named elements of effort. These 8 elements typify a movement. We look for movements that are made of these elements so we can quantify them. The movements are recorded with the kinect camera and saved in a csv file. In order to process this data a neural network is chosen owe to its flexibility and capability of processing non-linear inputs. For its implementation it is required a wide study regarding: topology, activation functions, different types of learning methods and training algorithms among others. The neural network for this project will have 2 hidden layers, it will be static and follow a feedforward process ruled by backpropagation. In a static net the inputs must be fixed, this means they cannot vary in time, so we will have to implement an intermediate program to calculate the average of our data. A second test for our net will be checking its ability to recognize more than one effort element in just one movement. In order to do this all the movements are recorded again but this time in pairs, the rest of the process remains the same.

Influencia de la adición de escorias de aluminio en las propiedades de productos de arcilla cocida

El presente trabajo plantea la reutilización directa de escorias de aluminio procedentes de la metalurgia secundaria mediante. La escoria con un contenido variable del 10-20% de aluminio metálico y oxido de aluminio es triturada hasta obtener una fracción inferior a las 600micras. Las mezclas con arcilla en contenidos del 10 y 20% de escoria se realizaron en un molino de bolas (145rpm/30min). Mediante compactación en matriz a 100 MPa se alcanzaron densidades de 2.2-2.3 g/cm3. Los materiales de arcilla cocida a 980 presentaron densidades finales de 1.95-2.1 g/cm3. La distribución de la escoria es muy uniforme en el material cocido, mejorando su densidad y disminuyendo la absorción de agua. La resistencia a flexión se mejora con la adición de escorias, si bien no hay diferencias importantes entre las composiciones empleadas. Una mayor temperatura de cocción (1080?) mejora la densidad final y disminuye la absorción de agua. La realización de un tratamiento termoquímico previo a los polvos de escorias, permite mejorar su la resistencia a flexión de las mezclas con 10% y 20% de escoria y reducir la variación dimensional y la absorción de agua tras cocción a 950.

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.

Análisis del comportamiento mecánico de un rack de baterías frente a eventos de choque.

El trabajo fin de máster, titulado “ANÁLISIS DEL COMPORTAMIENTO MECÁNICO DE UN RACK DE BATERÍAS FRENTE A EVENTOS DE CHOQUE” fue desarrollado por el estudiante D. Javier Rivera Hoyos como proyecto final del Máster Universitario en Ingeniería Mecánica de la UPM y que estuvo bajo la tutoría del Dr. D. Luis Martínez, profesor y director de la Unidad de Biomecánica del INSIA-UPM. Este TFM se llevó a cabo en el desarrollo del proyecto europeo OPERA4FEV, el cual hace parte del 7º Programa Marco de la Comisión Europea realizado por diez entidades, de seis países diferentes, especializadas en diversos campos de la ingeniería, teniendo como objetivo, el proponer una solución alternativa que sea barata, ligera y versátil, que mejore la tecnología actual, la cual está basada en la utilización de racks metálicos para el empaquetamiento de las baterías de los vehículos eléctricos. Para cumplir con ese objetivo, se ha propuesto desarrollar un rack para baterías fabricado en un material termoplástico, además del rediseño de los componentes internos del mismo, con el cumpliendo de los requisitos normativos de seguridad exigidos para este tipo de dispositivos. El tema escogido para la elaboración del Trabajo Fin de Master, trata del análisis de la resistencia mecánica de un rack de baterías, el cual fue llevado a cabo mediante el uso de la técnica de los elementos finitos, empleando para ello la suite de HYPERWORWS, una serie de programas especializados en simulación que permite la creación de modelos de elementos finitos a partir de diseños CAD en 3D. Con el uso de estos programas fue posible la realización de ensayos virtuales los cuales permitieron la representación de las condiciones características de diferentes eventos de choque. Se siguió la metodología tradicional para el análisis por elementos finitos, que inicia con una geometría inicial creada en un programa CAD y la cual posteriormente es dividida en elementos finitos. A continuación, se procede a la asignación de cargas y condiciones de contorno completando el modelo y dejándolo preparado para el proceso de cálculo. Finalmente, los resultados fueron analizados y se tomaron las decisiones oportunas para llevar a cabo las modificaciones en el modelo que permitieran mejorar los resultados. Con este TFM se logró realizar la evaluación de una primera propuesta de diseño de un rack de baterías para un vehículo industrial tipo N2, determinando las áreas críticas de fallo y aportando soluciones para su mejoramiento.

Espacios de interacción. Estrategias de relación en los proyectos de vivienda de SANAA.

La oficina de arquitectura SANAA está generando cambios significativos en la práctica de la arquitectura actual, especialmente aportando una nueva manera de utilizar el espacio de relación en la vivienda como lugar neutro, no deformado por el programa funcional y que de esta manera ofrece un campo abierto para que se desarrollen las relaciones humanas con más libertad y con una mayor integración con el entorno. SANAA intenta dar una respuesta a la complejidad de la vida actual japonesa por medio de un espacio más flexible y más interconectado que considera al habitante partícipe activo. La variedad de espacios y sus conexiones ofrecen diferentes posibilidades de uso, circulación y relación entre personas. La arquitectura genera herramientas para sorprender o despertar la curiosidad del habitante siendo éste en última instancia quien decide cómo utilizarla. Sus proyectos se pueden comparar con una playa donde existen reglas de juego pero cada uno tiene libertad de movimiento, libertad a la hora de elegir cómo y dónde colocarse. En su arquitectura la acción da sentido al espacio. Se diseña una estructura flexible que relaciona todas las estancias de la misma manera y sobre la que el habitante debe actuar. Una misma estancia puede albergar diferentes programas dependiendo de los acontecimientos y las necesidades del usuario. Se incita a la reflexión. Sería como un profesor que busca que el alumno se cuestione y genere sus propias herramientas. No se espera que el habitante simplemente ocupe el espacio sino que le obliga a actuar sobre él. La arquitectura busca la interacción entre sus habitantes. La vida urbana moderna aísla cada vez más al individuo y genera nuevos retos a la arquitectura. SANAA responde a las necesidades actuales utilizando espacios y conexiones que facilitan la interacción entre los habitantes. Sin embargo a la vez que proyecta estos espacios de interacción mantiene la privacidad según las circunstancias y necesidades. Este artículo consiste en la búsqueda de los espacios que buscan la máxima interacción entre los habitantes y el entorno en la vivienda unifamiliar de SANAA.

La vivienda plurifamiliar de Juan Manuel Ruiz de la Prada

El objetivo de este trabajo es conocer la arquitectura de Juan Manuel Ruiz de la Prada, un arquitecto cuya obra ha dejado una impronta en la ciudad de Madrid, pero sobre el que no hay apenas información objetiva que ponga en valor su trabajo. Lo más relevante dentro de su trayectoria como arquitecto, es una serie de edificios en los barrios de Salamanca y Chamberí, con un programa similar y ejecutados en un corto periodo de tiempo. Este trabajo analiza las circunstancias del Madrid de los 60 junto con la arquitectura de la vivienda plurifamiliar destinada a las clases acomodadas de la época. Se han estudiado con mayor profundidad, dos de los edificios de Juan Manuel Ruiz de la Prada, en los que tuvo un doble papel de promotor y de arquitecto. El primero situado en José Abascal nº50 con Zurbano nº73 y el segundo situado en Martínez Campos con Zurbano nº51 que, a su vez, es el primero de una serie de cuatro.