Las Redes de Petri Interpretadas en el Diagnóstico de Fallos de Sistemas Híbridos. Aplicación a un Helicóptero no Tripulado

La seguridad y fiabilidad de los procesos industriales son la principal preocupación de los ingenieros encargados de las plantas industriales. Por lo tanto, desde un punto de vista económico, el objetivo principal es reducir el costo del mantenimiento, el tiempo de inactividad y las pérdidas causadas por los fallos. Por otra parte, la seguridad de los operadores, que afecta a los aspectos sociales y económicos, es el factor más relevante a considerar en cualquier sistema Debido a esto, el diagnóstico de fallos se ha convertido en un foco importante de interés para los investigadores de todo el mundo e ingenieros en la industria. Los principales trabajos enfocados en detección de fallos se basan en modelos de los procesos. Existen diferentes técnicas para el modelado de procesos industriales tales como máquinas de estado, árboles de decisión y Redes de Petri (RdP). Por lo tanto, esta tesis se centra en el modelado de procesos utilizando redes de petri interpretadas. Redes de Petri es una herramienta usada en el modelado gráfico y matemático con la habilidad para describir información de los sistemas de una manera concurrente, paralela, asincrona, distribuida y no determinística o estocástica. RdP son también una herramienta de comunicación visual gráfica útil como lo son las cartas de flujo o diagramas de bloques. Adicionalmente, las marcas de las RdP simulan la dinámica y concurrencia de los sistemas. Finalmente, ellas tienen la capacidad de definir ecuaciones de estado específicas, ecuaciones algebraicas y otros modelos que representan el comportamiento común de los sistemas. Entre los diferentes tipos de redes de petri (Interpretadas, Coloreadas, etc.), este trabajo de investigación trata con redes de petri interpretadas principalmente debido a características tales como sincronización, lugares temporizados, aparte de su capacidad para procesamiento de datos. Esta investigación comienza con el proceso para diseñar y construir el modelo y diagnosticador para detectar fallos definitivos, posteriormente, la dinámica temporal fue adicionada para detectar fallos intermitentes. Dos procesos industriales, concretamente un HVAC (Calefacción, Ventilación y Aire Acondicionado) y un Proceso de Envasado de Líquidos fueron usados como banco de pruebas para implementar la herramienta de diagnóstico de fallos (FD) creada. Finalmente, su capacidad de diagnóstico fue ampliada en orden a detectar fallos en sistemas híbridos. Finalmente, un pequeño helicóptero no tripulado fue elegido como ejemplo de sistema donde la seguridad es un desafío, y las técnicas de detección de fallos desarrolladas en esta tesis llevan a ser una herramienta valorada, desde que los accidentes de las aeronaves no tripuladas (UAVs) envuelven un alto costo económico y son la principal razón para introducir restricciones de volar sobre áreas pobladas. Así, este trabajo introduce un proceso sistemático para construir un Diagnosticador de Fallos del sistema mencionado basado en RdR Esta novedosa herramienta es capaz de detectar fallos definitivos e intermitentes. El trabajo realizado es discutido desde un punto de vista teórico y práctico. El procedimiento comienza con la división del sistema en subsistemas para seguido integrar en una RdP diagnosticadora global que es capaz de monitorear el sistema completo y mostrar las variables críticas al operador en orden a determinar la salud del UAV, para de esta manera prevenir accidentes. Un Sistema de Adquisición de Datos (DAQ) ha sido también diseñado para recoger datos durante los vuelos y alimentar la RdP diagnosticadora. Vuelos reales realizados bajo condiciones normales y de fallo han sido requeridos para llevar a cabo la configuración del diagnosticador y verificar su comportamiento. Vale la pena señalar que un alto riesgo fue asumido en la generación de fallos durante los vuelos, a pesar de eso esto permitió recoger datos básicos para desarrollar el diagnóstico de fallos, técnicas de aislamiento, protocolos de mantenimiento, modelos de comportamiento, etc. Finalmente, un resumen de la validación de resultados obtenidos durante las pruebas de vuelo es también incluido. Un extensivo uso de esta herramienta mejorará los protocolos de mantenimiento para UAVs (especialmente helicópteros) y permite establecer recomendaciones en regulaciones. El uso del diagnosticador usando redes de petri es considerado un novedoso enfoque. ABSTRACT Safety and reliability of industrial processes are the main concern of the engineers in charge of industrial plants. Thus, from an economic point of view, the main goal is to reduce the maintenance downtime cost and the losses caused by failures. Moreover, the safety of the operators, which affects to social and economic aspects, is the most relevant factor to consider in any system. Due to this, fault diagnosis has become a relevant focus of interest for worldwide researchers and engineers in the industry. The main works focused on failure detection are based on models of the processes. There are different techniques for modelling industrial processes such as state machines, decision trees and Petri Nets (PN). Thus, this Thesis is focused on modelling processes by using Interpreted Petri Nets. Petri Nets is a tool used in the graphic and mathematical modelling with ability to describe information of the systems in a concurrent, parallel, asynchronous, distributed and not deterministic or stochastic manner. PNs are also useful graphical visual communication tools as flow chart or block diagram. Additionally, the marks of the PN simulate the dynamics and concurrence of the systems. Finally, they are able to define specific state equations, algebraic equations and other models that represent the common behaviour of systems. Among the different types of PN (Interpreted, Coloured, etc.), this research work deals with the interpreted Petri Nets mainly due to features such as synchronization capabilities, timed places, apart from their capability for processing data. This Research begins with the process for designing and building the model and diagnoser to detect permanent faults, subsequently, the temporal dynamic was added for detecting intermittent faults. Two industrial processes, namely HVAC (Heating, Ventilation and Air Condition) and Liquids Packaging Process were used as testbed for implementing the Fault Diagnosis (FD) tool created. Finally, its diagnostic capability was enhanced in order to detect faults in hybrid systems. Finally, a small unmanned helicopter was chosen as example of system where safety is a challenge and fault detection techniques developed in this Thesis turn out to be a valuable tool since UAVs accidents involve high economic cost and are the main reason for setting restrictions to fly over populated areas. Thus, this work introduces a systematic process for building a Fault Diagnoser of the mentioned system based on Petri Nets. This novel tool is able to detect both intermittent and permanent faults. The work carried out is discussed from theoretical and practical point of view. The procedure begins with a division of the system into subsystems for further integration into a global PN diagnoser that is able to monitor the whole system and show critical variables to the operator in order to determine the UAV health, preventing accidents in this manner. A Data Acquisition System (DAQ) has been also designed for collecting data during the flights and feed PN Diagnoser. Real flights carried out under nominal and failure conditions have been required to perform the diagnoser setup and verify its performance. It is worth noting that a high risk was assumed in the generation of faults during the flights, nevertheless this allowed collecting basic data so as to develop fault diagnosis, isolations techniques, maintenance protocols, behaviour models, etc. Finally, a summary of the validation results obtained during real flight tests is also included. An extensive use of this tool will improve preventive maintenance protocols for UAVs (especially helicopters) and allow establishing recommendations in regulations. The use of the diagnoser by using Petri Nets is considered as novel approach.

Proposal for the Management of temporal and semantic components of Geographic Information

This poster raises the issue of a research work oriented to the storage, retrieval, representation and analysis of dynamic GI, taking into account The ultimate objective is the modelling and representation of the dynamic nature of geographic features, establishing mechanisms to store geometries enriched with a temporal structure (regardless of space) and a set of semantic descriptors detailing and clarifying the nature of the represented features and their temporality. the semantic, the temporal and the spatiotemporal components. We intend to define a set of methods, rules and restrictions for the adequate integration of these components into the primary elements of the GI: theme, location, time [1]. We intend to establish and incorporate three new structures (layers) into the core of data storage by using mark-up languages: a semantictemporal structure, a geosemantic structure, and an incremental spatiotemporal structure. Thus, data would be provided with the capability of pinpointing and expressing their own basic and temporal characteristics, enabling them to interact each other according to their context, and their time and meaning relationships that could be eventually established

Proposal for the Management of temporal and semantic components of Geographic Information

This poster raises the issue of a research work oriented to the storage, retrieval, representation and analysis of dynamic GI, taking into account the semantic, the temporal and the spatiotemporal components. We intend to define a set of methods, rules and restrictions for the adequate integration of these components into the primary elements of the GI: theme, location, time [1]. We intend to establish and incorporate three new structures (layers) into the core of data storage by using mark-up languages: a semantictemporal structure, a geosemantic structure, and an incremental spatiotemporal structure. The ultimate objective is the modelling and representation of the dynamic nature of geographic features, establishing mechanisms to store geometries enriched with a temporal structure (regardless of space) and a set of semantic descriptors detailing and clarifying the nature of the represented features and their temporality. Thus, data would be provided with the capability of pinpointing and expressing their own basic and temporal characteristics, enabling them to interact each other according to their context, and their time and meaning relationships that could be eventually established

A dual-band priority assignment algorithm for dynamic QoS resource management

Future high-quality consumer electronics will contain a number of applications running in a highly dynamic environment, and their execution will need to be efficiently arbitrated by the underlying platform software. The multimedia applications that currently execute in such similar contexts face frequent run-time variations in their resource demands, originated by the greedy nature of the multimedia processing itself. Changes in resource demands are triggered by numerous reasons (e.g. a switch in the input media compression format). Such situations require real-time adaptation mechanisms to adjust the system operation to the new requirements, and this must be done seamlessly to satisfy the user experience. One solution for efficiently managing application execution is to apply quality of service resource management techniques, based on assigning and enforcing resource contracts to applications. Most resource management solutions provide temporal isolation by enforcing resource assignments and avoiding any resource overruns. However, this has a clear limitation over the cost-effective resource usage. This paper presents a simple priority assignment scheme based on uniform priority bands to allow that greedy multimedia tasks incur in safe overruns that increase resource usage and do not threaten the timely execution of non-overrunning tasks. Experimental results show that the proposed priority assignment scheme in combination with a resource accounting mechanism preserves timely multimedia execution and delivery, achieves a higher cost-effective processor usage, and guarantees the execution isolation of non-overrunning tasks.

An Interactive Bibliography on Temporal GIS.

This report introduces TimeBliography, a dynamic and online bibliography on temporal GIS. We provide a brief description of the bibliography as well as the components and functionalities of the web application that supports it. The bibliography is fully accessible on the Web at http://spaceandtime.wsiabato.info.

Análisis espacio-temporal del gradiente urbano-rural del sur de la Región Metropolitana de Madrid y su entorno. Caracterización de los procesos y patrones paisajísticos acaecidos en el período 1990-2006

El objetivo de esta tesis es proponer una metodología capaz de cuantificar la dinámica paisajística a lo largo del gradiente urbano – rural perteneciente al sur de la Región Metropolitana de Madrid y su entorno. Esta tesis se estructura en ocho capítulos, planos y anejos. El primero se refiere a los antecedentes tanto conceptuales como metodológicos. Los primeros se centran en los diversos enfoques existentes en relación al estudio de la dinámica paisajística, con el objetivo de encontrar los puntos en común existentes entre el enfoque del metabolismo social, el de la ecología del paisaje y el humanista, para obtener un diagnóstico que permita entender la complejidad de la realidad a la que esta Tesis se enfrenta. Los segundos se centran en los antecedentes de carácter metodológico que también desde diversos enfoques han abordado el análisis de la dinámica paisajística. El segundo capítulo se centra en los objetivos concretos derivados del objetivo general ya expresado, la tesis considera que para comprender y cuantificar la dinámica hay que identificar en primer lugar los procesos de transformación, como manifestación espacial de los factores socioeconómicos y naturales responsables en última instancia de la variación de los patrones paisajísticos existentes. En segundo lugar se identifican los patrones paisajísticos con el objetivo de analizar sus características espaciales y su evolución en el período analizado. Por último se identifican los procesos paisajísticos, es decir qué tipos de variaciones espaciales se producen en los patrones paisajísticos como consecuencia de los procesos de transformación identificados así como su pauta de distribución a lo largo del gradiente urbano ‐ rural. El tercer capítulo se dedica a la caracterización del ámbito de estudio, ésta se extiende al sur del límite del suelo urbano de la capital madrileña en el año 1990, comprende la totalidad de los municipios madrileños que contactan con los municipios castellano – manchegos que se encuentran en el área de influencia de la capital, abarcando el área 9.968 km2. El cuarto capítulo se centra en la metodología. Como material de partida se ha utilizado en la cartografía del Corine Land Cover y como herramienta de análisis se ha utilizado los Sistemas de Información Geográfica. En primer lugar se identifican los procesos de transformación, acaecidos en los períodos 1990 – 2000 y 2000 – 2006, mediante la aplicación de matrices de transición. Se han identificado cuatro tipos de procesos dinámicos: Urbanización, abandono, renaturalización y agrarización. Se ha realizado un análisis de indicadores compuestos lo que ha permitido identificar los tipos de patrones paisajísticos existentes a lo largo del gradiente urbano – rural. Del mismo modo se ha calculado la variación de los indicadores individuales para identificar los procesos paisajísticos mediante el análisis de indicadores compuestos que se produjeron en el período 1990 – 2000 y 2000 – 2006. En el quinto capítulo se aportan los resultados tanto de carácter cuantitativo como gráfico de los tres componentes analizados tanto de forma independiente como integrada. En el sexto capítulo se describen las conclusiones producto de la investigación realizada. En el séptimo capítulo se identifican qué líneas de investigación podrían desarrollarse en el futuro para continuar la línea de investigación iniciada con esta tesis. ABSTRACT The aim of this thesis was to propose a methodology to characterize landscape dynamics along the urban – rural gradient in the south Madrid area. It´s structured in eight chapters, planes and annexes: the first one describes previous research. Firstly to make a diagnosis of the effects of landscape dynamic we have performed an integrated analysis from social metabolism, landscape ecology and the humanistic point of view. Secondly we have focused on previous methodological research mainly developped by landscape ecology. The second chapter focuses on specific objectives derived from the general objective. The thesis considers that to understand and quantify landscape dynamics must first identify the transformation processes: spatial manifestation of natural and socioeconomics factors that induce the change of landscape patterns. Secondly landscape patterns have been identified in order to analyze their spatial characteristics and evolution. Finally the landscape processes have been identified, i.e. what kind of spatial variations cause changes in landscape patterns along urban – rural gradient. The third chapter describes the study area. The study area occupies 9968 km2. It covers the area to the south of Madrid’s 1990 urban land area, and takes in the southeast of the Madrid Autonomous Region plus all the municipal areas of the Castilla–La Mancha Autonomous Region directly influenced by the expansion of Madrid. The fourth chapter contains the methodology. To identify the changes in the landscape of the study area, the land cover data for the area held in the CORINE LandCover Project Database was examined. To characterize the transformations processes in the period 1990 ‐ 2000 and 2000 – 2006, transition matrices were constructed. We have identified four clear changes: Urbanization, renaturalization, abandonment and agrarianization. We have characterized landscape patterns using composite indicators by integrating individual spatial metrics. Similarly we have characterized landscape processes using composite indicators by integrating the variation of individual spatial metrics. Chapter fifth includes the results, both for each component and its final integration. The conclusions of this research have been described in the sixth chapter. The seventh chapter describes what kind of investigations could be done in the future.

Análisis espacio-temporal del gradiente urbano-rural del sur de la Región Metropolitana de Madrid y su entorno. Caracterización de los procesos y patrones paisajísticos acaecidos en el período 1990-2006 (versión revisada y corregida)

El objetivo de esta tesis es proponer una metodología capaz de cuantificar la dinámica paisajística a lo largo del gradiente urbano – rural perteneciente al sur de la Región Metropolitana de Madrid y su entorno. Esta tesis se estructura en ocho capítulos, planos y anejos. El primero se refiere a los antecedentes tanto conceptuales como metodológicos. Los primeros se centran en los diversos enfoques existentes en relación al estudio de la dinámica paisajística, con el objetivo de encontrar los puntos en común existentes entre el enfoque del metabolismo social, el de la ecología del paisaje y el humanista, para obtener un diagnóstico que permita entender la complejidad de la realidad a la que esta Tesis se enfrenta. Los segundos se centran en los antecedentes de carácter metodológico que también desde diversos enfoques han abordado el análisis de la dinámica paisajística. El segundo capítulo se centra en los objetivos concretos derivados del objetivo general ya expresado, la tesis considera que para comprender y cuantificar la dinámica hay que identificar en primer lugar los procesos de transformación, como manifestación espacial de los factores socioeconómicos y naturales responsables en última instancia de la variación de los patrones paisajísticos existentes. En segundo lugar se identifican los patrones paisajísticos con el objetivo de analizar sus características espaciales y su evolución en el período analizado. Por último se identifican los procesos paisajísticos, es decir qué tipos de variaciones espaciales se producen en los patrones paisajísticos como consecuencia de los procesos de transformación identificados así como su pauta de distribución a lo largo del gradiente urbano ‐ rural. El tercer capítulo se dedica a la caracterización del ámbito de estudio, ésta se extiende al sur del límite del suelo urbano de la capital madrileña en el año 1990, comprende la totalidad de los municipios madrileños que contactan con los municipios castellano – manchegos que se encuentran en el área de influencia de la capital, abarcando el área 9.968 km2. El cuarto capítulo se centra en la metodología. Como material de partida se ha utilizado en la cartografía del Corine Land Cover y como herramienta de análisis se ha utilizado los Sistemas de Información Geográfica. En primer lugar se identifican los procesos de transformación, acaecidos en los períodos 1990 – 2000 y 2000 – 2006, mediante la aplicación de matrices de transición. Se han identificado cuatro tipos de procesos dinámicos: Urbanización, abandono, renaturalización y agrarización. Se ha realizado un análisis de indicadores compuestos lo que ha permitido identificar los tipos de patrones paisajísticos existentes a lo largo del gradiente urbano – rural. Del mismo modo se ha calculado la variación de los indicadores individuales para identificar los procesos paisajísticos mediante el análisis de indicadores compuestos que se produjeron en el período 1990 – 2000 y 2000 – 2006. En el quinto capítulo se aportan los resultados tanto de carácter cuantitativo como gráfico de los tres componentes analizados tanto de forma independiente como integrada. En el sexto capítulo se describen las conclusiones producto de la investigación realizada. En el séptimo capítulo se identifican qué líneas de investigación podrían desarrollarse en el futuro para continuar la línea de investigación iniciada con esta tesis. ABSTRACT The aim of this thesis was to propose a methodology to characterize landscape dynamics along the urban – rural gradient in the south Madrid area. It´s structured in eight chapters, planes and annexes: the first one describes previous research. Firstly to make a diagnosis of the effects of landscape dynamic we have performed an integrated analysis from social metabolism, landscape ecology and the humanistic point of view. Secondly we have focused on previous methodological research mainly developped by landscape ecology. The second chapter focuses on specific objectives derived from the general objective. The thesis considers that to understand and quantify landscape dynamics must first identify the transformation processes: spatial manifestation of natural and socioeconomics factors that induce the change of landscape patterns. Secondly landscape patterns have been identified in order to analyze their spatial characteristics and evolution. Finally the landscape processes have been identified, i.e. what kind of spatial variations cause changes in landscape patterns along urban – rural gradient. The third chapter describes the study area. The study area occupies 9968 km2. It covers the area to the south of Madrid’s 1990 urban land area, and takes in the southeast of the Madrid Autonomous Region plus all the municipal areas of the Castilla–La Mancha Autonomous Region directly influenced by the expansion of Madrid. The fourth chapter contains the methodology. To identify the changes in the landscape of the study area, the land cover data for the area held in the CORINE LandCover Project Database was examined. To characterize the transformations processes in the period 1990 ‐ 2000 and 2000 – 2006, transition matrices were constructed. We have identified four clear changes: Urbanization, renaturalization, abandonment and agrarianization. We have characterized landscape patterns using composite indicators by integrating individual spatial metrics. Similarly we have characterized landscape processes using composite indicators by integrating the variation of individual spatial metrics. Chapter fifth includes the results, both for each component and its final integration. The conclusions of this research have been described in the sixth chapter. The seventh chapter describes what kind of investigations could be done in the future.

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.

Methodology for Dynamic Stability and Robustness Analysis of Commercial-Power-Module-Based DC-Distributed Systems

El propósito de esta tesis es presentar una metodología para realizar análisis de la dinámica en pequeña señal y el comportamiento de sistemas de alimentación distribuidos de corriente continua (CC), formados por módulos comerciales. Para ello se hace uso de un método sencillo que indica los márgenes de estabilidad menos conservadores posibles mediante un solo número. Este índice es calculado en cada una de las interfaces que componen el sistema y puede usarse para obtener un índice global que indica la estabilidad del sistema global. De esta manera se posibilita la comparación de sistemas de alimentación distribuidos en términos de robustez. La interconexión de convertidores CC-CC entre ellos y con los filtros EMI necesarios puede originar interacciones no deseadas que dan lugar a la degradación del comportamiento de los convertidores, haciendo el sistema más propenso a inestabilidades. Esta diferencia en el comportamiento se debe a interacciones entre las impedancias de los diversos elementos del sistema. En la mayoría de los casos, los sistemas de alimentación distribuida están formados por módulos comerciales cuya estructura interna es desconocida. Por ello los análisis presentados en esta tesis se basan en medidas de la respuesta en frecuencia del convertidor que pueden realizarse desde los terminales de entrada y salida del mismo. Utilizando las medidas de las impedancias de entrada y salida de los elementos del sistema, se puede construir una función de sensibilidad que proporciona los márgenes de estabilidad de las diferentes interfaces. En esta tesis se utiliza el concepto del valor máximo de la función de sensibilidad (MPC por sus siglas en inglés) para indicar los márgenes de estabilidad como un único número. Una vez que la estabilidad de todas las interfaces del sistema se han evaluado individualmente, los índices obtenidos pueden combinarse para obtener un único número con el que comparar la estabilidad de diferentes sistemas. Igualmente se han analizado las posibles interacciones en la entrada y la salida de los convertidores CC-CC, obteniéndose expresiones analíticas con las que describir en detalle los acoplamientos generados en el sistema. Los estudios analíticos realizados se han validado experimentalmente a lo largo de la tesis. El análisis presentado en esta tesis se culmina con la obtención de un índice que condensa los márgenes de estabilidad menos conservativos. También se demuestra que la robustez del sistema está asegurada si las impedancias utilizadas en la función de sensibilidad se obtienen justamente en la entrada o la salida del subsistema que está siendo analizado. Por otra parte, la tesis presenta un conjunto de parámetros internos asimilados a impedancias, junto con sus expresiones analíticas, que permiten una explicación detallada de las interacciones en el sistema. Dichas expresiones analíticas pueden obtenerse bien mediante las funciones de transferencia analíticas si se conoce la estructura interna, o utilizando medidas en frecuencia o identificación de las mismas a través de la respuesta temporal del convertidor. De acuerdo a las metodologías presentadas en esta tesis se puede predecir la estabilidad y el comportamiento de sistemas compuestos básicamente por convertidores CC-CC y filtros, cuya estructura interna es desconocida. La predicción se basa en un índice que condensa la información de los márgenes de estabilidad y que permite la obtención de un indicador de la estabilidad global de todo el sistema, permitiendo la comparación de la estabilidad de diferentes arquitecturas de sistemas de alimentación distribuidos. ABSTRACT The purpose of this thesis is to present dynamic small-signal stability and performance analysis methodology for dc-distributed systems consisting of commercial power modules. Furthermore, the objective is to introduce simple method to state the least conservative margins for robust stability as a single number. In addition, an index characterizing the overall system stability is obtained, based on which different dc-distributed systems can be compared in terms of robustness. The interconnected systems are prone to impedance-based interactions which might lead to transient-performance degradation or even instability. These systems typically are constructed using commercial converters with unknown internal structure. Therefore, the analysis presented throughout this thesis is based on frequency responses measurable from the input and output terminals. The stability margins are stated utilizing a concept of maximum peak criteria, derived from the behavior of impedance-based sensitivity function that provides a single number to state robust stability. Using this concept, the stability information at every system interface is combined to a meaningful number to state the average robustness of the system. In addition, theoretical formulas are extracted to assess source and load side interactions in order to describe detailed couplings within the system. The presented theoretical analysis methodologies are experimentally validated throughout the thesis. In this thesis, according to the presented analysis, the least conservative stability margins are provided as a single number guaranteeing robustness. It is also shown that within the interconnected system the robust stability is ensured only if the impedance-based minor-loop gain is determined at the very input or output of each subsystem. Moreover, a complete set of impedance-type internal parameters as well as the formulas according to which the interaction sensitivity can be fully explained and analyzed, is provided. The given formulation can be utilized equally either based on measured frequency responses, time-domain identified internal parameters or extracted analytic transfer functions. Based on the analysis methodologies presented in this thesis, the stability and performance of interconnected systems consisting of converters with unknown internal structure, can be predicted. Moreover, the provided concept to assess the least conservative stability margins enables to obtain an index to state the overall robust stability of distributed power architecture and thus to compare different systems in terms of stability.