Análisis de datos de periódicos digitales

En este proyecto se ha desarrollado una aplicación Web cuya finalidad es ofrecer al usuario datos provenientes del análisis de texto de las noticias que se encuentran en periódicos online. La aplicación permite al usuario realizar búsquedas personalizadas sobre temáticas específicas y configurar algunos tipos de análisis sobre la información recuperada. Entre los análisis que son llevados a cabo destaca el análisis del sentimiento. Para ello se ofrece la posibilidad de que el usuario utilice sus propios diccionarios de pares palabra-valor, utilizados para realizar este tipo de análisis. Para la codificación de la herramienta, se ha utilizado el lenguaje de programación Python y la framework web Django. El almacenamiento de la información de la aplicación se ha realizado sobre una base de datos NoSQL de tipo MongoDB.

Verificación de algoritmos y estructuras de datos en Dafny

La verificación formal de un programa es la demostración de que este funciona de acuerdo a una descripción del comportamiento esperado en toda posible ejecución. La especificación de lo deseado puede utilizar técnicas diversas y entrar en mayor o menor detalle, pero para ganarse el título de formal esta ha de ser matemáticamente rigurosa. El estudio y ejercicio manual de alguna de esas técnicas forma parte del currículo común a los estudios de grado de la Facultad de Informática y del itinerario de Ciencias de la Computación de la Facultad de Ciencias Matemáticas de la Universidad Complutense de Madrid, como es el caso de la verificación con pre- y postcondiciones o lógica de Hoare. En el presente trabajo se explora la automatización de estos métodos mediante el lenguaje y verificador Dafny, con el que se especifican y verifican algoritmos y estructuras de datos de diversa complejidad. Dafny es un lenguaje de programación diseñado para integrar la especificación y permitir la verificación automática de sus programas, con la ayuda del programador y de un demostrador de teoremas en la sombra. Dafny es un proyecto en desarrollo activo aunque suficientemente maduro, que genera programas ejecutables.

Generación automática de tests en DomJudge

Los jueces online están cobrando cada día más importancia, especialmente en el ámbito de la enseñanza. Su funciona-miento es simple, un juez/profesor sube un problema de programación con un enunciado y unos casos de prueba (entradas y salidas esperadas) al juez online. El alumno/concursante deberá subir el código que considera como solución al problema. Si el código del alumno devuelve las mismas salidas que las que se encuentran en los casos de prueba para las correspondientes entradas en los test-cases dada las mismas entradas, el código se considera correcto. En la Facultad de Informática de la Universidad Complutense de Madrid ha aparecido un juez virtual que cada vez está siendo más usado por los docentes como complemento a la hora de evaluar. Este juez online es DomJudge. DomJudge es un juez online desarrollado en la universidad de Utrecht con el fin de ser un juez virtual de concursos de programación. Su código es libre y se puede descargar y modificar, lo que lo hace ideal si se quiere adaptar su funcionamiento. Es bien sabido que generar casos de prueba de calidad es una tarea muy compleja. Existen diversas técnicas que ayudan a la generación automática de tests. Por ejemplo, la ejecución simbólica permite generar tests garantizando que todos los caminos de ejecución del programa son ejercitados hasta una cierta profundidad. El objetivo de este proyecto es hacer uso de estas técnicas de testing para generar casos de prueba de forma automática. Para que la autoevaluación realizada por estos jueces sea efectiva, los profesores deben proporcionar casos de prueba de calidad que son ejecutados automáticamente cuando los alumnos suben sus soluciones. Escribir estos casos de prueba resulta costoso y complejo, y es en este punto, donde el uso de jPET podría resultar muy útil. Los casos de prueba generados por jPET podrían servir como punto de partida a la hora de generar un conjunto de casos de prueba de calidad. Un aspecto muy interesante en este sentido, es que no es necesario que los programas de los alumnos uti licen el lenguaje Java. Lo único que sería necesario es que el profesor proporcione una solución escrita en Java. A partir de esta se podrían generar los casos de prueba iniciales. Si se diese el caso de que las soluciones de los alumnos viniesen escritas en Java, se podrían plantear enfoques más interesantes en los cuales los tests se forman a partir de ambas soluciones. La del alumno, para generarlos datos de entrada, y la del profesor, para chequear que las salidas para esas entradas son las correctas. Por eso hemos llevado a cabo no solo una traducción automática del xml generado por JPET en ficheros in y out. Sino una total integración con el sistema DomJudge para poder generar los casos de prueba sin intermediarios. Gracias a esta integración podemos facilitar el trabajo de los profesores a la hora de crear problemas en jueces online y conseguimos una generación automática de tests en DomJudge.

Integración y visualización de datos abiertos medioambientales

En la actualidad, muchos gobiernos están publicando (o tienen la intención de publicar en breve) miles de conjuntos de datos para que personas y organizaciones los puedan utilizar. Como consecuencia, la cantidad de aplicaciones basadas en Open Data está incrementándose. Sin embargo cada gobierno tiene sus propios procedimientos para publicar sus datos, y esto causa una variedad de formatos dado que no existe un estándar internacional para especificar los formatos de estos datos. El objetivo principal de este trabajo es un análisis comparativo de datos ambientales en bases de datos abiertas (Open Data) pertenecientes a distintos gobiernos. Debido a esta variedad de formatos, debemos construir un proceso de integración de datos que sea capaz de unir todos los tipos de formatos. El trabajo implica un pre-procesado, limpieza e integración de las diferentes fuentes de datos. Existen muchas aplicaciones desarrolladas para dar soporte en el proceso de integración por ejemplo Data Tamer, Data Wrangler como se explica en este documento. El problema con estas aplicaciones es que necesitan la interacción del usuario como parte fundamental del proceso de integración. En este trabajo tratamos de evitar la supervisión humana aprovechando las similitudes de los datasets procedentes de igual área que en nuestro caso se aplica al área de medioambiente. De esta forma los procesos pueden ser automatizados con una programación adecuada. Para conseguirlo, la idea principal de este trabajo es construir procesos ad hoc adaptados a las fuentes de cada gobierno para conseguir una integración automática. Concretamente este trabajo se enfoca en datos ambientales como lo son la temperatura, consumo de energía, calidad de aire, radiación solar, velocidad del viento, etc. Desde hace dos años el gobierno de Madrid está publicando sus datos relativos a indicadores ambientales en tiempo real. Del mismo modo, otros gobiernos han publicado conjuntos de datos Open Data relativos al medio ambiente (como Andalucía o Bilbao), pero todos estos datos tienen diferentes formatos. En este trabajo se presenta una solución capaz de integrar todas ellos que además permite al usuario visualizar y hacer análisis sobre los datos en tiempo real. Una vez que el proceso de integración está realizado, todos los datos de cada gobierno poseen el mismo formato y se pueden lanzar procesos de análisis de una manera más computacional. Este trabajo tiene tres partes fundamentales: 1. Estudio de los entornos Open Data y la literatura al respecto; 2. Desarrollo de un proceso de integración y 3. Desarrollo de una Interface Gráfica y Analítica. Aunque en una primera fase se implementaron los procesos de integración mediante Java y Oracle y la Interface Gráfica con Java (jsp), en una fase posterior se realizó toda la implementación con lenguaje R y la interface gráfica mediante sus librerías, principalmente con Shiny. El resultado es una aplicación que provee de un conjunto de Datos Ambientales Integrados en Tiempo Real respecto a dos gobiernos muy diferentes en España, disponible para cualquier desarrollador que desee construir sus propias aplicaciones.

Análisis de terminación para una plataforma de verificación de programas

De entre una serie de métodos estudiados acerca de la terminación de algoritmos, tales como Size-Change Termination o Isabelle, elegimos el método de RANK como instrumento para desarrollar nuestro propio programa de detección de terminación sobre el lenguaje de la IR. Esta decisión se basa en el coste polinómico de este método (frente a costes en PSPACE como el Size-Change Termination)y la posibilidad de obtener una herramienta asociada al mismo que además nos da la posibilidad de conocer un tiempo de ejecución aproximado. La herramienta asociada a RANK es compleja y va de la mano de una segunda herramienta (ASPIC). Hemos estudiado varios ejemplos, tales como el Mergesort o el Quicksort, para explicar la utilización de estas dos herramientas y a su vez ponernos en situación de los diferentes problemas que nos podemos encontrar a la hora de estudiar un programa. Partiendo del proceso que hemos usado para construir los automátas de los ejemplos anteriores, hemos diseñado e implementado en Java un algoritmo para transformar programas en el lenguaje de la IR al formato de entrada de RANK. Los resultados han sido satisfactorios, puesto que con los autómatas generados somos capaces de detectar de forma automatizada la terminación de, entre otros, los algoritmos recursivos antes mencionados.