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.

Sistema Integrado de Gestión Académica

El Sistema Integrado de Gestión Académica consiste en una plataforma software modular orientada a apoyar la labor del profesorado en la gestión docente de las asignaturas impartidas por el Departamento de Mecánica de la Escuela Técnica Superior de Ingeniería y Diseño Industrial de la Universidad Politécnica de Madrid. Durante los últimos 5 años se ha trabajado en la creación de esta plataforma que se encuentra ahora en su recta final. Es necesario aclarar que toda la plataforma desde su inicio ha sido creada por el mismo autor y que debido al tiempo disponible para la realización del TFG, éste se ha centrado en realizar mejoras sobre lo ya desarrollado y en implementar uno de los módulos. El trabajo desarrollado comienza con un estudio de plataformas educativas online. Se han valorado las alternativas de Moodle y ATutor como posibles soluciones a los requisitos planteados llegando a la conclusión de que era necesario realizar un desarrollo a medida. La plataforma consta de 3 módulos principales:  Plataforma de Gestión Docente en Internet (PGDNet)  Aplicación de Notas (AdN)  Plataforma de Entrega de Prácticas Académicas (PEPA) PGDNet está orientado a la realización de pruebas de evaluación online. El profesor tiene a su alcance un conjunto de opciones que le permiten la creación de actividades y ejercicios de diferente índole, gestionar alumnos y establecer periodos de evaluación. El sistema recoge los resultados y corrige automáticamente permitiendo además exportar los resultados, manteniendo de esta manera la compatibilidad con otros sistemas informáticos de la UPM. PGDNet ofrece además un servicio de correo electrónico para realizar comunicaciones con grupos predefinidos de alumnos, un gestor documental enlazado con las diferentes actividades y un gestor de encuestas programable a medida. AdN se integra en la plataforma como un sistema para la gestión de calificaciones y permite mantener un historial del alumno. Las materias pueden dividirse en diferentes evaluaciones con un determinado peso sobre la calificación final. La nota total se calcula en tiempo real y de forma automática. El alumno puede entrar a consultar sus calificaciones en cualquier momento. El módulo ofrece a los profesores acceso simultáneo a introducir las calificaciones e importar notas guardadas de convocatorias pasadas. PEPA es el nuevo módulo que se añade a la plataforma y el que concentra los esfuerzos de desarrollo de este TFG. Se trata de un sistema de entrega de prácticas online que permite al profesor centralizar la recogida de documentación para su posterior corrección. PEPA dispone de un sistema de plantillas de respuestas fijas utilizadas en los laboratorios que son corregidas de forma automática en la entrega. Los 3 módulos se complementan entre sí compartiendo datos y permitiendo realizar importaciones y exportaciones de información con las aplicaciones actuales de Secretaría de alumnos como puede ser la introducción de listas de alumnos.---ABSTRACT---Academic Management Framework (Sistema Integrado de Gestión Académica) is a module‐oriented software application that aims to help teachers from ETSIDI Department from UPM to manage all information related to graduate courses. The software, which has been in continuous developing during the last 5 years, is now about to be finished. It must be pointed out the fact that the entire application has been designed and implemented by the same author. However, due to time schedule restrictions in this TFG (spanish acronym for “Graduation Project”), it has been focused on developing a few improvements in the software already implemented and creating a specific new module. In the beginning, this TFG includes an educational software comparative study. Moodle and ATutor have been selected as plausible assembled solutions that would fit the requirements given. Nonetheless, the conclusion ends up with rejecting both possibilities and moving the project towards a custom‐developed software. The application is divided in 3 modules:  Network Based Academic Management Platform (Plataforma de Gestión Docente en Internet ‐ PGDNet)  Evaluation Aid Tool (Aplicación de Notas ‐ AdN)  Academic Lab‐Work Delivery Platform (Plataforma de Entrega de Prácticas Académicas ‐ PEPA) PGDNet main purpose is handling online tests for students. There are a bunch of tools available for teachers that allow them to create activities and different types of exercises, manage students and set examination schedules. The system gathers the results and marks exercises automatically. Moreover, the teacher is able to export this information which is compatible with other UPM systems. PGDNet offers a mail service, a document management system and a survey application among others. AdN adds new features to the system. It helps teachers to manage student marks by keeping a history over the years. Subjects can be divided into little parts with a different weight in the final mark. Eventually, the mark is automatically calculated and published. The application can be accessed by both students and teachers simultaneously. This module is also ready to import old marks into the current course and allow all teachers to fill in the results at the same time. PEPA, which is a new module added from scratch, concentrate this TFG efforts. It consists of a practice delivery system that gathers all student documentation in a single site for easy correction. Besides, PEPA deploys an answer template repository for laboratory training. Students fill the templates and PEPA corrects them automatically on sending. These 3 modules are integrated in a single system that allows them to share data and import information such as student lists from the Administration Department.

Posibilidades de cultivo de nuevas especies marinas en el área mediterránea

La acuicultura, el cultivo y cría de animales y plantas acuáticas, representa en la actualidad una fuente esencial de proteína animal y vegetal altamente saludable y nutritiva, proporcionando un sistema de vida y de ingresos en todo el mundo. La acuicultura además de ser un motor para el desarrollo social y económico de las áreas costeras marinas y fluviales mundiales, supone en muchas regiones subdesarrolladas una garantía de alimento de alta calidad y es clave en la seguridad alimentaria de sus poblaciones. El desarrollo de la acuicultura se ha realizado fundamentalmente en los últimos 50 años, y ha sido sobre todo en la década de los años 80, cuando la acuicultura ha experimentado un fuerte crecimiento con tasas anuales que superan el 6%. Con el estancamiento de la producción pesquera y el incremento de la población mundial, la acuicultura se presenta como la única fuente posible de suministro de proteínas (vegetales y animales) de alta calidad, ricas en aceites omega 3 (EPA y DHA) de origen acuático. En la actualidad la producción procedente de la acuicultura supera los 95 millones de toneladas anuales, siendo ligeramente superior a los 94 millones de toneladas anuales provenientes de la pesca extractiva. De este total mundial acuícola, la producción asiática representa el 89%, mientras que la europea el 4,2% Aunque el 46% de la producción mundial acuícola se concentra únicamente en solo 10 especies, una de las principales características de la acuicultura es la gran diversidad de especies cultivadas, más de 500, realizándose su cría bajo diferentes tecnologías y sistemas productivos. El ámbito de esta tesis, es únicamente la acuicultura marina que se desarrolla en las aguas del mar mediterráneo, indistintamente de los sistemas y tecnología de producción utilizados. Los principales grupos de cultivo que se realizan en las aguas del Mediterráneo son los moluscos y los peces, siendo muy escasos los cultivos de otros grupos como crustáceos y macroalgas. La piscicultura marina mediterránea está dominada por el cultivo en jaulas flotantes de dos especies, la dorada (Sparus auratus) y la lubina (Dicentrarchus labrax). Estas dos especies y tras 30 años de experiencia de cultivo, mantienen todavía una ineficiencia productiva alta (reducida selección genética, lento crecimiento hasta talla comercial, alto factor de conversón del pienso…) y además ocupan un estrecho nicho de mercado, ya que prácticamente toda la comercialización de la dorada y lubina se realiza en fresco y sin elaborar ni transformar, a una talla media de 500 g. Para dar respuesta desde la acuicultura mediterránea al alto consumo y a la creciente demanda que en la Unión Europea existe de los productos acuícolas, y en especial los productos elaborados y transformados, es necesario de manera urgente, un aumento de la producción de las especies ya cultivadas (dorada y lubina) mediante la mejora de su eficiencia productiva, al mismo tiempo que se debe iniciar la producción industrial de nuevas especies piscícolas, mediante la diversificación de los cultivos. Para llevar a cabo esta diversificación, se hace necesario el establecimiento de una metodología clara, que asegure una selección de especies apropiadas y rentables para la industria acuícola mediterránea, cuyo cultivo sostenible debiera cumplir con los desafíos que el sector tiene. Nuevas especies que complementen y cubran las demandas actuales y futuras del mercado Europeo e Internacional de productos acuícolas. Nuevas especies con parámetros productivos eficientes, que garanticen unos costes productivos competitivos. Nuevas especies que puedan ser cultivadas utilizando como base la tecnología de producción ya existente en el sector. El objetivo de esta tesis es la definición y desarrollo de una metodología sencilla para la selección de nuevas especies piscícolas marinas para su cultivo eficiente y sostenible Y bajo la aplicación de esta metodología, la selección de un grupo de especies piscícolas para su cultivo rentable a corto y medio plazo (6-8 años) en el Mediterráneo. Para ello se ha definido y aplicado una metodología con la que se han evaluado diez especies candidatas, previamente escogidas de una serie de listas previas originadas en los distintos estudios y trabajos de diversificación realizados con anterioridad por otros equipos de investigación. Estas especies candidatas han sido: Seriola dumerili. (Seriola) , Argyrosomus regius (Corvina), Polyprion americanus (Cherna), Ephinephelus marginatus (Mero), Dentex dentex (Dentón), Pagrus pagrus (Pargo), Solea senegalensis (Lenguado del Senegal), Thunnus thynnus (Atún rojo), Mugil cephalus (Lisa), Coryphaena hippurus (Lampuga). El conjunto de estas especies ocupa un amplio y variado espectro dentro de las distintas áreas de mercado, productiva, tecnológica, y medioambiental . Y en todas ellas existe una experiencia mínima en sus diferentes fases de cultivo. En el desarrollo de la metodología de selección, en esta tesis se han definido diversos parámetros de evaluación, considerados como los más significativos y sencillos de aplicar. Los parámetros se han agrupado en tres bloques, el comercial, el productivo y el medioambiental. El Bloque de Mercado, comprende aquellos criterios que están relacionados con la comercialización de la especie. Calidad de la carne del pescado. Competencia con otras especies en el mercado. Potencial de Transformado. Precio de venta del pescado. El bloque Medioambiental incluye criterios del grado de idoneidad de la especie en la región y del grado de impacto ambiental de su cultivo. Rango de temperaturas del agua óptimo para el cultivo. Potencial impacto ambiental de su cultivo. Eslabón trófico de la especie.. El bloque Productivo, engloba los criterios y parámetros relacionados con el nivel de conocimiento y control que sobre su cultivo existen ( larvario, engorde, tecnología) Grado de control de la fase larvaria. Disponibilidad de alevines en el sector Crecimiento. Factor de conversión Aprovechamiento de la capacidad productiva instalada, Coste de inversión. Previa a la evaluación se han descrito las principales características de las especies candidatas en función del estado y experiencia actual sus cultivos. En la aplicación de estos criterios se han establecido matrices de evaluación y a cada criterio se le ha asignado un valor diferente en función de sus características y propiedades selectivas. Los resultados obtenidos mediante la aplicación de la metodología de evaluación propuesta, han señalado la seriola y la corvina como especies más recomendadas para su puesta en cultivo en el Mediterráneo a corto y medio plazo. Las otras dos especies seleccionadas han sido la lisa y la lampuga. Como conclusión final podemos señalar que el cultivo de nuevas especies es fundamentalmente para el desarrollo sostenible de la acuicultura mediterránea. Esta diversificación debe basarse en la aplicación de una metodología sencilla y práctica, que garantice una selección de especies cuyo cultivo sea rentable y abarquen nuevos segmentos de mercado. ABSTRACT Aquaculture, the cultivation and breeding of aquatic animals and plants, currently represents an essential source of highly nutritious and healthy protein that provides a way of life and income all over the world. Apart from being a social and economic driver in coastal and marine areas, it also entails a guaranteed high quality nourishment in many undeveloped areas being key to the alimentary safety of their population. Aquaculture has developed mainly in the last 50 years and experienced a high growth especially during the Eighties when the annual rates were above 6%. With fishing production stagnating and the global population increasing, aquaculture emerges as the only possible animal and vegetable protein source of aquatic origin, high in quality and omega 3 oils (EPA and DHA). Here and now, aquaculture production is over 95 million tons per year, which is slightly higher than the 94 million tons per year that come from extractive fisheries. From this aquaculture total, Asiatic production represents 89% while Europe´s is only 4.2%. Even though 46% of the global aquaculture production focuses just on 10 species, one of the main characteristics of aquaculture is the wide diversity of cultivated species –over 500– using different technologies and production systems. This PhD’s scope is only marine aquaculture in Mediterranean water, regardless of the technology or systems used. The main crop groups in the Mediterranean sea are molluscs and finfish, while crustacean and macroalgae cultivations are very limited. Mediterranean fish culture is dominated by the cultivation in floating cages of two species: Bream (Sparus auratus) and Bass (Dicentrarchus labrax). After 30 years of farming, these two species still keep a high productive inefficiency –reduced genetic selection, slow growth to marketable size, high feed conversion rate– and fill a narrow niche market as practically all bream and bass is sold fresh and whole, unprocessed and untransformed, with an average size of 500 grams. To meet the high consumption and growing demand of aquaculture products, in the European Union (especially those prepared and transformed), Mediterranean aquaculture needs to urgently increase the production of the species already under cultivation (Bass and Bream) by means of improving its productive efficiency and at the same time begin initiating industrial production of new species by diversifying the cultivation. To carry out this diversification it is necessary to establish a clear methodology that ensures the selection of adapted and profitable species for the Mediterranean aquaculture industry. The sustainable farming of these new species needs to meet the challenges this sector faces: New species that complement and meet the current and future needs of the European and International markets for aquaculture products. New species with efficient production parameters that ensure competitive production costs. New species that can be cultivated using already existing production technologies. The aim of this PhD is to define and develop a simple methodology for the selection of new marine fish species for their efficient and sustainable cultivation. And by applying this methodology, to select a group of fish species for its profitable crop in the short and medium term (6-8 years) in the Mediterranean. For this, a methodology has been defined and applied evaluating ten candidate species selected from a series of lists originated from different studies and from diversification works previously conducted by other research teams. These candidate species are: Seriola dumerili. (Greater amberjack), Argyrosomus regius (Meagre), Polyprion americanus (Wreckfish), Ephinephelus marginatus (Dusky grouper), Dentex dentex (Common dentex), Pagrus pagrus (Red porgy), Solea senegalensis (Senegal sole), Thunnus thynnus (Bluefin tuna), Mugil cephalus (Grey mullet), Coryphaena hippurus (Dolphinfish). All these species occupy a broad and varied spectrum within different productive, technological and environmental market areas. There is minimal experience in their different stages of cultivation for all of them. While developing the selection methodology several evaluation parameters have been defined in this PhD, considered the most significant and simple to apply. The parameters are grouped in three blocks: commercial, productivity and environmental. Market block comprises criteria related to the marketing of the species. Quality of the fish meatCompetition with other species in the marketTransformation potentialFish selling price Environment block includes criteria related to the degree of suitability of the species in the region and the degree of environmental impact of their cultivation. Optimal water temperature range for cultivationPotential environmental impact of their cultivationTrophic chain level. Productivity block includes criteria and parameters related to the level of knowledge and control over their cultivation (larval, ongrowing, technology) Degree of control of the larval stageAvailability of alevin in the sector GrowthFeed conversion rate. Exploitation of installed capacityInvestment cost Prior to the evaluation, the main characteristics of the candidate species have been described based on the current status and experience of their cultivations. When applying these criteria evaluation matrices have been established assigning to each criteria a different value depending on their characteristics and selective properties. The results obtained by applying the proposed assessment methodology have identified the Greater Amberjack and Meagre as the most recommended species for farming in the Mediterranean in the short and medium term. The other two selected species were the Grey Mullet and the Dolphinfish. In conclusion, the cultivation of new species is crucial for the sustainable development of Mediterranean aquaculture. This diversification has to be based on the application of a simple and practical methodology that guarantees a selection of species whose cultivation is profitable and covers new market segments.

Aplicación móvil y web para la gestión de lugares geolocalizados

El proyecto “Aplicación móvil y web para la gestión de lugares geolocalizados (www.midiez.com)” tiene como objetivo principal crear un repositorio de listas categorizadas de sitios para su uso en el ámbito personal o comercial. Tanto la aplicación web como la aplicación móvil desarrollada en Android tienen el propósito de gestionar listas de lugares de interés (Restaurantes, tiendas,..) o con propósitos específicos (Organización de viajes) o simplemente como una forma de anotar aquellos sitios que nos comentan y que nos gustaría visitar. El desarrollo de este proyecto además permitirá contrastar las distintas alternativas y la evolución de las distintas herramientas que se han ido desarrollando para la gestión del ocio en los últimos años desde el sistema Android y plataformas web. Todo el proyecto ha sido realizado usando software libre (PHP para el lenguaje web servidor y Java para la programación móvil). La principal finalidad desde el punto de vista del desarrollador es: aprovechar las sinergias de la programación móvil y la programación web de manera que las mismas capas de negocio de Datos sean usadas por ambas plataformas. Asimismo crear una aplicación distribuida y fácilmente escalable. Las herramientas que se han usado para desarrollar han sido: la SDK proporcionada por Google, una JDK de Java y un IDE de desarrollo Java como es Eclipse y otro similar para el desarrollo de la parte PHP. La BBDD elegida ha sido MySQL. El proyecto pretende mostrar el potencial de las aplicaciones móviles geolocalizadas desde el punto de vista del ocio y compararlas con el estado del arte actual. Por lo tanto la mayor parte del tiempo dedicado al proyecto ha sido empleado en el desarrollo de la aplicación web, la aplicación móvil y en la base de datos pero también he dedicado una pequeña parte del trabajo para realizar un estudio sobre las consecuencias que esta tecnología está teniendo en nuestros cerebros. ABSTRACT The project "Web and Mobile App for managing geolocation places” has as main objective managing of places lists in order to use them in the leisure time scope. Nowadays the use of GPS is being a constant in mobile applications so that is already part of our daily life. We used to know where we are always and at the same time we can find locations using the technology of our mobile phones. Now it is very difficult to get lost outside but also is difficult to explain somebody how to get to anywhere without using Google Maps. Google Maps, Geolocation, gps navigators, … all that kind of stuff are making our life easier and less complicated but also are making our brains lazier. Furthermore, the development of this project will use the potential of locate places into maps to avoid annotate every spot we would like to visit or a brand new restaurant. The project itself shows the location features of Google Maps combined with an places data base in order to create, and manage places lists and use them to get to them as well as to share those places with our contacts. Also, the main purpose from the point of view of the developer is to combine different programming languages and use the resulting synergies in a easily scalable and portable environment. The tools that have been used to develop are: the SDK provided by Google, one JDK Java and Java development IDE such as Eclipse and similar to the development of the PHP part. The DB has been chosen MySQL. Finally, this project aims to show, from an educational point of view, the use and potential of this technology. Thus, it has been devoted a large amount of time of the project (and, consequently, its documentation) on develop the Android app, the data base and the web app but also but also to highlight the consequences of using technology.