Towards execution time estimation for logic programs via static analysis and profiling

Effective static analyses have been proposed which infer bounds on the number of resolutions or reductions. These have the advantage of being independent from the platform on which the programs are executed and have been shown to be useful in a number of applications, such as granularity control in parallel execution. On the other hand, in distributed computation scenarios where platforms with different capabilities come into play, it is necessary to express costs in metrics that include the characteristics of the platform. In particular, it is specially interesting to be able to infer upper and lower bounds on actual execution times. With this objective in mind, we propose an approach which combines compile-time analysis for cost bounds with a one-time profiling of the platform in order to determine the valúes of certain parameters for a given platform. These parameters calíbrate a cost model which, from then on, is able to compute statically time bound functions for procedures and to predict with a significant degree of accuracy the execution times of such procedures in the given platform. The approach has been implemented and integrated in the CiaoPP system.

Combining static analysis and profiling for estimating execution times in logic programs

Effective static analyses have been proposed which allow inferring functions which bound the number of resolutions or reductions. These have the advantage of being independent from the platform on which the programs are executed and such bounds have been shown useful in a number of applications, such as granularity control in parallel execution. On the other hand, in certain distributed computation scenarios where different platforms come into play, with each platform having different capabilities, it is more interesting to express costs in metrics that include the characteristics of the platform. In particular, it is specially interesting to be able to infer upper and lower bounds on actual execution time. With this objective in mind, we propose a method which allows inferring upper and lower bounds on the execution times of procedures of a program in a given execution platform. The approach combines compile-time cost bounds analysis with a one-time profiling of the platform in order to determine the values of certain constants for that platform. These constants calibrate a cost model which from then on is able to compute statically time bound functions for procedures and to predict with a significant degree of accuracy the execution times of such procedures in the given platform. The approach has been implemented and integrated in the CiaoPP system.

Inferring determinacy and mutual exclusion in logic programs using mode and type analysis.

We propose an analysis for detecting procedures and goals that are deterministic (i.e., that produce at most one solution at most once), or predicates whose clause tests are mutually exclusive (which implies that at most one of their clauses will succeed) even if they are not deterministic. The analysis takes advantage of the pruning operator in order to improve the detection of mutual exclusion and determinacy. It also supports arithmetic equations and disequations, as well as equations and disequations on terms, for which we give a complete satisfiability testing algorithm, w.r.t. available type information. We have implemented the analysis and integrated it in the CiaoPP system, which also infers automatically the mode and type information that our analysis takes as input. Experiments performed on this implementation show that the analysis is fairly accurate and efficient.

Adaptive liquid-crystal phase-only passive devices

This PhD work is focused on liquid crystal based tunable phase devices with special emphasis on their design and manufacturing. In the course of the work a number of new manufacturing technologies have been implemented in the UPM clean room facilities, leading to an important improvement in the range of devices being manufactured in the laboratory. Furthermore, a number of novel phase devices have been developed, all of them including novel electrodes, and/or alignment layers. The most important manufacturing progress has been the introduction of reactive ion etching as a tool for achieving high resolution photolithography on indium-tin-oxide (ITO) coated glass and quartz substrates. Another important manufacturing result is the successful elaboration of a binding protocol of anisotropic conduction adhesives. These have been employed in high density interconnections between ITO-glass and flexible printed circuits. Regarding material characterization, the comparative study of nonstoichiometric silicon oxide (SiOx) and silica (SiO2) inorganic alignment layers, as well as the relationship between surface layer deposition, layer morphology and liquid crystal electrooptical response must be highlighted, together with the characterization of the degradation of liquid crystal devices in simulated space mission environment. A wide variety of phase devices have been developed, with special emphasis on beam steerers. One of these was developed within the framework of an ESA project, and consisted of a high density reconfigurable 1D blaze grating, with a spatial separation of the controlling microelectronics and the active, radiation exposed, area. The developed devices confirmed the assumption that liquid crystal devices with such a separation of components, are radiation hard, and can be designed to be both vibration and temperature sturdy. In parallel to the above, an evenly variable analog beam steering device was designed, manufactured and characterized, providing a narrow cone diffraction free beam steering. This steering device is characterized by a very limited number of electrodes necessary for the redirection of a light beam. As few as 4 different voltage levels were needed in order to redirect a light beam. Finally at the Wojskowa Akademia Techniczna (Military University of Technology) in Warsaw, Poland, a wedged analog tunable beam steering device was designed, manufactured and characterized. This beam steerer, like the former one, was designed to resist the harsh conditions both in space and in the context of the shuttle launch. Apart from the beam steering devices, reconfigurable vortices and modal lens devices have been manufactured and characterized. In summary, during this work a large number of liquid crystal devices and liquid crystal device manufacturing technologies have been developed. Besides their relevance in scientific publications and technical achievements, most of these new devices have demonstrated their usefulness in the actual work of the research group where this PhD has been completed. El presente trabajo de Tesis se ha centrado en el diseño, fabricación y caracterización de nuevos dispositivos de fase basados en cristal líquido. Actualmente se están desarrollando dispositivos basados en cristal líquido para aplicaciones diferentes a su uso habitual como displays. Poseen la ventaja de que los dispositivos pueden ser controlados por bajas tensiones y no necesitan elementos mecánicos para su funcionamiento. La fabricación de todos los dispositivos del presente trabajo se ha realizado en la cámara limpia del grupo. La cámara limpia ha sido diseñada por el grupo de investigación, es de dimensiones reducidas pero muy versátil. Está dividida en distintas áreas de trabajo dependiendo del tipo de proceso que se lleva a cabo. La cámara limpia está completamente cubierta de un material libre de polvo. Todas las entradas de suministro de gas y agua están selladas. El aire filtrado es constantemente bombeado dentro de la zona limpia, a fin de crear una sobrepresión evitando así la entrada de aire sin filtrar. Las personas que trabajan en esta zona siempre deben de estar protegidas con un traje especial. Se utilizan trajes especiales que constan de: mono, máscara, guantes de látex, gorro, patucos y gafas de protección UV, cuando sea necesario. Para introducir material dentro de la cámara limpia se debe limpiar con alcohol y paños especiales y posteriormente secarlos con nitrógeno a presión. La fabricación debe seguir estrictamente unos pasos determinados, que pueden cambiar dependiendo de los requerimientos de cada dispositivo. Por ello, la fabricación de dispositivos requiere la formulación de varios protocolos de fabricación. Estos protocolos deben ser estrictamente respetados a fin de obtener repetitividad en los experimentos, lo que lleva siempre asociado un proceso de fabricación fiable. Una célula de cristal líquido está compuesta (de forma general) por dos vidrios ensamblados (sándwich) y colocados a una distancia determinada. Los vidrios se han sometido a una serie de procesos para acondicionar las superficies internas. La célula se llena con cristal líquido. De forma resumida, el proceso de fabricación general es el siguiente: inicialmente, se cortan los vidrios (cuya cara interna es conductora) y se limpian. Después se imprimen las pistas sobre el vidrio formando los píxeles. Estas pistas conductoras provienen del vidrio con la capa conductora de ITO (óxido de indio y estaño). Esto se hace a través de un proceso de fotolitografía con una resina fotosensible, y un desarrollo y ataque posterior del ITO sin protección. Más tarde, las caras internas de los vidrios se acondicionan depositando una capa, que puede ser orgánica o inorgánica (un polímero o un óxido). Esta etapa es crucial para el funcionamiento del dispositivo: induce la orientación de las moléculas de cristal líquido. Una vez que las superficies están acondicionadas, se depositan espaciadores en las mismas: son pequeñas esferas o cilindros de tamaño calibrado (pocos micrómetros) para garantizar un espesor homogéneo del dispositivo. Después en uno de los sustratos se deposita un adhesivo (gasket). A continuación, los sustratos se ensamblan teniendo en cuenta que el gasket debe dejar una boca libre para que el cristal líquido se introduzca posteriormente dentro de la célula. El llenado de la célula se realiza en una cámara de vacío y después la boca se sella. Por último, la conexión de los cables a la célula y el montaje de los polarizadores se realizan fuera de la sala limpia (Figura 1). Dependiendo de la aplicación, el cristal líquido empleado y los demás componentes de la célula tendrán unas características particulares. Para el diseño de los dispositivos de este trabajo se ha realizado un estudio de superficies inorgánicas de alineamiento del cristal líquido, que será de gran importancia para la preparación de los dispositivos de fase, dependiendo de las condiciones ambientales en las que vayan a trabajar. Los materiales inorgánicos que se han estudiado han sido en este caso SiOx y SiO2. El estudio ha comprendido tanto los factores de preparación influyentes en el alineamiento, el comportamiento del cristal líquido al variar estos factores y un estudio de la morfología de las superficies obtenidas.

Functional validation of MB-OFDM system using HW-in the loop

Functional validation of complex digital systems is a hard and critical task in the design flow. In particular, when dealing with communication systems, like Multiband Orthogonal Frequency Division Multiplexing Ultra Wideband (MB-OFDM UWB), the design decisions taken during the process have to be validated at different levels in an easy way. In this work, a unified algorithm-architecture-circuit co-design environment for this type of systems, to be implemented in FPGA, is presented. The main objective is to find an efficient methodology for designing a configurable optimized MB-OFDM UWB system by using as few efforts as possible in verification stage, so as to speed up the development period. Although this efficient design methodology is tested and considered to be suitable for almost all types of complex FPGA designs, we propose a solution where both the circuit and the communication channel are tested at different levels (algorithmic, RTL, hardware device) using a common testbench.

CookieLibs: An Intuitive Software Platform For Controlling Cookies Wireless Sensor Nodes

In this work a complete set of libraries for developing wireless sensor applications in a simple and intuitive way is presented, in contraposition to the most spread application abstraction-level mechanisms based on operating systems. The main target of this software platform, named CookieLibs, is to provide the highest abstraction level on the management of WSNs but in the simplest way for those users who are not familiar with software design, in order to achieve a fast profiling mechanism for reliable prototyping based on the Cookies platform.

Sistema para cambiar la geometría de un motor

En este proyecto se desarrolla un sistema electrónico para variar la geometría de un motor de un monoplaza que participa en la competición Fórmula SAE. Fórmula SAE es una competición de diseño de monoplazas para estudiantes, organizado por “Society of Automotive Enginners” (SAE). Este concurso busca la innovación tecnológica de la automoción, así como que estudiantes participen en un trabajo real, en el cual el objetivo es obtener resultados competitivos cumpliendo con una serie de requisitos. La variación de la geometría de un motor en un vehículo permite mejorar el rendimiento del monoplaza consiguiendo elevar el par de potencia del motor. Cualquier mejora en del vehículo en un ámbito de competición puede resultar determinante en el desenlace de la misma. El objetivo del proyecto es realizar esta variación mediante el control de la longitud de los tubos de admisión de aire o “runners” del motor de combustión, empleando un motor lineal paso a paso. A partir de la información obtenida por sensores de revoluciones del motor de combustión y la posición del acelerador se debe controlar la distancia de dichos tubos. Integrando este sistema en el bus CAN del vehículo para que comparta la información medida al resto de módulos. Por todo esto se realiza un estudio aclarando los aspectos generales del objetivo del trabajo, para la comprensión del proyecto a realizar, las posibilidades de realización y adquisición de conocimientos para un mejor desarrollo. Se presenta una solución basada en el control del motor lineal paso a paso mediante el microcontrolador PIC32MX795F512-L. Dispositivo del fabricante Microchip con una arquitectura de 32 bits. Este dispone de un módulo CAN integrado y distintos periféricos que se emplean en la medición de los sensores y actuación sobre el motor paso a paso empleando el driver de Texas Instruments DRV8805. Entonces el trabajo se realiza en dos líneas, una parte software de programación del control del sistema, empleando el software de Microchip MPLABX IDE y otra parte hardware de diseño de una PCB y circuitos acondicionadores para la conexión del microcontrolador, con los sensores, driver, motor paso a paso y bus CAN. El software empleado para la realización de la PCB es Orcad9.2/Layout. Para la evaluación de las medidas obtenidas por los sensores y la comprobación del bus CAN se emplea el kit de desarrollo de Microchip, MCP2515 CAN Bus Monitor Demo Board, que permite ver la información en el bus CAN e introducir tramas al mismo. ABSTRACT. This project develops an electronic system to vary the geometry of a car engine which runs the Formula SAE competition. Formula SAE is a design car competition for students, organized by "Society of Automotive Engineers" (SAE). This competition seeks technological innovation in the automotive industry and brings in students to participate in a real job, in which the objective is to obtain competitive results in compliance with certain requirements. Varying engine’s geometry in a vehicle improves car’s performance raising engine output torque. Any improvement in the vehicle in a competition field can be decisive in the outcome of it. The goal of the project is the variation by controlling the length of the air intake pipe or "runners" in a combustion engine, using a linear motor step. For these, uses the information gathered by speed sensors from the combustion engine and by the throttle position to control the distance of these tubes. This system is integrated in the vehicle CAN bus to share the information with the other modules. For all this is made a study to clarify the general aspects of the project in order to understand the activities developed inside the project, the different options available and also, to acquire knowledge for a better development of the project. The solution is based on linear stepper motor control by the microcontroller PIC32MX795F512-L. Device from manufacturer Microchip with a 32-bit architecture. This module has an integrated CAN various peripherals that are used in measuring the performance of the sensors and drives the stepper motor using Texas Instruments DRV8805 driver. Then the work is done in two lines, first, control programming software system using software MPLABX Microchip IDE and, second, hardware design of a PCB and conditioning circuits for connecting the microcontroller, with sensors, driver stepper motor and CAN bus. The software used to carry out the PCB is Orcad9.2/Layout. For the evaluation of the measurements obtained by the sensors and CAN bus checking is used Microchip development kit, MCP2515 CAN Bus Monitor Demo Board, that allows you to see the information on the CAN bus and enter new frames in the bus.

Energy consumption and carbon dioxide emissions in rail and road freight transport in Spain: a case study of car carriers and bulk petrochemicals

This article provides a new methodology for estimating fuel consumption and emissions by enabling a correct comparison between freight transportation modes. The approach is developed and integrated as a part of an intelligent transportation system dealing with goods movement. A key issue is related to energy consumption ratios and consequent CO2 emissions. Energy consumption ratios are often used based on transport demand. However, including other ratios based on transport supply can be useful. Furthermore, it is important to indicate which factors are associated with variations in energy consumption and emissions; especially of interest are parameters that have a higher incidence and order of magnitude, in order to fairly compare and understand the difference between transport modes and sub-modes. The study finds that the use of an energy consumption equation can improve the quality of the estimates. The study proposes that coefficients that define the energy consumption equation should be tested to determine market niches and sources of improvement in energy consumption according to the category of vehicles, fuel types used, and classes of products transported.

A cyber-physical approach to combined HW-SW monitoring for improving energy efficiency in data centers

High-Performance Computing, Cloud computing and next-generation applications such e-Health or Smart Cities have dramatically increased the computational demand of Data Centers. The huge energy consumption, increasing levels of CO2 and the economic costs of these facilities represent a challenge for industry and researchers alike. Recent research trends propose the usage of holistic optimization techniques to jointly minimize Data Center computational and cooling costs from a multilevel perspective. This paper presents an analysis on the parameters needed to integrate the Data Center in a holistic optimization framework and leverages the usage of Cyber-Physical systems to gather workload, server and environmental data via software techniques and by deploying a non-intrusive Wireless Sensor Net- work (WSN). This solution tackles data sampling, retrieval and storage from a reconfigurable perspective, reducing the amount of data generated for optimization by a 68% without information loss, doubling the lifetime of the WSN nodes and allowing runtime energy minimization techniques in a real scenario.

An integrated approach to conceptual design of arch bridges with curved deck

El concepto de funicularidad se puede extender a estructuras lineales espaciales como, por ejemplo, los puentes arco con tablero curvo. Estas estructuras, especialmente pasarelas peatonales, son consecuencia de la necesidad de encajar trazados exigentes y de dar respuesta a nuevas demandas arquitectónicas. En las estructuras curvas el diseño conceptual juega un papel absolutamente esencial. Siempre ha sido así, pero en el caso presente, cabe resaltar que una errónea elección de la geometría conlleva una serie de problemas que se irán acumulando a lo largo del proceso de proyecto, de la construcción y de la vida de la estructura. En este trabajo se presenta SOFIA (Shaping Optimal Form with an Interactive Approach), una herramienta capaz de, conocida la geometría del tablero, de buscar automáticamente la forma del arco antifunicular correspondiente. El planteamiento seguido es conceptualmente el mismo que el utilizado en la búsqueda de formas óptimas en estructuras en dos dimensiones: el arco antifunicular es el que representa, para unas cargas dadas, el lugar geométrico de los puntos con momento flector nulo. La herramienta ha sido desarrollada en un entorno integrado, interactivo y paramético. Su implementación está ilustrada y unos ejemplos de análisis paramétricos están desarrollados. La posición transversal relativa entre tablero y arco ha sido investigada para obtener la configuración del puente estructuralmente más eficiente. Las pasarelas curvas se han convertido en un problema de ingeniería más común de lo habitual en el contexto de los desarrollos urbanos cuando el cliente está buscando un fuerte componente estético: un diseño conceptual adecuado permite obtener una estructura eficiente y elegante. Spatial arch bridges represent an innovative answer to demands on functionality, structural optimization and aesthetics for curved decks, popular in urban contexts. This thesis presents SOFIA (Shaping Optimal Form with an Interactive Approach), a methodology for conceptual designing of antifunicular spatial arch bridges with curved deck in a parametric, interactive and integrated environment. The approach and its implementation are in-depth described and detailed examples of parametric analyses are illustrated. The optimal deck-arch relative transversal position has been investigated for obtaining the most cost-effective bridge. Curved footbridges have become a more common engineering problem in the context of urban developments when the client is looking for a strong aesthetics component: an appropriate conceptual design allows to obtain an efficient and elegant structure.

Energy and Lighting Performance of Buildings in the Neighbourhood Ciudad de los Angeles, Before and After Refurbishing.

The Spanish Ministry of Economy and Competitiveness is funding the SHERIF Research Project, which falls under the INNPACTO pr ogram. This project aims to increase the rate of the existing building refurbishment fro m the energy efficiency point of view by designing a facade system that must be an economica l, flexible and integrated solution 1 . Under this project has been performing several task s regarding the constructive characterization and energy evaluation of the therm al behaviour of facades on existing buildings . In order to perform the latter task, in which this article will focus, has been developing a survey of various buildings in the nei ghbourhood Ciudad de los Angeles, which has as main objective the comparison between the ac tual energy and light behaviour of different buildings, prior and posterior to any ref urbishment works have been undertaken. The evaluation of the actual performance of buildin gs before and after being refurbished is aimed to determine the impact of the work developed as well as learn from the work performed for future interventions.

Accessibility instruments for planning practice: bridging the gap between academic research and decision-making.

One of the core objectives of urban planning practice is to provide spatial equity in terms of opportunities and use of public space and facilities. Accessibility is the element that serves this purpose as a concept linking the reciprocal relationship between transport and land use, thus shaping individual potential mobility to reach the desired destinations. Accessibility concepts are increasingly acknowledged as fundamental to understand the functioning of cities and urban regions. Indeed, by introducing them in planning practice, better solutions can be achieved in terms of spatial equity. The COST Action TU1002 "Accessibility instruments for planning practice" was specifically designed to address the gap between scientific research in measuring and modelling accessibility, and the current use of indicators of accessibility in urban planning practice. This paper shows the full process of introducing an easily understandable measure of accessibility to planning practitioners in Madrid, which is one of the case studies of the above-mentioned COST action. Changes in accessibility after the opening of a new metro line using contour measures were analyzed and then presented to a selection of urban planners and practitioners in Madrid as part of a workshop to evaluate the usefulness of this tool for planning practice. Isochrone maps were confirmed as an effective tool, as their utility can be supplemented by other indicators, and being GIS-based, it can be easily computed (when compared with transport models) and integrated with other datasets.

Environmental Wireless Sensor Network Deployment in Food Industry: from Theory to Practice

The difficulty behind Wireless Sensor Network deployments in industrial environments not only resides in the number of nodes or the communication protocols but also in the real location of the sensor nodes and the parameters to be monitored. Sensor soiling, high humidity and unreachable locations, among others, make real deployments a very difficult task to plan. Even though it is possible to find myriad approaches for floor planners and deployment tools in the state of the art, most of these problems are very difficult to model and foresee before actually deploying the network in the final scenario. This work shows two real deployments in food factories and how their problems are found and overcome.

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.

CMOS integration of AlN based piezoelectric microcantilevers

El gran crecimiento de los sistemas MEMS (Micro Electro Mechanical Systems) así como su presencia en la mayoría de los dispositivos que usamos diariamente despertó nuestro interés. Paralelamente, la tecnología CMOS (Complementary Metal Oxide Semiconductor) es la tecnología más utilizada para la fabricación de circuitos integrados. Además de ventajas relacionadas con el funcionamiento electrónico del dispositivo final, la integración de sistemas MEMS en la tecnología CMOS reduce significantemente los costes de fabricación. Algunos de los dispositivos MEMS con mayor variedad de aplicaciones son los microflejes. Estos dispositivos pueden ser utilizados para la extracción de energía, en microscopios de fuerza atómica o en sensores, como por ejemplo, para biodetección. Los materiales piezoeléctricos más comúnmente utilizados en aplicaciones MEMS se sintetizan a altas temperaturas y por lo tanto no son compatibles con la tecnología CMOS. En nuestro caso hemos usado nitruro de alumino (AlN), que se deposita a temperatura ambiente y es compatible con la tecnología CMOS. Además, es biocompatible, y por tanto podría formar parte de un dispositivo que actúe como biosensor. A lo largo de esta tesis hemos prestado especial atención en desarrollar un proceso de fabricación rápido, reproducible y de bajo coste. Para ello, todos los pasos de fabricación han sido minuciosamente optimizados. Los parámetros de sputtering para depositar el AlN, las distintas técnicas y recetas de ataque, los materiales que actúan como electrodos o las capas sacrificiales para liberar los flejes son algunos de los factores clave estudiados en este trabajo. Una vez que la fabricación de los microflejes de AlN ha sido optimizada, fueron medidos para caracterizar sus propiedades piezoeléctricas y finalmente verificar positivamente su viabilidad como dispositivos piezoeléctricos. ABSTRACT The huge growth of MEMS (Micro Electro Mechanical Systems) as well as their presence in most of our daily used devices aroused our interest on them. At the same time, CMOS (Complementary Metal Oxide Semiconductor) technology is the most popular technology for integrated circuits. In addition to advantages related with the electronics operation of the final device, the integration of MEMS with CMOS technology reduces the manufacturing costs significantly. Some of the MEMS devices with a wider variety of applications are the microcantilevers. These devices can be used for energy harvesting, in an atomic force microscopes or as sensors, as for example, for biodetection. Most of the piezoelectric materials used for these MEMS applications are synthesized at high temperature and consequently are not compatible with CMOS technology. In our case we have used aluminum nitride (AlN), which is deposited at room temperature and hence fully compatible with CMOS technology. Otherwise, it is biocompatible and and can be used to compose a biosensing device. During this thesis work we have specially focused our attention in developing a high throughput, reproducible and low cost fabrication process. All the manufacturing process steps of have been thoroughly optimized in order to achieve this goal. Sputtering parameters to synthesize AlN, different techniques and etching recipes, electrode material and sacrificial layers are some of the key factors studied in this work to develop the manufacturing process. Once the AlN microcantilevers fabrication was optimized, they were measured to characterize their piezoelectric properties and to successfully check their viability as piezoelectric devices.