Monitorización y verificación de un almacenamiento geológico de CO2. Aplicación de la monitorización superficial en la PDT de Hontomín (Burgos, España)

La necesidad de reducir las emisiones de gases de efecto invernadero ha contribuido al desarrollo de nuevas tecnologías de utilización sostenible de los combustibles fósiles. Destacan entre ellas la captura y almacenamiento de CO2 (CAC), aunque su aplicación industrial aún requiere avances tecnológicos. En este sentido, la Fundación Ciudad de la Energía (CIUDEN) desarrolla un proyecto integral de demostración de las técnicas CAC en el marco del proyecto Compostilla OXYCFB300 financiado por el programa europeo “European Energy Program for Recovery (EEPR)”

Diseño, implementación y verificación de una antena de microondas

A lo largo de este proyecto se han tratado las diferentes fases que tienen lugar durante el desarrollo del programa de Diseño y Verificación de una Bocina en Banda C destinada a un satélite comercial de comunicaciones. En un primer lugar, se introduce el proyecto en el mundo real realizando una pequeña aproximación a los satélites artificiales y su historia. Después, en una primera fase, se describen los diversos puntos de la etapa de diseño y los resultados de la simulación de nuestra Antena. Se estudian por separado los diferentes elementos que componen el equipo, y además, se realiza un análisis de los parámetros eléctricos que se deben tener en cuenta durante el diseño para adaptar el comportamiento de la Antena a los requisitos solicitados por el cliente. Antes de realizar la verificación de la Antena, se procede a la definición de los ensayos, que se debe realizar sobre el equipo con el fin de simular las condiciones a las que se verá sometido. Pruebas y medidas, niveles de test, etc. que nos ayudan a demostrar que nuestra Antena está preparada para realizar su misión en el espacio. Se hará una descripción sobre la forma de realizar de los ensayos y de las instalaciones donde se van a llevar a cabo, además del orden que llevaremos durante la campaña. Una vez determinados los test y con la Antena fabricada y lista, se procede a la Verificación de nuestro equipo mediante la Campaña de Ensayos con el objetivo de caracterizar por completo el funcionamiento de nuestra Antena en cualquier circunstancia. Se muestran los resultados obtenidos en los test siguiendo el orden establecido por el Test Plan. Medidas en Laboratorio y Radiación, los test de vibración y las pruebas ambientales en las Cámaras Térmicas de Vacío, y medidas eléctricas en condiciones extremas de temperatura y presión. Y una vez realizada la Campaña, se vuelve a medir la Antena para comprobar el funcionamiento tras soportar todos los ensayos. Se analizan los resultados obtenidos en cada una de las pruebas y se comparan con las simulaciones obtenidas durante la fase de diseño. Finalmente, se realiza un pequeño resumen de los valores más importantes obtenidos durante la Verificación y exponen las Conclusiones que se desprende de dicho proceso. Como último punto del proyecto, se estudian las correcciones y mejoras que se podrán llevar a cabo en futuros programas gracias a lo que hemos aprendido en este proyecto. Abstract This project presents a C Band Horn Antenna for a commercial communications satellite. All the different phases from Design to Verification are presented. First of all, an introduction to artificial satellites and their history is presented to put this project into perspective. Next, the electrical design of the Antenna is presented. Taking into account the theoretical fundamentals, each element that comprises this Antenna was designed. Their electrical performances, obtained from analysis using commercial software, are presented in the simulation results. In the design of each element of the antenna, some critical parameters are set and optimized in order to be compliant with the global requirements requested by the customer. After the design is completed, it is necessary to define the Test Campaign that has to be carried out in order to verify the validity of the designed and manufactured Antenna. Therefore, a Test Plan and the Electrical and Environmental Test Procedures are defined. This Test Campaign must be representative of the same conditions of the real space mission. Considering this, the following are defined: parameters for the network analyzer and radiation patterns measurements; test levels for the environmental test; definition of the RF measurements to be carried out and the temperatures to be applied in the thermal vacuum cycling. If the Antenna surpasses these tests, it will be ready to perform its mission in space over the entire satellite’s life cycle. The facilities where the tests are performed, as well as the sequence of the tests along the campaign are described too. After that, the Test Campaign is performed to fully characterize the Antenna in the space simulated conditions. Following the order established in the Test Plan, a radiation pattern and laboratory parameters are measured to correlate its electrical response with the simulations. Then, vibration and thermal vacuum tests are performed to verify its behavior in extreme environmental conditions. Last, if the final electrical results are the same as the initial ones, it can be stated that the antenna has successfully passed the Test Campaign. And finally, conclusions obtained from the data simulation design and Test Campaign results are presented. Status of Compliance with the specification is shown to demonstrate that the Antenna fulfills the requested requirements. Although the purpose of this project is to design and verify the response of C Band Horn Antenna, it is important to highlight improvements for future developments and the lessons learnt during this project.

Entorno de simulación para verificación y validación de equipamiento CBTC

Debido a sus características de seguridad, los sistemas de señalización ferroviarios requieren una gran cantidad de pruebas para su verificación y validación durante las diferentes etapas de su ciclo de vida, y en particular durante la instalación y puesta en marcha de una nueva línea o rehabilitación de una línea existente, siendo esta última aún más complicada debido a los cortos períodos de tiempo disponibles durante la noche para los trabajos. Este proyecto tiene como objetivo desarrollar una herramienta para reducir los esfuerzos antes mencionados mediante la simulación de los diferentes subsistemas de una línea equipada con sistema CBTC, el cumplimiento de las interfaces entre los subsistemas y el uso dentro de la simulación de equipos reales. Con estas premisas se desarrolló un entorno de pruebas para equipos y datos de señalización para líneas equipadas con el sistema CBTC. Los objetivos del proyecto que fueron establecidos en el inicio del desarrollo y han sido cumplidos con el desarrollo que se presenta en este artículo son los siguientes: • Poder realizar ensayos reales de equipos CBTC y su integración: equipos embarcados, equipos de control de área, etc. • Poder realizar ensayos reales con otros elementos de señalización y su integración: enclavamientos y ATS. • Poder realizar validación de datos vía CBTC. Para lograr estos objetivos se han desarrollado diversas aplicaciones de simulación, de las cuales, los más importantes son las siguientes: infraestructura, trenes automáticos, simulación de sistemas de tren, herramienta de gestión de los escenarios de simulación, etc Este sistema ha sido desarrollado y está añadiendo actualmente nuevos módulos y funcionalidades para las empresas del Grupo Invensys: Westinghouse Rail Systems en el Reino Unido y Dimetronic Signals en España, y está en uso en las nuevas líneas CBTC bajo su responsabilidad.

Modelización tridimensional de una figura por métodos fotogramétricos y escaneado de precisión. Verificación y comparación de resultados.

El objetivo principal de este proyecto es la obtención del modelo tridimensional de la escultura del patrón San Isidoro de la E.T.S.I. Topografía, Geodesia y Cartografía fabricada en yeso con unas dimensiones de 225 mm de largo, 182 mm de ancho y 318 mm de alto. Se realizará mediante dos métodos diferentes: por medios fotogramétricos utilizando correlación,y por métodos de topografía industrial. En la toma de imágenes para la restitución fotogramétrica se utilizó una cámara no métrica, cuya calibración tuvo que ser realizada comparando dos sistemas de coordenadas, el sistema imagen determinado por técnicas fotogramétricas, y el sistema objeto o terreno determinado por técnicas de topografía clásica. De esta forma se obtienen los datos internos de la cámara. La tolerancia establecida a priori para fotogrametría terrestre es de 1 mm, verificando y contrastando los resultados obtenidos con equipos de trazabilidad superior con los que se procede a la extracción del modelo digital por métodos de topografía industrial, mediante escaneado de precisión. El modelo tridimensional obtenido podría ser útil para múltiples tareas, como disponer de documentación geométrica digital de la figura, su estudio para una posible restauración,etc.

Propuesta, implementación y evaluación de la biometría de firma en el aire como sistema de verificación en teléfonos móviles

En esta tesis doctoral se propone una técnica biométrica de verificación en teléfonos móviles consistente en realizar una firma en el aire con la mano que sujeta el teléfono móvil. Los acelerómetros integrados en el dispositivo muestrean las aceleraciones del movimiento de la firma en el aire, generando tres señales temporales que pueden utilizarse para la verificación del usuario. Se proponen varios enfoques para la implementación del sistema de verificación, a partir de los enfoques más utilizados en biometría de firma manuscrita: correspondencia de patrones, con variantes de los algoritmos de Needleman-Wusch (NW) y Dynamic Time Warping (DTW), modelos ocultos de Markov (HMM) y clasificador estadístico basado en Máquinas de Vector Soporte (SVM). Al no existir bases de datos públicas de firmas en el aire y con el fin de evaluar los métodos propuestos en esta tesis doctoral, se han capturado dos con distintas características; una con falsificaciones reales a partir del estudio de las grabaciones de usuarios auténticos y otra con muestras de usuarios obtenidas en diferentes sesiones a lo largo del tiempo. Utilizando estas bases de datos se han evaluado una gran cantidad de algoritmos para implementar un sistema de verificación basado en firma en el aire. Esta evaluación se ha realizado de acuerdo con el estándar ISO/IEC 19795, añadiendo el caso de verificación en mundo abierto no incluido en la norma. Además, se han analizado las características que hacen que una firma sea suficientemente segura. Por otro lado, se ha estudiado la permanencia de las firmas en el aire a lo largo del tiempo, proponiendo distintos métodos de actualización, basados en una adaptación dinámica del patrón, para mejorar su rendimiento. Finalmente, se ha implementado un prototipo de la técnica de firma en el aire para teléfonos Android e iOS. Los resultados de esta tesis doctoral han tenido un gran impacto, generando varias publicaciones en revistas internacionales, congresos y libros. La firma en el aire ha sido nombrada también en varias revistas de divulgación, portales de noticias Web y televisión. Además, se han obtenido varios premios en competiciones de ideas innovadoras y se ha firmado un acuerdo de explotación de la tecnología con una empresa extranjera. ABSTRACT This thesis proposes a biometric verification technique on mobile phones consisting on making a signature in the air with the hand holding a mobile phone. The accelerometers integrated in the device capture the movement accelerations, generating three temporal signals that can be used for verification. This thesis suggests several approaches for implementing the verification system, based on the most widely used approaches in handwritten signature biometrics: template matching, with a lot of variations of the Needleman- Wusch (NW) and Dynamic Time Warping (DTW) algorithms, Hidden Markov Models (HMM) and Supported Vector Machines (SVM). As there are no public databases of in-air signatures and with the aim of assessing the proposed methods, there have been captured two databases; one. with real falsification attempts from the study of recordings captured when genuine users made their signatures in front of a camera, and other, with samples obtained in different sessions over a long period of time. These databases have been used to evaluate a lot of algorithms in order to implement a verification system based on in-air signatures. This evaluation has been conducted according to the standard ISO/IEC 19795, adding the open-set verification scenario not included in the norm. In addition, the characteristics of a secure signature are also investigated, as well as the permanence of in-air signatures over time, proposing several updating strategies to improve its performance. Finally, a prototype of in-air signature has been developed for iOS and Android phones. The results of this thesis have achieved a high impact, publishing several articles in SCI journals, conferences and books. The in-air signature deployed in this thesis has been also referred in numerous media. Additionally, this technique has won several awards in the entrepreneurship field and also an exploitation agreement has been signed with a foreign company.

Verificación experimental de las correlaciones de transferencia de calor por ebullición en película, en piscina, en torno a esferas

La ebullición en película es el mecanismo de transferencia de calor básico que acopla térmicamente un líquido y una superficie caliente cuando existe una gran diferencia de temperatura entre ambos. El conocimiento preciso del comportamiento de este mecanismo térmico en torno a esferas es necesario para el análisis de seguridad de escenarios industriales en los que exista contacto entre un líquido y un material fundido fragmentado, generalmente en piezas esferoidales, y resulta esencial para garantizar la seguridad de los reactores nucleares ante escenarios accidentales de muy baja probabilidad, pero de gran severidad, en los que se postule la rotura en guillotina del circuito de refrigeración del reactor simultánea al fallo total activo del sistema de refrigeración de emergencia del núcleo. En tal hipotético escenario, se produciría la fusión del combustible en el plazo de algunas horas, con dispersión y relocalización de fragmentos sólidos esferoidales a muy alta temperatura. Para hacer frente a este escenario se precisa desarrollar procedimientos automáticos y manuales de operación de emergencia, resultando imprescindible disponer de modelos térmicos confiables, con un calificado soporte experimental, que permitan analizar de forma realista la refrigeración por ebullición en película, en modo ebullición en piscina, de las geometrías esferoidales sólidas resultantes. En el presente trabajo UNET-UPM abordan la verificación de las correlaciones más conocidas para ebullición en película en piscina en torno a esferas, mediante la comparación de las mismas con los resultados experimentales obtenidos por Liu-Theofanous. Algunos de los aspectos resaltantes son la limitada aplicabilidad de la correlación empírica de Frederking-Clark, el buen ajuste que muestran las correlaciones de Tou- Tso y de Grigoriew frente a los datos experimentales usados, y las deficiencias que muestran las correlaciones que toman en cuenta el subenfriamiento del líquido, sobre todo a altos niveles de subenfriamiento. En una futura segunda fase de esta investigación, de tipo analítica-numérica-experimental, se abordará en el desarrollo de nuevas correlaciones semi-empíricas, de mejor ajuste, que permitan una mejor capacidad predictiva en los modelos.

Desarrollo de una herramienta de verificación para cálculos de difusión mediante COBAYA

El código COBAYA4 es un simulador de núcleo multi-escala que resuelve la ecuación de difusión 3D en multigrupos en geometría cartesiana y hexagonal[3]. Este código ha sido desarrollado en el Departamento de Ingeniería Nuclear desde los años 80[2] ampliando su alcance y funcionalidades de forma continua. Como parte de estos desarrollos es necesaria la verificación continua de que el código sigue teniendo al menos las mismas capacidades que tenía anteriormente. Además es necesario establecer casos de referencia que nos permitan confirmar que los resultados son comparables a los obtenidos con otros códigos con modelos de mayor precisión. El desarrollo de una herramienta informática que automatice la comparación de resultados con versiones anteriores del código y con resultados obtenidos mediante modelos de mayor precisión es crucial para implementar en el código nuevas funcionalidades. El trabajo aquí presentado ha consistido en la generación de la mencionada herramienta y del conjunto de casos de referencia que han constituido la matriz mencionada.

Estudio de verificación biométrica de voz

En este proyecto estudia la posibilidad de realizar una verificación de locutor por medio de la biometría de voz. En primer lugar se obtendrán las características principales de la voz, que serían los coeficientes MFCC, partiendo de una base de datos de diferentes locutores con 10 muestras por cada locutor. Con estos resultados se procederá a la creación de los clasificadores con los que luego testearemos y haremos la verificación. Como resultado final obtendremos un sistema capaz de identificar si el locutor es el que buscamos o no. Para la verificación se utilizan clasificadores Support Vector Machine (SVM), especializado en resolver problemas biclase. Los resultados demuestran que el sistema es capaz de verificar que un locutor es quien dice ser comparándolo con el resto de locutores disponibles en la base de datos. ABSTRACT. Verification based on voice features is an important task for a wide variety of applications concerning biometric verification systems. In this work, we propose a human verification though the use of their voice features focused on supervised training classification algorithms. To this aim we have developed a voice feature extraction system based on MFCC features. For classification purposed we have focused our work in using a Support Vector Machine classificator due to it’s optimization for biclass problems. We test our system in a dataset composed of various individuals of di↵erent gender to evaluate our system’s performance. Experimental results reveal that the proposed system is capable of verificating one individual against the rest of the dataset.

La verificación de las fuentes sonoras en la acreditación de laboratorios de ensayos acústicos

La norma UNE-EN ISO/IEC 17025 establece los requisitos generales para la competencia en la realización de ensayos y sirve de referencia para la acreditación de los laboratorios. Entre los requisitos que establece está el de asegurar que los equipos utilizados en las mediciones cumplen con las especificaciones que determinan las normas de ensayo correspondientes. En este trabajo se analizan los requisitos que se imponen a las fuentes sonoras en los ensayos acústicos más usuales. Se describen las técnicas de verificación habitualmente utilizadas y se discuten los errores más comunes en las verificaciones y en la evaluación de los resultados.

Propuesta de Mecanismos de Verificación de Integridad de Plataformas Móviles de Computación basados en Entornos Seguros de Ejecución

Las prestaciones y características de los dispositivos móviles actuales los sitúa a un nivel similar a los ordenadores de escritorio tradicionales en cuanto a funcionalidad y posibilidades de uso, añadiendo además la movilidad y la sensación de pertenencia al usuario que se deriva de ésta. Estas cualidades convierten a las plataformas móviles de computación en verdaderos ordenadores personales, y cada día es más popular su utilización en ámbitos distintos del ocio y las comunicaciones propiamente dichas, pasando a convertirse en herramientas de apoyo a la productividad también en el entorno profesional y corporativo. La utilización del dispositivo móvil como parte de una infraestructura de telecomunicaciones da lugar a nuevas expresiones de problemas clásicos de gestión y seguridad. Para tratar de abordarlos con la flexibilidad y la escalabilidad necesarias se plantean alternativas novedosas que parten de enfoques originales a estos problemas, como las ideas y conceptos que se engloban en la filosofía del Control de Acceso a la Red (Network Access Control, o NAC). La mayoría de los planteamientos de NAC se basan, en el ámbito de la seguridad, en comprobar ciertas características del dispositivo móvil para tratar de determinar hasta qué punto puede éste suponer una amenaza para los recursos de la red u otros usuarios de la misma. Obtener esta información de forma fiable resulta extremadamente difícil si se caracteriza el dispositivo mediante un modelo de caja blanca, muy adecuado dada la apertura propia de los sistemas operativos móviles actuales, muy diferentes de los de antaño, y la ausencia de un marco de seguridad efectivo en ellos. Este trabajo explora el Estado de la Técnica en este ámbito de investigación y plantea diferentes propuestas orientadas a cubrir las deficiencias de las soluciones propuestas hasta el momento y a satisfacer los estrictos requisitos de seguridad que se derivan de la aplicación del modelo de caja blanca, materializándose en última instancia en la definición de un mecanismo de evaluación de características arbitrarias de un cierto dispositivo móvil basado en Entornos Seguros de Ejecución (Trusted Execution Environments, o TEEs) con elevadas garantías de seguridad compatible con los planteamientos actuales de NAC. ABSTRACT The performance and features of today’s mobile devices make them able to compete with traditional desktop computers in terms of functionality and possible usages. In addition to this, they sport mobility and the stronger sense of ownership that derives from it. These attributes change mobile computation platforms into truly personal computers, allowing them to be used not only for leisure or as mere communications devices, but also as supports of productivity in professional and corporative environments. The utilization of mobile devices as part of a telecommunications infrastructure brings new expressions of classic management and security problems with it. In order to tackle them with appropriate flexibility and scalability, new alternatives are proposed based on original approaches to these problems, such as the concepts and ideas behind the philosophy of Network Access Control (NAC). The vast majority of NAC proposals are based, security-wise, on checking certain mobile device’s properties in order to evaluate how probable it is for it to become a threat for network resources or even other users of the infrastructure. Obtaining this information in a reliable and trustworthy way is extremely difficult if the device is characterized using a white-box model, which is the most appropriate if the openness of today’s mobile operating systems, very different from former ones, and the absence of an effective security framework are taken into account. This work explores the State of the Art related with the aforementioned field of research and presents different proposals targeted to overcome the deficiencies of current solutions and satisfy the strict security requirements derived from the application of the white box model. These proposals are ultimately materialized in the definition of a high-security evaluation procedure of arbitrary properties of a given mobile device based on Trusted Execution Environments (TEEs) which is compatible with modern NAC approaches.

Urbanismo y seguridad: Verificación del método CPTED en un barrio de Madrid

El presente trabajo está motivado por la verificación de cómo influye el urbanismo en los delitos e infracciones que se producen en las ciudades. Para realizar este estudio se ha empleado el método CPTED (Crime Prevention Through Enviromental Design). Este método, desarrollado en otros países como Holanda, Reino Unido, Australia o Estados Unidos, no es tan conocido en España. Ha sido tratado sin embardo en la Tesis Doctoral “SEGURIDAD Y DISEÑO URBANO EN LOS NUEVOS CRECIMIENTOS DE MADRID” realizada por Elena Escudero, tomada como base para la investigación. El ámbito de estudio seleccionado es a la escala de barrio, para llegar a unas conclusiones lo más ajustadas a la realidad posibles en el tiempo designado para la realización del trabajo. El barrio estudiado es Gaztambide, perteneciente al distrito de Chamberí. Se ha elegido éste en particular y no otro, dado que inicialmente se pensó que podría tener más deficiencias en el ámbito de la seguridad. Lo que infundió esas conclusiones iniciales fueron los locales y sitios de ocio nocturno concentrados en el mismo. Tras aplicar el método CPTED de forma cuantitativa (tal y como propone Elena en su tesis), se comparan los resultados obtenidos con datos policiales y encuestas de seguridad subjetiva, gracias al Atlas de Seguridad. Finalizado el análisis y la recopilación de información, se espera verificar el funcionamiento de la herramienta CPTED y su correspondencia con los datos objetivos y subjetivos obtenidos por los medios mencionados con anterioridad. Una vez obtenidos estos resultados, se compararán los niveles de Seguridad con los que aparecen en la Tesis de Elena Escudero en los nuevos crecimientos de Madrid.

Verificación de extensiones de Redes de Petri con precios, tiempo y múltiples instancias

Las redes de Petri son un lenguaje formal muy adecuado para la modelizacíon, ańalisis y verificacíon de sistemas concurrentes con infinitos estados. En particular, son muy apropiadas para estudiar las propiedades de seguridad de dichos sistemas, dadas sus buenas propiedades de decidibilidad. Sin embargo, en muchas ocasiones las redes de Petri carecen de la expresividad necesaria para representar algunas caracteŕısticas fundamentales de los sistemas que se manejan hoy en d́ıa, como el manejo de tiempo real, costes reales, o la presencia de varios procesos con un ńumero no acotado de estados ejecut́andose en paralelo. En la literatura se han definido y estudiado algunas extensiones de las redes de Petri para la representaci ́on de las caracteŕısticas anteriores. Por ejemplo, las “Redes de Petri Temporizadas” [83, 10](TPN) incluyen el manejo de tiempo real y las ν-redes de Petri [78](ν-PN) son capaces de representar un ńumero no acotado de procesos con infinitos estados ejecut́andose concurrentemente. En esta tesis definimos varias extensiones que réunen estas dos caracteŕısticas y estudiamos sus propiedades de decidibilidad. En primer lugar definimos las “ν-Redes de Petri Temporizadas”, que réunen las caracteŕısticas expresivas de las TPN y las ν-PN. Este nuevo modelo es capaz de representar sistemas con un ńumero no acotado de procesos o instancias, donde cada proceso es representado por un nombre diferente, y tiene un ńumero no acotado de relojes reales. En este modelo un reloj de una instancia debe satisfacer ciertas condiciones (pertenecer a un intervalo dado) para formar parte en el disparo de una transicíon. Desafortunadamente, demostramos que la verificacíon de propiedades de seguridad es indecidible para este modelo...

Verificación de Sistemas Basada en Teoría de Tipos

Este proyecto se enmarca en la utlización de métodos formales (más precisamente, en la utilización de teoría de tipos) para garantizar la ausencia de errores en programas. Por un lado se plantea el diseño de nuevos algoritmos de chequeo de tipos. Para ello, se proponen nuevos algoritmos basados en la idea de normalización por evaluación que sean extensibles a otros sistemas de tipos. En el futuro próximo extenderemos resultados que hemos conseguido recientemente [16,17] para obtener: una simplificación de los trabajos realizados para sistemas sin regla eta (acá se estudiarán dos sistemas: a la Martin Löf y a la PTS), la formulación de estos chequeadores para sistemas con variables, generalizar la noción de categoría con familia utilizada para dar semántica a teoría de tipos, obtener una formulación categórica de la noción de normalización por evaluación y finalmente, aplicar estos algoritmos a sistemas con reescrituras. Para los primeros resultados esperados mencionados, nos proponemos como método adaptar las pruebas de [16,17] a los nuevos sistemas. La importancia radica en que permitirán tornar más automatizables (y por ello, más fácilmente utilizables) los asistentes de demostración basados en teoría de tipos. Por otro lado, se utilizará la teoría de tipos para certificar compiladores, intentando llevar adelante la propuesta nunca explorada de [22] de utilizar un enfoque abstracto basado en categorías funtoriales. El método consistirá en certificar el lenguaje "Peal" [29] y luego agregar sucesivamente funcionalidad hasta obtener Forsythe [23]. En este período esperamos poder agregar varias extensiones. La importancia de este proyecto radica en que sólo un compilador certificado garantiza que un programa fuente correcto se compile a un programa objeto correcto. Es por ello, crucial para todo proceso de verificación que se base en verificar código fuente. Finalmente, se abordará la formalización de sistemas con session types. Los mismos han demostrado tener fallas en sus formulaciones [30], por lo que parece conveniente su formalización. Durante la marcha de este proyecto, esperamos tener alguna formalización que dé lugar a un algoritmo de chequeo de tipos y a demostrar las propiedades usuales de los sistemas. La contribución es arrojar un poco de luz sobre estas formulaciones cuyos errores revelan que el tema no ha adquirido aún suficiente madurez o comprensión por parte de la comunidad.

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.

Utilización del modelo HEC-HMS en sistemas de pronósticos hidrológicos y verificación de los datos obtenidos por el modelo CMPORH, en la cuenca del Río Sucio

La presente investigación, consistió en verificar los datos obtenidos del modelo de precipitación satelital CMORPH, habiendo seleccionado como fuente de estudio la cuenca del Río Sucio, con la información obtenida de pluviométros ubicados dentro y en las cercanías de dicha cuenca, se realizaron hietogramas, mapas de distribución de lluvia y cálculo de caudales máximos, para poder determinar si los datos del modelo de precipitación satelital CMORPH, son aplicables a nuestro país