FPGA-Based Wireless Sensor Node Architecture for High Performance Applications

While for years traditional wireless sensor nodes have been based on ultra-low power microcontrollers with sufficient but limited computing power, the complexity and number of tasks of today’s applications are constantly increasing. Increasing the node duty cycle is not feasible in all cases, so in many cases more computing power is required. This extra computing power may be achieved by either more powerful microcontrollers, though more power consumption or, in general, any solution capable of accelerating task execution. At this point, the use of hardware based, and in particular FPGA solutions, might appear as a candidate technology, since though power use is higher compared with lower power devices, execution time is reduced, so energy could be reduced overall. In order to demonstrate this, an innovative WSN node architecture is proposed. This architecture is based on a high performance high capacity state-of-the-art FPGA, which combines the advantages of the intrinsic acceleration provided by the parallelism of hardware devices, the use of partial reconfiguration capabilities, as well as a careful power-aware management system, to show that energy savings for certain higher-end applications can be achieved. Finally, comprehensive tests have been done to validate the platform in terms of performance and power consumption, to proof that better energy efficiency compared to processor based solutions can be achieved, for instance, when encryption is imposed by the application requirements.

Impacto de los medios sociales en la estrategia de las organizaciones

Dado el impacto que las redes sociales tienen en la vida diaria de los países desarrollados o en vías de desarrollo, éstas han pasado a tener un papel clave en dicho desarrollo social. Dicha consideración no sólo debe centrarse en cómo las personas forman las redes, sino las herramientas que emplean y la forma en la que estas deben ser tratadas por las organizaciones para conseguir una posición preferencial con los usuarios que forman las redes (considerando el creciente número de éstos todos los días). El presente trabajo trata de exponer la diferencia entre medios sociales y redes sociales, estableciendo una diferencia clara entre entre ambos, define lo que son los medios sociales (Social Media en Inglés), qué se debe considerar para que el uso de los mismos tenga una carácter exitoso en sus operaciones y cómo las organizaciones perciben la diferencia competitiva que éstos aportan en sus actividades. Una vez definida, destacamos la importancia de la consideración de estos nuevos medios en las estrategias de la compañías. Para ello, debemos ver el ecosistema de los medios sociales de forma general, y focalizarnos en la relación marca-compañía con el usuario/cliente. La inclusión de los medios sociales en las estrategias de las compañías, primero de forma independiente y, posteriormente, de forma integrada, hace que los modelos de negocio de las compañías se vayan adaptando a los tiempos. Se describe el cambio de paradigma de los modelos de negocio afectados por la introducción de los medios sociales, los elementos y tipos de modelos de negocio que se pueden tener, así como la adaptación de los modelos establecidos a los nuevos modelos. Posteriormente se ve cómo las compañías incluyen los medios sociales en su estrategia, a través de una planificación de medios sociales,partiendo de qué es una estrategia y cómo debe evaluarse. Una vez se ha definido el contexto (qué son los medios sociales, redes sociales, modelo de negocio, estrategia; así como sus características), se definen los bloques funcionales de los medios sociales, con su paralelismo en términos de la estrategia de las compañías, así como se indican determinados factores de éxito para su adopción. Hasta ahora, estamos mirando la organización de forma individual pero, dentro del mercado en el que desarrollan sus actividades, éstas deben ser evaluadas sobre el grado de desarrollo de los medios sociales en sus operaciones; y poder establecer así comparativas, con otras organizaciones, en relación a su grado de implantación. Con dicho objetivo, desarrollaremos un modelo de madurez de medios sociales (Social Media Maturity Model, SMMM o SM3), de forma teórica. ¿Cómo considerar dicho modelo de forma realista?. Basándonos en el método del estudio de casos, se realizará una análisis e investigación de diferentes organizaciones que nos indicará el grado de aproximación del modelo de madurez referenciado, con respecto a la realidad. ABSTRACT Considering the impact that social networks have in the daily life in developed or developing countries, they have come to play a key role in this social development. This consideration should not only focus on how people set up networks, but the tools they use and how these ones should be addressed by organizations to achieve a preferential position with users, forming networks (considering the increasing number of them every day). This work tries to explain the difference between social media and social networking, establishing a clear difference between them, defines what is Social Media, which should be considered for its use has a successful character in their operations and how organizations perceive the competitive edge they bring in their activities. Once they are defined, we remark the importance of considering these new media in companies strategies. For this, we see the social media ecosystem in general, and to focus on brandcompany relationship with the user/client. The inclusion of social media strategies in the companies, independently and in a integrated way, makes the business models of companies evolve along the time. It is described the paradigm shift in business models affected by the introduction of social media, elements and types of business models that can be had, and the adaptation of established models to new models. After that, it’s shown how companies include social media strategy through social media planning and building on what is a strategy and how it should be evaluated. Once the context is defined (what is social media, social networking, business model, strategy, and its features), the functional blocks of social media are defined, with its parallelism in terms of the strategy of companies and specific success factors are indicated. So far, we are looking at the organization individually but within the market in which they operate, they must be evaluated on the degree of development of social media in their operations; and to establish and compare with other organizations in relation to their degree of implementation. With this goal, we will develop a maturity model for social media (Social Media Maturity Model, SMMM or SM3), theoretically. How to consider the model realistically?. Based on the case study method, the analysis and research of different organizations that it will indicate the accuracy of the maturity model referenced with respect to the actually performed.

Diseño de un Procesador de Membranas Paralelo para los Sistemas P de Transición

La computación con membranas surge como una alternativa a la computación tradicional. Dentro de este campo se sitúan los denominados Sistemas P de Transición que se basan en la existencia de regiones que contienen recursos y reglas que hacen evolucionar a dichos recursos para poder llevar a cada una de las regiones a una nueva situación denominada configuración. La sucesión de las diferentes configuraciones conforman la computación. En este campo, el Grupo de Computación Natural de la Universidad Politécnica de Madrid lleva a cabo numerosas investigaciones al amparo de las cuales se han publicado numerosos artículos y realizado varias tesis doctorales. Las principales vías de investigación han sido, hasta el momento, el estudio del modelo teórico sobre el que se definen los Sistemas P, el estudio de los algoritmos que se utilizan para la aplicación de las reglas de evolución en las regiones, el diseño de nuevas arquitecturas que mejoren las comunicaciones entre las diferentes membranas (regiones) que componen el sistema y la implantación de estos sistemas en dispositivos hardware que pudiesen definir futuras máquinas basadas en este modelo. Dentro de este último campo, es decir, dentro del objetivo de construir finalmente máquinas que puedan llevar a cabo la funcionalidad de la computación con Sistemas P, la presente tesis doctoral se centra en el diseño de dos procesadores paralelos que, aplicando variantes de algoritmos existentes, favorezcan el crecimiento en el nivel de intra-paralelismo a la hora de aplicar las reglas. El diseño y creación de ambos procesadores presentan novedosas aportaciones al entorno de investigación de los Sistemas P de Transición en tanto en cuanto se utilizan conceptos que aunque previamente definidos de manera teórica, no habían sido introducidos en el hardware diseñado para estos sistemas. Así, los dos procesadores mantienen las siguientes características: - Presentan un alto rendimiento en la fase de aplicación de reglas, manteniendo por otro lado una flexibilidad y escalabilidad medias que son dependientes de la tecnología final sobre la que se sinteticen dichos procesadores. - Presentan un alto nivel de intra-paralelismo en las regiones al permitir la aplicación simultánea de reglas. - Tienen carácter universal en tanto en cuanto no depende del carácter de las reglas que componen el Sistema P. - Tienen un comportamiento indeterminista que es inherente a la propia naturaleza de estos sistemas. El primero de los circuitos utiliza el conjunto potencia del conjunto de reglas de aplicación así como el concepto de máxima aplicabilidad para favorecer el intra-paralelismo y el segundo incluye, además, el concepto de dominio de aplicabilidad para determinar el conjunto de reglas que son aplicables en cada momento con los recursos existentes. Ambos procesadores se diseñan y se prueban mediante herramientas de diseño electrónico y se preparan para ser sintetizados sobre FPGAs. ABSTRACT Membrane computing appears as an alternative to traditional computing. P Systems are placed inside this field and they are based upon the existence of regions called “membranes” that contain resources and rules that describe how the resources may vary to take each of these regions to a new situation called "configuration". Successive configurations conform computation. Inside this field, the Natural Computing Group of the Universidad Politécnica of Madrid develops a large number of works and researches that provide a lot of papers and some doctoral theses. Main research lines have been, by the moment, the study of the theoretical model over which Transition P Systems are defined, the study of the algorithms that are used for the evolution rules application in the regions, the design of new architectures that may improve communication among the different membranes (regions) that compose the whole system and the implementation of such systems over hardware devices that may define machines based upon this new model. Within this last research field, this is, within the objective of finally building machines that may accomplish the functionality of computation with P Systems, the present thesis is centered on the design of two parallel processors that, applying several variants of some known algorithms, improve the level of the internal parallelism at the evolution rule application phase. Design and creation of both processors present innovations to the field of Transition P Systems research because they use concepts that, even being known before, were never used for circuits that implement the applying phase of evolution rules. So, both processors present the following characteristics: - They present a very high performance during the application rule phase, keeping, on the other hand, a level of flexibility and scalability that, even known it is not very high, it seems to be acceptable. - They present a very high level of internal parallelism inside the regions, allowing several rule to be applied at the same time. - They present a universal character meaning this that they are not dependent upon the active rules that compose the P System. - They have a non-deterministic behavior that is inherent to this systems nature. The first processor uses the concept of "power set of the application rule set" and the concept of "maximal application" number to improve parallelism, and the second one includes, besides the previous ones, the concept of "applicability domain" to determine the set of rules that may be applied in each moment with the existing resources.. Both processors are designed and tested with the design software by Altera Corporation and they are ready to be synthetized over FPGAs.

Modelo de concurrencia de ADA: implementación y sus implicaciones en el interfaz con el entorno

El principal problema que impide actualmente una mayor utilización de las máquinas paralelas es la falta de herramientas de programación que permitan generar programas transportables a máquinas con diferentes prestaciones. En este trabajo se ha estudiado si los lenguajes con paralelismo explícito cumplen este requisito y son, por lo tanto, adecuados para programar este tipo de máquinas. El exceso de paralelismo, esto es, el uso de mayor paralelismo en el programa que el proporcionado por la máquina para esconder la latencia en la comunicación, se presenta en este trabajo como una solución a los problemas de eficiencia de los programas con paralelismo explícito cuando se ejecutan en máquinas que no tienen una granularidad adecuada. Con esta técnica, por lo tanto, los programas escritos con estos lenguajes pueden transportarse con eficiencia a diferentes máquinas. Para llevar a cabo el estudio de los lenguajes con paralelismo explícito, se ha desarrollado un modelo abstracto de paralelismo, en el cual un sistema está formado por una jerarquía de máquinas virtuales paralelas. Este modelo permite realizar un análisis genérico de la implementación de este tipo de lenguajes, ya sea sobre una máquina con sistema operativo o directamente sobre la máquina física. Este análisis genérico se ha aplicado a un lenguaje de este tipo, el lenguaje Ada. Se han estudiado las características específicas de Ada que pueden influir en la implementación eficiente del lenguaje, analizando también la propuesta de modificación del lenguaje correspondiente al proceso de revisión Ada 9X. Dentro del marco del modelo de paralelismo, se analiza también la problemática específica de las implementaciones del lenguaje sobre el sistema operativo. En este tipo de implementaciones, las interacciones de un programa con el entorno externo pueden causar ciertos problemas, como el bloqueo del proceso correspondiente del sistema operativo, que disminuyen el rendimiento del programa. Se analizan estos problemas y se proponen soluciones a los mismos. Se desarrolla en profundidad un ejemplo de este tipo de problemas: El acceso al estándar gráfico GKS desde Ada.---ABSTRACT---The major obstacle to the widespread utilization of the parallel machines is the lack of programming tools allowing the development of software portable between machines with different performance. This dissertation analyzes whether languages with explicit parallelism fulfil this requirement. The approach of using programs with more parallelism than available on the machine (parallel slackness) is presented. This technique can solve the efficiency problems appearing in the execution of programs with explicit parallelism over machines with a too coarse granularity. Therefore, with this approach programs can run efficiently on different machines. A new abstract model of parallelism allowing the generic study of the implementation of languages with explicit parallelism is developed. In this model, a parallel system is described by a hierarchy of parallel virtual machines. This generic analysis is applied to Ada language. Ada specific features with problematic implementation are identified and analyzed. The change proposals to Ada language in the frame of Ada 9X revisión process are also analyzed. The specific problematic of the language implementation on top of the operating system is studied under the scope of the parallelism model. With this kind of implementation, program interactions with extemal environments can lead to problems, like the blocking of the corresponding operating system process, decreasing the program execution performance. A practical example of this kind of problems, the access to GKS (Graphic Kernel System) from Ada programs, is analyzed and the implemented solution is described.

Distributed Estimation of Distribution Algorithms for continuous optimization: how does the exchanged information influence their behavior?

One of the most promising areas in which probabilistic graphical models have shown an incipient activity is the field of heuristic optimization and, in particular, in Estimation of Distribution Algorithms. Due to their inherent parallelism, different research lines have been studied trying to improve Estimation of Distribution Algorithms from the point of view of execution time and/or accuracy. Among these proposals, we focus on the so-called distributed or island-based models. This approach defines several islands (algorithms instances) running independently and exchanging information with a given frequency. The information sent by the islands can be either a set of individuals or a probabilistic model. This paper presents a comparative study for a distributed univariate Estimation of Distribution Algorithm and a multivariate version, paying special attention to the comparison of two alternative methods for exchanging information, over a wide set of parameters and problems ? the standard benchmark developed for the IEEE Workshop on Evolutionary Algorithms and other Metaheuristics for Continuous Optimization Problems of the ISDA 2009 Conference. Several analyses from different points of view have been conducted to analyze both the influence of the parameters and the relationships between them including a characterization of the configurations according to their behavior on the proposed benchmark.

Conditions for perfect focusing multiple point sources with the SMS design method

In this work, we demonstrate how it is possible to sharply image multiple object points. The Simultaneous Multiple Surface (SMS) design method has usually been presented as a method to couple N wave-front pairs with N surfaces, but recent findings show that when using N surfaces, we can obtain M image points when Nparallelism, and getting to the designs of six surfaces imaging up to eight object points. These designs are limited with the condition that the surfaces cannot be placed at the aperture stop. In the process of maximizing the object points to sharp image, we try to exhaust the degrees of freedom of aspherics and free-forms. We conjecture that maximal SMS designs are very close to a good solution, hence using them as a starting point for the optimization will lead us faster to a final optical system. We suggest here different optimization strategies which combined with the SMS method are proven to give the best solution. Through the example of imaging with the high aspect ratio, we compare the results obtained optimizing the rotational lens and using a combination of SMS method and optimization, showing that the second approach is giving significantly smaller value of overall RMS spot diameter.

Modelo de computación conexionista inspirado en las redes de procesadores evolutivos y su aprendizaje

La informática teórica es una disciplina básica ya que la mayoría de los avances en informática se sustentan en un sólido resultado de esa materia. En los últimos a~nos debido tanto al incremento de la potencia de los ordenadores, como a la cercanía del límite físico en la miniaturización de los componentes electrónicos, resurge el interés por modelos formales de computación alternativos a la arquitectura clásica de von Neumann. Muchos de estos modelos se inspiran en la forma en la que la naturaleza resuelve eficientemente problemas muy complejos. La mayoría son computacionalmente completos e intrínsecamente paralelos. Por este motivo se les está llegando a considerar como nuevos paradigmas de computación (computación natural). Se dispone, por tanto, de un abanico de arquitecturas abstractas tan potentes como los computadores convencionales y, a veces, más eficientes: alguna de ellas mejora el rendimiento, al menos temporal, de problemas NPcompletos proporcionando costes no exponenciales. La representación formal de las redes de procesadores evolutivos requiere de construcciones, tanto independientes, como dependientes del contexto, dicho de otro modo, en general una representación formal completa de un NEP implica restricciones, tanto sintácticas, como semánticas, es decir, que muchas representaciones aparentemente (sintácticamente) correctas de casos particulares de estos dispositivos no tendrían sentido porque podrían no cumplir otras restricciones semánticas. La aplicación de evolución gramatical semántica a los NEPs pasa por la elección de un subconjunto de ellos entre los que buscar los que solucionen un problema concreto. En este trabajo se ha realizado un estudio sobre un modelo inspirado en la biología celular denominado redes de procesadores evolutivos [55, 53], esto es, redes cuyos nodos son procesadores muy simples capaces de realizar únicamente un tipo de mutación puntual (inserción, borrado o sustitución de un símbolo). Estos nodos están asociados con un filtro que está definido por alguna condición de contexto aleatorio o de pertenencia. Las redes están formadas a lo sumo de seis nodos y, teniendo los filtros definidos por una pertenencia a lenguajes regulares, son capaces de generar todos los lenguajes enumerables recursivos independientemente del grafo subyacente. Este resultado no es sorprendente ya que semejantes resultados han sido documentados en la literatura. Si se consideran redes con nodos y filtros definidos por contextos aleatorios {que parecen estar más cerca a las implementaciones biológicas{ entonces se pueden generar lenguajes más complejos como los lenguajes no independientes del contexto. Sin embargo, estos mecanismos tan simples son capaces de resolver problemas complejos en tiempo polinomial. Se ha presentado una solución lineal para un problema NP-completo, el problema de los 3-colores. Como primer aporte significativo se ha propuesto una nueva dinámica de las redes de procesadores evolutivos con un comportamiento no determinista y masivamente paralelo [55], y por tanto todo el trabajo de investigación en el área de la redes de procesadores se puede trasladar a las redes masivamente paralelas. Por ejemplo, las redes masivamente paralelas se pueden modificar de acuerdo a determinadas reglas para mover los filtros hacia las conexiones. Cada conexión se ve como un canal bidireccional de manera que los filtros de entrada y salida coinciden. A pesar de esto, estas redes son computacionalmente completas. Se pueden también implementar otro tipo de reglas para extender este modelo computacional. Se reemplazan las mutaciones puntuales asociadas a cada nodo por la operación de splicing. Este nuevo tipo de procesador se denomina procesador splicing. Este modelo computacional de Red de procesadores con splicing ANSP es semejante en cierto modo a los sistemas distribuidos en tubos de ensayo basados en splicing. Además, se ha definido un nuevo modelo [56] {Redes de procesadores evolutivos con filtros en las conexiones{ , en el cual los procesadores tan solo tienen reglas y los filtros se han trasladado a las conexiones. Dicho modelo es equivalente, bajo determinadas circunstancias, a las redes de procesadores evolutivos clásicas. Sin dichas restricciones el modelo propuesto es un superconjunto de los NEPs clásicos. La principal ventaja de mover los filtros a las conexiones radica en la simplicidad de la modelización. Otras aportaciones de este trabajo ha sido el dise~no de un simulador en Java [54, 52] para las redes de procesadores evolutivos propuestas en esta Tesis. Sobre el término "procesador evolutivo" empleado en esta Tesis, el proceso computacional descrito aquí no es exactamente un proceso evolutivo en el sentido Darwiniano. Pero las operaciones de reescritura que se han considerado pueden interpretarse como mutaciones y los procesos de filtrado se podrían ver como procesos de selección. Además, este trabajo no abarca la posible implementación biológica de estas redes, a pesar de ser de gran importancia. A lo largo de esta tesis se ha tomado como definición de la medida de complejidad para los ANSP, una que denotaremos como tama~no (considerando tama~no como el número de nodos del grafo subyacente). Se ha mostrado que cualquier lenguaje enumerable recursivo L puede ser aceptado por un ANSP en el cual el número de procesadores está linealmente acotado por la cardinalidad del alfabeto de la cinta de una máquina de Turing que reconoce dicho lenguaje L. Siguiendo el concepto de ANSP universales introducido por Manea [65], se ha demostrado que un ANSP con una estructura de grafo fija puede aceptar cualquier lenguaje enumerable recursivo. Un ANSP se puede considerar como un ente capaz de resolver problemas, además de tener otra propiedad relevante desde el punto de vista práctico: Se puede definir un ANSP universal como una subred, donde solo una cantidad limitada de parámetros es dependiente del lenguaje. La anterior característica se puede interpretar como un método para resolver cualquier problema NP en tiempo polinomial empleando un ANSP de tama~no constante, concretamente treinta y uno. Esto significa que la solución de cualquier problema NP es uniforme en el sentido de que la red, exceptuando la subred universal, se puede ver como un programa; adaptándolo a la instancia del problema a resolver, se escogerín los filtros y las reglas que no pertenecen a la subred universal. Un problema interesante desde nuestro punto de vista es el que hace referencia a como elegir el tama~no optimo de esta red.---ABSTRACT---This thesis deals with the recent research works in the area of Natural Computing {bio-inspired models{, more precisely Networks of Evolutionary Processors first developed by Victor Mitrana and they are based on P Systems whose father is Georghe Paun. In these models, they are a set of processors connected in an underlying undirected graph, such processors have an object multiset (strings) and a set of rules, named evolution rules, that transform objects inside processors[55, 53],. These objects can be sent/received using graph connections provided they accomplish constraints defined at input and output filters processors have. This symbolic model, non deterministic one (processors are not synchronized) and massive parallel one[55] (all rules can be applied in one computational step) has some important properties regarding solution of NP-problems in lineal time and of course, lineal resources. There are a great number of variants such as hybrid networks, splicing processors, etc. that provide the model a computational power equivalent to Turing machines. The origin of networks of evolutionary processors (NEP for short) is a basic architecture for parallel and distributed symbolic processing, related to the Connection Machine as well as the Logic Flow paradigm, which consists of several processors, each of them being placed in a node of a virtual complete graph, which are able to handle data associated with the respective node. All the nodes send simultaneously their data and the receiving nodes handle also simultaneously all the arriving messages, according to some strategies. In a series of papers one considers that each node may be viewed as a cell having genetic information encoded in DNA sequences which may evolve by local evolutionary events, that is point mutations. Each node is specialized just for one of these evolutionary operations. Furthermore, the data in each node is organized in the form of multisets of words (each word appears in an arbitrarily large number of copies), and all the copies are processed in parallel such that all the possible events that can take place do actually take place. Obviously, the computational process just described is not exactly an evolutionary process in the Darwinian sense. But the rewriting operations we have considered might be interpreted as mutations and the filtering process might be viewed as a selection process. Recombination is missing but it was asserted that evolutionary and functional relationships between genes can be captured by taking only local mutations into consideration. It is clear that filters associated with each node allow a strong control of the computation. Indeed, every node has an input and output filter; two nodes can exchange data if it passes the output filter of the sender and the input filter of the receiver. Moreover, if some data is sent out by some node and not able to enter any node, then it is lost. In this paper we simplify the ANSP model considered in by moving the filters from the nodes to the edges. Each edge is viewed as a two-way channel such that the input and output filters coincide. Clearly, the possibility of controlling the computation in such networks seems to be diminished. For instance, there is no possibility to loose data during the communication steps. In spite of this and of the fact that splicing is not a powerful operation (remember that splicing systems generates only regular languages) we prove here that these devices are computationally complete. As a consequence, we propose characterizations of two complexity classes, namely NP and PSPACE, in terms of accepting networks of restricted splicing processors with filtered connections. We proposed a uniform linear time solution to SAT based on ANSPFCs with linearly bounded resources. This solution should be understood correctly: we do not solve SAT in linear time and space. Since any word and auxiliary word appears in an arbitrarily large number of copies, one can generate in linear time, by parallelism and communication, an exponential number of words each of them having an exponential number of copies. However, this does not seem to be a major drawback since by PCR (Polymerase Chain Reaction) one can generate an exponential number of identical DNA molecules in a linear number of reactions. It is worth mentioning that the ANSPFC constructed above remains unchanged for any instance with the same number of variables. Therefore, the solution is uniform in the sense that the network, excepting the input and output nodes, may be viewed as a program according to the number of variables, we choose the filters, the splicing words and the rules, then we assign all possible values to the variables, and compute the formula.We proved that ANSP are computationally complete. Do the ANSPFC remain still computationally complete? If this is not the case, what other problems can be eficiently solved by these ANSPFCs? Moreover, the complexity class NP is exactly the class of all languages decided by ANSP in polynomial time. Can NP be characterized in a similar way with ANSPFCs?

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.

Securing implementations of feedback-shift-register-based ciphers using compiler optimizations and co-processors

Los algoritmos basados en registros de desplazamiento con realimentación (en inglés FSR) se han utilizado como generadores de flujos pseudoaleatorios en aplicaciones con recursos limitados como los sistemas de apertura sin llave. Se considera canal primario a aquel que se utiliza para realizar una transmisión de información. La aparición de los ataques de canal auxiliar (en inglés SCA), que explotan información filtrada inintencionadamente a través de canales laterales como el consumo, las emisiones electromagnéticas o el tiempo empleado, supone una grave amenaza para estas aplicaciones, dado que los dispositivos son accesibles por un atacante. El objetivo de esta tesis es proporcionar un conjunto de protecciones que se puedan aplicar de forma automática y que utilicen recursos ya disponibles, evitando un incremento sustancial en los costes y alargando la vida útil de aplicaciones que puedan estar desplegadas. Explotamos el paralelismo existente en algoritmos FSR, ya que sólo hay 1 bit de diferencia entre estados de rondas consecutivas. Realizamos aportaciones en tres niveles: a nivel de sistema, utilizando un coprocesador reconfigurable, a través del compilador y a nivel de bit, aprovechando los recursos disponibles en el procesador. Proponemos un marco de trabajo que nos permite evaluar implementaciones de un algoritmo incluyendo los efectos introducidos por el compilador considerando que el atacante es experto. En el campo de los ataques, hemos propuesto un nuevo ataque diferencial que se adapta mejor a las condiciones de las implementaciones software de FSR, en las que el consumo entre rondas es muy similar. SORU2 es un co-procesador vectorial reconfigurable propuesto para reducir el consumo energético en aplicaciones con paralelismo y basadas en el uso de bucles. Proponemos el uso de SORU2, además, para ejecutar algoritmos basados en FSR de forma segura. Al ser reconfigurable, no supone un sobrecoste en recursos, ya que no está dedicado en exclusiva al algoritmo de cifrado. Proponemos una configuración que ejecuta múltiples algoritmos de cifrado similares de forma simultánea, con distintas implementaciones y claves. A partir de una implementación sin protecciones, que demostramos que es completamente vulnerable ante SCA, obtenemos una implementación segura a los ataques que hemos realizado. A nivel de compilador, proponemos un mecanismo para evaluar los efectos de las secuencias de optimización del compilador sobre una implementación. El número de posibles secuencias de optimizaciones de compilador es extremadamente alto. El marco de trabajo propuesto incluye un algoritmo para la selección de las secuencias de optimización a considerar. Debido a que las optimizaciones del compilador transforman las implementaciones, se pueden generar automáticamente implementaciones diferentes combinamos para incrementar la seguridad ante SCA. Proponemos 2 mecanismos de aplicación de estas contramedidas, que aumentan la seguridad de la implementación original sin poder considerarse seguras. Finalmente hemos propuesto la ejecución paralela a nivel de bit del algoritmo en un procesador. Utilizamos la forma algebraica normal del algoritmo, que automáticamente se paraleliza. La implementación sobre el algoritmo evaluado mejora en rendimiento y evita que se filtre información por una ejecución dependiente de datos. Sin embargo, es más vulnerable ante ataques diferenciales que la implementación original. Proponemos una modificación del algoritmo para obtener una implementación segura, descartando parcialmente ejecuciones del algoritmo, de forma aleatoria. Esta implementación no introduce una sobrecarga en rendimiento comparada con las implementaciones originales. En definitiva, hemos propuesto varios mecanismos originales a distintos niveles para introducir aleatoridad en implementaciones de algoritmos FSR sin incrementar sustancialmente los recursos necesarios. ABSTRACT Feedback Shift Registers (FSR) have been traditionally used to implement pseudorandom sequence generators. These generators are used in Stream ciphers in systems with tight resource constraints, such as Remote Keyless Entry. When communicating electronic devices, the primary channel is the one used to transmit the information. Side-Channel Attack (SCA) use additional information leaking from the actual implementation, including power consumption, electromagnetic emissions or timing information. Side-Channel Attacks (SCA) are a serious threat to FSR-based applications, as an attacker usually has physical access to the devices. The main objective of this Ph.D. thesis is to provide a set of countermeasures that can be applied automatically using the available resources, avoiding a significant cost overhead and extending the useful life of deployed systems. If possible, we propose to take advantage of the inherent parallelism of FSR-based algorithms, as the state of a FSR differs from previous values only in 1-bit. We have contributed in three different levels: architecture (using a reconfigurable co-processor), using compiler optimizations, and at bit level, making the most of the resources available at the processor. We have developed a framework to evaluate implementations of an algorithm including the effects introduced by the compiler. We consider the presence of an expert attacker with great knowledge on the application and the device. Regarding SCA, we have presented a new differential SCA that performs better than traditional SCA on software FSR-based algorithms, where the leaked values are similar between rounds. SORU2 is a reconfigurable vector co-processor. It has been developed to reduce energy consumption in loop-based applications with parallelism. In addition, we propose its use for secure implementations of FSR-based algorithms. The cost overhead is discarded as the co-processor is not exclusively dedicated to the encryption algorithm. We present a co-processor configuration that executes multiple simultaneous encryptions, using different implementations and keys. From a basic implementation, which is proved to be vulnerable to SCA, we obtain an implementation where the SCA applied were unsuccessful. At compiler level, we use the framework to evaluate the effect of sequences of compiler optimization passes on a software implementation. There are many optimization passes available. The optimization sequences are combinations of the available passes. The amount of sequences is extremely high. The framework includes an algorithm for the selection of interesting sequences that require detailed evaluation. As existing compiler optimizations transform the software implementation, using different optimization sequences we can automatically generate different implementations. We propose to randomly switch between the generated implementations to increase the resistance against SCA.We propose two countermeasures. The results show that, although they increase the resistance against SCA, the resulting implementations are not secure. At bit level, we propose to exploit bit level parallelism of FSR-based implementations using pseudo bitslice implementation in a wireless node processor. The bitslice implementation is automatically obtained from the Algebraic Normal Form of the algorithm. The results show a performance improvement, avoiding timing information leakage, but increasing the vulnerability against differential SCA.We provide a secure version of the algorithm by randomly discarding part of the data obtained. The overhead in performance is negligible when compared to the original implementations. To summarize, we have proposed a set of original countermeasures at different levels that introduce randomness in FSR-based algorithms avoiding a heavy overhead on the resources required.

La Guerra de las Galaxias como metodología innovadora para mejorar la motivación

Numerosos estudiantes ven el estudio como algo aburrido, se sienten desmotivados. El docente no puede limitarse a aceptar la situación como un espectador. Es nuestra realidad y de la misma forma que cada estudiante debe responsabilizarse de su propia educación, los profesores tenemos que responsabilizarnos de cambiar ese sentimiento. Para ello se analizará en primer lugar el significado del término motivación y cuáles son los factores en los que los profesores podemos influir. Se verá que una de las formas de intervención es la innovación, por lo que también se analizará el vocablo y se discutirá qué constituye innovación y qué no. Por tanto, el docente se enfrenta a diario con la necesidad de encontrar nuevas formas de enseñar, que capten la atención de los alumnos. Se dice que no hay nada nuevo bajo el sol; sin embargo, hay que ser capaz de encontrar nuevos usos a con recursos que ya existen. Con el presente trabajo se pretende dar respuesta a esa necesidad. Se plantea el uso de una metodología que propone una innovación continua que consiste en establecer un paralelismo entre un relato o una historia y una unidad didáctica de la asignatura de Tecnología. Como historia se ha escogido la conocida película “La Guerra de las Galaxias” y el curso de referencia será el primer curso de Educación Secundaria Obligatoria (1º E.S.O.). En concreto se presenta un material adaptado con fotografías de la película, ejemplos inspirados en la saga y otras adaptaciones educativas. Con ello se consigue una sorpresa continua para el estudiante y así mantener su atención, facilitando su aprendizaje. Se tiene hecho parte del camino, aunque no todo. En este punto, se hace necesario introducir algunas medidas suplementarias, que refuercen y complementen esta metodología y que nos impidan apartarnos del objetivo pretendido: que los alumnos aprendan de manera significativa. ¿Quién dijo que estudiar es aburrido? A number of students see studying as something boring. The teacher cannot be a spectator. It is our reality and, so on one hand, the student has the responsibility of building his education and on the other, the teacher must change that feeling. In order to this, the term motivation will be analysed, and also which are the related aspects in which we have some influence. One of those ways of intervention is motivation. It is for that word, innovation will be analysed as well, discussing what innovation is and what is not. Therefore, teachers face, day by day, the need of finding new ways of teaching for students to pay attention in classes. As people say, there is nothing new under the sun; however, new uses for existing resources are required. This paper pretends to solve that problem. A continuous innovating methodology is set, consisting in establishing a parallelism between a story or tale and a didactic unit in Technology subject. As a story, the well-known film “Star Wars” is chosen, and as a reference course, the first course of Educación Secundaria Obligatoria (1st E.S.O.). Specifically, we introduce an adapted material with pictures from the movie, saga inspired examples and, some other educational adaptations. With it, students are continuously surprised and their attention grabbed, making his learning easier. Part of the problem is solved, but there is a long way to go. At this point, some supplementary steps are needed, in order to enforce and complement this methodology, and to avoid getting far away from the attempted objective: students learning in a significant way. Who said studying is annoying?

Efficient parallelization of a regional ocean model for the western Mediterranean Sea

This paper focuses on the parallelization of an ocean model applying current multicore processor-based cluster architectures to an irregular computational mesh. The aim is to maximize the efficiency of the computational resources used. To make the best use of the resources offered by these architectures, this parallelization has been addressed at all the hardware levels of modern supercomputers: firstly, exploiting the internal parallelism of the CPU through vectorization; secondly, taking advantage of the multiple cores of each node using OpenMP; and finally, using the cluster nodes to distribute the computational mesh, using MPI for communication within the nodes. The speedup obtained with each parallelization technique as well as the combined overall speedup have been measured for the western Mediterranean Sea for different cluster configurations, achieving a speedup factor of 73.3 using 256 processors. The results also show the efficiency achieved in the different cluster nodes and the advantages obtained by combining OpenMP and MPI versus using only OpenMP or MPI. Finally, the scalability of the model has been analysed by examining computation and communication times as well as the communication and synchronization overhead due to parallelization.

Parallel Computer Vision Algorithms for Graphics Processing Units

La evolución de los teléfonos móviles inteligentes, dotados de cámaras digitales, está provocando una creciente demanda de aplicaciones cada vez más complejas que necesitan algoritmos de visión artificial en tiempo real; puesto que el tamaño de las señales de vídeo no hace sino aumentar y en cambio el rendimiento de los procesadores de un solo núcleo se ha estancado, los nuevos algoritmos que se diseñen para visión artificial han de ser paralelos para poder ejecutarse en múltiples procesadores y ser computacionalmente escalables. Una de las clases de procesadores más interesantes en la actualidad se encuentra en las tarjetas gráficas (GPU), que son dispositivos que ofrecen un alto grado de paralelismo, un excelente rendimiento numérico y una creciente versatilidad, lo que los hace interesantes para llevar a cabo computación científica. En esta tesis se exploran dos aplicaciones de visión artificial que revisten una gran complejidad computacional y no pueden ser ejecutadas en tiempo real empleando procesadores tradicionales. En cambio, como se demuestra en esta tesis, la paralelización de las distintas subtareas y su implementación sobre una GPU arrojan los resultados deseados de ejecución con tasas de refresco interactivas. Asimismo, se propone una técnica para la evaluación rápida de funciones de complejidad arbitraria especialmente indicada para su uso en una GPU. En primer lugar se estudia la aplicación de técnicas de síntesis de imágenes virtuales a partir de únicamente dos cámaras lejanas y no paralelas—en contraste con la configuración habitual en TV 3D de cámaras cercanas y paralelas—con información de color y profundidad. Empleando filtros de mediana modificados para la elaboración de un mapa de profundidad virtual y proyecciones inversas, se comprueba que estas técnicas son adecuadas para una libre elección del punto de vista. Además, se demuestra que la codificación de la información de profundidad con respecto a un sistema de referencia global es sumamente perjudicial y debería ser evitada. Por otro lado se propone un sistema de detección de objetos móviles basado en técnicas de estimación de densidad con funciones locales. Este tipo de técnicas es muy adecuada para el modelado de escenas complejas con fondos multimodales, pero ha recibido poco uso debido a su gran complejidad computacional. El sistema propuesto, implementado en tiempo real sobre una GPU, incluye propuestas para la estimación dinámica de los anchos de banda de las funciones locales, actualización selectiva del modelo de fondo, actualización de la posición de las muestras de referencia del modelo de primer plano empleando un filtro de partículas multirregión y selección automática de regiones de interés para reducir el coste computacional. Los resultados, evaluados sobre diversas bases de datos y comparados con otros algoritmos del estado del arte, demuestran la gran versatilidad y calidad de la propuesta. Finalmente se propone un método para la aproximación de funciones arbitrarias empleando funciones continuas lineales a tramos, especialmente indicada para su implementación en una GPU mediante el uso de las unidades de filtraje de texturas, normalmente no utilizadas para cómputo numérico. La propuesta incluye un riguroso análisis matemático del error cometido en la aproximación en función del número de muestras empleadas, así como un método para la obtención de una partición cuasióptima del dominio de la función para minimizar el error. ABSTRACT The evolution of smartphones, all equipped with digital cameras, is driving a growing demand for ever more complex applications that need to rely on real-time computer vision algorithms. However, video signals are only increasing in size, whereas the performance of single-core processors has somewhat stagnated in the past few years. Consequently, new computer vision algorithms will need to be parallel to run on multiple processors and be computationally scalable. One of the most promising classes of processors nowadays can be found in graphics processing units (GPU). These are devices offering a high parallelism degree, excellent numerical performance and increasing versatility, which makes them interesting to run scientific computations. In this thesis, we explore two computer vision applications with a high computational complexity that precludes them from running in real time on traditional uniprocessors. However, we show that by parallelizing subtasks and implementing them on a GPU, both applications attain their goals of running at interactive frame rates. In addition, we propose a technique for fast evaluation of arbitrarily complex functions, specially designed for GPU implementation. First, we explore the application of depth-image–based rendering techniques to the unusual configuration of two convergent, wide baseline cameras, in contrast to the usual configuration used in 3D TV, which are narrow baseline, parallel cameras. By using a backward mapping approach with a depth inpainting scheme based on median filters, we show that these techniques are adequate for free viewpoint video applications. In addition, we show that referring depth information to a global reference system is ill-advised and should be avoided. Then, we propose a background subtraction system based on kernel density estimation techniques. These techniques are very adequate for modelling complex scenes featuring multimodal backgrounds, but have not been so popular due to their huge computational and memory complexity. The proposed system, implemented in real time on a GPU, features novel proposals for dynamic kernel bandwidth estimation for the background model, selective update of the background model, update of the position of reference samples of the foreground model using a multi-region particle filter, and automatic selection of regions of interest to reduce computational cost. The results, evaluated on several databases and compared to other state-of-the-art algorithms, demonstrate the high quality and versatility of our proposal. Finally, we propose a general method for the approximation of arbitrarily complex functions using continuous piecewise linear functions, specially formulated for GPU implementation by leveraging their texture filtering units, normally unused for numerical computation. Our proposal features a rigorous mathematical analysis of the approximation error in function of the number of samples, as well as a method to obtain a suboptimal partition of the domain of the function to minimize approximation error.

AVALIAÇÃO DAS ALTERAÇÕES DO SORRISO EM INDIVÍDUOS SUBMETIDOS À EXPANSÃO RÁPIDA DA MAXILA

O objetivo deste estudo foi avaliar as possíveis alterações das características horizontais, verticais, de simetria e do arco do sorriso de pacientes com atresia maxilar submetidos à expansão rápida da maxila. A amostra consistiu de 81 fotografias extra-bucais do sorriso máximo de 27 pacientes com idade média de 10 anos e 3 meses. Foram realizadas fotografias do sorriso máximo nos períodos: inicial (antes da instalação do aparelho expansor); 3 meses após a fixação do parafuso expansor; 6 meses após a fixação do parafuso expansor. Para a calibragem e análise das fotografias foi utilizado o programa CEFX 2001 CDT. Os pontos fotométricos e as medidas a serem analisadas foram escolhidos após revisão da literatura do sorriso realizada. Para avaliar as alterações no sorriso durante as fases, foi utilizada a análise de variância ANOVA, com nível de significância de 5%. A expansão rápida da maxila promoveu aumento estatisticamente significante da dimensão transversal do sorriso; aumento da quantidade de exposição dos incisivos centrais e laterais superiores; manutenção da simetria entre os lados direito e esquerdo e da falta de paralelismo entre a curvatura das bordas dos incisivos superiores com a curvatura do lábio inferior (arco do sorriso).(AU)

AVALIAÇÃO DAS ALTERAÇÕES DO SORRISO EM INDIVÍDUOS SUBMETIDOS À EXPANSÃO RÁPIDA DA MAXILA

O objetivo deste estudo foi avaliar as possíveis alterações das características horizontais, verticais, de simetria e do arco do sorriso de pacientes com atresia maxilar submetidos à expansão rápida da maxila. A amostra consistiu de 81 fotografias extra-bucais do sorriso máximo de 27 pacientes com idade média de 10 anos e 3 meses. Foram realizadas fotografias do sorriso máximo nos períodos: inicial (antes da instalação do aparelho expansor); 3 meses após a fixação do parafuso expansor; 6 meses após a fixação do parafuso expansor. Para a calibragem e análise das fotografias foi utilizado o programa CEFX 2001 CDT. Os pontos fotométricos e as medidas a serem analisadas foram escolhidos após revisão da literatura do sorriso realizada. Para avaliar as alterações no sorriso durante as fases, foi utilizada a análise de variância ANOVA, com nível de significância de 5%. A expansão rápida da maxila promoveu aumento estatisticamente significante da dimensão transversal do sorriso; aumento da quantidade de exposição dos incisivos centrais e laterais superiores; manutenção da simetria entre os lados direito e esquerdo e da falta de paralelismo entre a curvatura das bordas dos incisivos superiores com a curvatura do lábio inferior (arco do sorriso).(AU)

Stretch-activated single K+ channels account for whole-cell currents elicited by swelling

Functionally significant stretch-activated ion channels have been clearly identified in excitable cells. Although single-channel studies suggest their expression in other cell types, their activity in the whole-cell configuration has not been shown. This discrepancy makes their physiological significance doubtful and suggests that their mechanical activation is artifactual. Possible roles for these molecules in nonexcitable cells are acute cell-volume regulation and, in epithelial cells, the complex adjustment of ion fluxes across individual cell membranes when the rate of transepithelial transport changes. We report the results of experiments on isolated epithelial cells expressing in the basolateral membrane stretch-activated K+ channels demonstrable by the cell-attached patch-clamp technique. In these cells, reversible whole-cell currents were elicited by both isosmotic and hyposmotic cell swelling. Cation selectivity and block by inorganic agents were the same for single-channel and whole-cell currents, indicating that the same entity underlies single-channel and whole-cell currents and that the single-channel events are not artifactual. In these cells, when the rate of apical-membrane NaCl entry increases, the cell Na+ content and volume also increase, stimulating the Na+,K+-ATPase at the basolateral membrane, i.e., both Na+ extrusion and K+ uptake increase. We speculate that, under these conditions, the parallel activation of basolateral K+ channels (by the swelling) elevates conductive K+ loss, tending to maintain the cell K+ content constant (“pump-leak parallelism”). This study describes a physiologically relevant stretch-activated channel, at both the single-channel and whole-cell levels, in a nonneural cell type.