Desarrollo Riguroso de Sistemas Tolerantes a Fallas

Los sistemas críticos son aquellos utilizados en áreas en las cuales las fallas, o los eventos inesperados, pueden ocasionar grandes perdidas de dinero; o quizás peor aún, daños a vidas humanas. Esta clase de sistemas juegan un rol importante en actividades esenciales de la sociedad tales como la medicina y las comunicaciones. Los sistemas críticos, cada vez son más usuales en la vida real, algunos ejemplos de estos son los sistemas de aviones, sistemas para automóviles y sistemas utilizados en telefonia móvil. Para minimizar las fallas, y las perdidas materiales o humanas ocasionadas por el funcionamiento incorrecto de dichos sistemas, se utilizan técnicas de tolerancia a fallas. Estas técnicas permiten que los sistemas continúen funcionando aún bajo la ocurrencia de fallas, o eventos inesperados. Existen diversas técnicas para lograr tolerancia a fallas utilizando, por ejemplo, redundancia a diferentes niveles de abstracción, como, por ejemplo, al nivel de hardware. Sin embargo, estas técnicas dependen fuertemente del sistema, y del contexto en las que se utilizan. Más aún, la mayoría de la técnicas de tolerancia a fallas son usadas a bajo nivel (código fuente o hardware), estimamos que el uso de formalismos rigurosos (con fundamentos matemáticos) pueden llevar al diseño de sistemas tolerantes a fallas y robustos a un nivel de abstracción más alto, a la vez que la utilización de técnicas de verificación que han sido exitosas en la práctica tales como model checking, o la síntesis de controladores, pueden llevar a una verificación y producción automática de sistemas robustos. El objetivo del presente proyecto es estudiar tanto marcos teóricos, que permitan la construcción de sistemas más robustos, como también herramientas automáticas que hagan posible la utilización de estos formalismos en escenarios complejos. Para lograr estos objetivos, será necesario considerar casos de estudios de diferente complejidad, y además que sean relevantes en la práctica. Por ejemplo: bombas de insulina, protocolos de comunicación, sistemas de vuelo y sistemas utilizados con fines médicos. Planeamos obtener prototipos de algunos de estos casos de estudio para evaluar los marcos teóricos propuestos. En los últimos años diferentes formalismos han sido utilizados para razonar sobre sistemas tolerantes a fallas de una forma rigurosa, sin embargo, la mayoría de estos son ad hoc, por lo cual sólo son aplicables a contextos específicos. Planeamos utilizar ciertas lógicas modales, en conjunto con nociones probabilísticas, para obtener un conjunto de herramientas suficientemente generales para que puedan ser utilizadas en diferentes contextos y aplicaciones. Los materiales a utilizar son equipos informáticos, en particular computadoras portátiles para el equipo de trabajo y computadoras más potentes para el testeo y desarrollo del software necesario para lograr los objetivos del proyecto. Para construir los prototipos mencionados se utilizarán equipos de computación estándar (el equipo investigación cuenta con computadoras intel y mac) en conjunto con lenguajes de programación modernos como JAVA o C#. En el caso de que los sistemas de software sean sistemas embebidos; se piensa desarrollar un motor de simulación que permita evaluar el desempeño del software cuando es ejecutado en el dispositivo mencionado. Se espera desarrollar, e investigar, las propiedades de formalismos matemáticos que permitan el desarrollo de sistemas tolerantes a fallas. Además, se desarrollarán herramientas de software para que estos sistemas tolerantes a fallas puedan verificarse, o obtenerse automáticamente. Los resultados obtenidos serán difundidos por medio de publicaciones en revistas del área. El desarrollo de sistemas tolerantes a fallas por medio de técnicas rigurosas, a diferentes niveles de abstracción (captura de requisitos, diseño, implementación y validación), permitirá minimizar los riesgos inherentes en actividades críticas.

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.

Analizar y comparar el lenguaje de alto nivel SystemC frente a los de HDL. aplicación al diseño de sistemas de computo

La complejidad de los sistemas actuales de computación ha obligado a los diseñadores de herramientas CAD/CAE a acondicionar lenguajes de alto nivel, tipo C++, para la descripción y automatización de estructuras algorítmicas a sus correspondientes diseños a nivel físico. Los proyectos a realizar se encuadran dentro de una línea de trabajo consistente en estudiar la programación, funcionamiento de los lenguajes SystemC y SystemVerilog, sus herramientas asociadas y analizar cómo se adecuan a las restricciones temporales y físicas de los componentes (librerías, IP's, macro-celdas, etc) para su directa implementación. En una primera fase, y para este TFG, se estudiarán los componentes que conforman el framework elegido que es SystemC y su inclusión en herramientas de diseño arquitectural. Este conocimiento nos ayudará a entender el funcionamiento y capacidad de dicha herramienta y proceder a su correcto manejo. Analizaremos y estudiaremos unos de los lenguajes de alto nivel de los que hace uso dicha herramienta. Una vez entendido el contexto de aplicación, sus restricciones y sus elementos, diseñaremos una estructura hardware. Una vez que se tenga el diseño, se procederá a su implementación haciendo uso, si es necesario, de simuladores. El proyecto finalizará con una definición de un conjunto de pruebas con el fin de verificar y validar la usabilidad y viabilidad de nuestra estructura hardware propuesta.

Integración de datos y análisis predictivo en tratamiento de drogodependencia

El análisis de datos actual se enfrenta a problemas derivados de la combinación de datos procedentes de diversas fuentes de información. El valor de la información puede enriquecerse enormemente facilitando la integración de nuevas fuentes de datos y la industria es muy consciente de ello en la actualidad. Sin embargo, no solo el volumen sino también la gran diversidad de los datos constituye un problema previo al análisis. Una buena integración de los datos garantiza unos resultados fiables y por ello merece la pena detenerse en la mejora de procesos de especificación, recolección, limpieza e integración de los datos. Este trabajo está dedicado a la fase de limpieza e integración de datos analizando los procedimientos existentes y proponiendo una solución que se aplica a datos médicos, centrándose así en los proyectos de predicción (con finalidad de prevención) en ciencias de la salud. Además de la implementación de los procesos de limpieza, se desarrollan algoritmos de detección de outliers que permiten mejorar la calidad del conjunto de datos tras su eliminación. El trabajo también incluye la implementación de un proceso de predicción que sirva de ayuda a la toma de decisiones. Concretamente este trabajo realiza un análisis predictivo de los datos de pacientes drogodependientes de la Clínica Nuestra Señora de la Paz, con la finalidad de poder brindar un apoyo en la toma de decisiones del médico a cargo de admitir el internamiento de pacientes en dicha clínica. En la mayoría de los casos el estudio de los datos facilitados requiere un pre-procesado adecuado para que los resultados de los análisis estadísticos tradicionales sean fiables. En tal sentido en este trabajo se implementan varias formas de detectar los outliers: un algoritmo propio (Detección de Outliers con Cadenas No Monótonas), que utiliza las ventajas del algoritmo Knuth-Morris-Pratt para reconocimiento de patrones, y las librerías outliers y Rcmdr de R. La aplicación de procedimientos de cleaning e integración de datos, así como de eliminación de datos atípicos proporciona una base de datos limpia y fiable sobre la que se implementarán procedimientos de predicción de los datos con el algoritmo de clasificación Naive Bayes en R.

Optimización de la ejecución de flujos de trabajos empresariales en infraestructuras cloud

En la actualidad, el uso del Cloud Computing se está incrementando y existen muchos proveedores que ofrecen servicios que hacen uso de esta tecnología. Uno de ellos es Amazon Web Services, que a través de su servicio Amazon EC2, nos ofrece diferentes tipos de instancias que podemos utilizar según nuestras necesidades. El modelo de negocio de AWS se basa en el pago por uso, es decir, solo realizamos el pago por el tiempo que se utilicen las instancias. En este trabajo se implementa en Amazon EC2, una aplicación cuyo objetivo es extraer de diferentes fuentes de información, los datos de las ventas realizadas por las editoriales y librerías de España. Estos datos son procesados, cargados en una base de datos y con ellos se generan reportes estadísticos, que ayudarán a los clientes a tomar mejores decisiones. Debido a que la aplicación procesa una gran cantidad de datos, se propone el desarrollo y validación de un modelo, que nos permita obtener una ejecución óptima en Amazon EC2. En este modelo se tienen en cuenta el tiempo de ejecución, el coste por uso y una métrica de coste/rendimiento. Adicionalmente, se utilizará la tecnología de contenedores Docker para llevar a cabo un caso específico del despliegue de la aplicación.

Diseño e implementación del kernel de xDEVS, versión distribuida

Para entender nuestro proyecto, debemos comprender DEVS. Dentro de los formalismos más populares de representación de sistemas de eventos discretos se encuentra DES. En la década de los 70, el matemático Bernard Zeigler propuso un formalismo general para la representación de dichos sistemas. Este formalismo denominado DEVS (Discrete EVent System Specification) es el formalismo más general para el tratamiento de DES. DEVS permite representar todos aquellos sistemas cuyo comportamiento pueda describirse mediante una secuencia de eventos discretos. Estos eventos se caracterizan por un tiempo base en el que solo un número de eventos finitos puede ocurrir. DEVS Modelado y Simulación tiene múltiples implementaciones en varios lenguajes de programación como por ejemplo en Java, C# o C++. Pero surge la necesidad de implementar una plataforma distribuida estable para proporcionar la mecánica de interoperabilidad e integrar modelos DEVS diversificados. En este proyecto, se nos dará como código base el core de xDEVS en java, aplicado de forma secuencial y paralelizada. Nuestro trabajo será implementar el core de manera distribuida de tal forma que se pueda dividir un sistema DEVS en diversas máquinas. Para esto hemos utilizado sockets de java para hacer la transmisión de datos lo más eficiente posible. En un principio deberemos especificar el número de máquinas que se conectarán al servidor. Una vez estas se hayan conectado se les enviará el trabajo específico que deberán simular. Cabe destacar que hay dos formas de dividir un sistema DEVS las cuales están implementadas en nuestro proyecto. La primera es dividirlo en módulos atómicos los cuales son subsistemas indivisibles en un sistema DEVS. Y la segunda es dividir las funciones de todos los subsistemas en grupos y repartirlos entre las máquinas. En resumen el funcionamiento de nuestro sistema distribuido será comenzar ejecutando el trabajo asignado al primer cliente, una vez finalizado actualizará la información del servidor y este mandara la orden al siguiente y así sucesivamente.

Simulando con OMNET: selección de la herramienta y su utilización

Incluye referencias bibliográficas e índice. CONTENIDO: Introducción -- Elección de una herramienta de simulación -- Instalación de OMNET -- Lenguajes de OMNET++ -- Ejemplo Tic-Toc -- Simulación de esquemas de encolamiento.

Introduccion - Simulando con OMNET: selección de la herramienta y su utilización

La diferenciación y el soporte en calidad de servicio es utilizada en muchas arquitecturas de red, técnicas y frameworks, tales como IP, con los esquemas de DiffServ e IntServ, redes NGN, GMPLS (Generalized Multiprotocol Label Switching) y redes ópticas, entre otras. Actualmente, la calidad de servicio no es solo una cuestión técnica, sino que se ha convertido en un producto que puede ser visto desde numerosas perspectivas, en las que los clientes, cada día, demandan más servicios, de mayor calidad. Por lo tanto, los proveedores deben mejorar sus implementaciones para permanecer en este reñido mercado (Piotr, Stankiewicz, Cholda, & Jajszczyk, 2011). En este contexto, las redes actuales deben garantizar la calidad en los servicios sin importar el incremento paulatino de usuarios y dispositivos de interconectividad. La mejor manera de hacerlo no es necesariamente invirtiendo en la infraestructura más moderna que soporte técnicas para este fin. Existen mecanismos que se pueden aplicar sobre infraestructuras de red actuales, las cuales ayudan a manejar el tráfico de manera adecuada, de tal manera que los parámetros de calidad de servicio se mantengan dentro de los límites permisibles establecidos por la Recomendación Y.1541 (UIT, 2011a).

Elección de una herramienta de simulación

Hoy en día, las herramientas de simulación son un componente fundamental para el diseño, la implementación y el monitoreo de redes de comunicación, porque permiten predecir el comportamiento de diferentes eventos que pueden afectar el desempeño de la red y degradar la calidad de las aplicaciones y los servicios. Como presenta Cuéllar (2011) las herramientas de simulación juegan un papel importante para evaluar el comportamiento de parámetros como el retardo y el jitter en una red, porque permiten la recreación de escenarios reales con el fin de analizar su desempeño, sin tener que implementar infraestructura física. Además, las simulaciones permiten tener en cuenta numerosas variables y son un método eficaz para la enseñanza y la investigación. La simulación no es un concepto nuevo; siempre se ha buscado la manera de evaluar sistemas complejos y tal como define Phillips (2007), la simulación es la ejecución de un modelo representado por un programa de computadora que permite recrear entornos de red, ahorrando tiempo y dinero. Comercialmente existen simuladores de tiempo continuo y tiempo discreto; la simulación en tiempo discreto modela sistemas que cambian en el tiempo de acuerdo con los diferentes estados que una variable puede tener, algo muy útil para sistemas de comunicación. Los simuladores de tiempo continuo, por su parte, avanzan en el tiempo y constantemente revisan si ha ocurrido algún evento, con el fin de actualizar las variables correspondientes, para, solo en ese caso, realizar la modificación de valores.

Instalación de OMNET

En este capítulo se explica la instalación de OMNET y del INET Framework en ambiente Windows 7, para un sistema operativo de 64 bits. Para un ambiente diferente –o para mayor información– se recomienda consultar el manual de instalación de OMNeT ++ (Varga, 2011), publicado en http://omnetpp.org/doc/ omnetpp/InstallGuide.pdf (actualmente la versión disponible es la 4.2.2).

Ejemplo Tic-Toc

Cali de Lat: 03 24 00 N degrees minutes Lat: 3.4000 decimal degrees Long: 076 30 00 W degrees minutes Long: -76.5000 decimal degrees.

Simulación de esquemas de encolamiento

En este capítulo se presenta el proceso realizado para simular diferentes esquemas de encolamiento (FIFO, PQ y LLQ) de manera básica con el fin de ofrecer QoS en una red. También se presentan gráficas que permiten realizar el análisis posterior de los datos obtenidos en la simulación.

Desarrollo de material educativo reutilizable para el portal educativo de la UCM "Acepta el reto"

El juez en línea https://www.aceptaelreto.com desarrollado por profesores de la UCM basa su éxito no solamente en la funcionalidad como juez, sino en la batería de problemas de programación que aloja y que presentan retos lo suficientemente variados como para satisfacer a un amplio rango de usuarios. El documento es la memoria final de un Proyecto de Innovación y Mejora de la Calidad Docente (PIMCD) de 2015 en el que se crearon más de 60 problemas para este juez.

Complemento práctico en la enseñanza de lenguajes formales usando las expresiones regulares en el contexto de aplicaciones web

Tradicionalmente la enseñanza de los autómatas y lenguajes formales basa su principal aplicación práctica en la construcción de compiladores. Sin embargo, las tareas de diseño y programación necesarias son excesivamente complejas como para que los estudiantes, que están cursando el tercer cuatrimestre de la Ingeniería, puedan abordarlas con el rigor necesario. Es posible incorporar otro enfoque práctico, real y más actual de las expresiones regulares en estas asignaturas, aprovechando su frecuente uso como herramienta de especificación de patrones a la hora de diseñar formularios de entrada de datos en diferentes contextos y, particularmente, en aplicaciones web de tres capas. El hecho de trabajar esta competencia junto con el desarrollo teórico de las expresiones regulares permite a los estudiantes ser conscientes de la importante utilidad práctica de este concepto, sin restringirlo a otros usos más clásicos relacionados con el diseño de procesadores de textos o analizadores léxicos. Durante el curso 2006-07 se ha propuesto a los estudiantes de Ingeniería Técnica en Informática de Sistemas de la Universidad del País Vasco desarrollar fragmentos de código basados en una notación formal para resolver problemas de reconocimiento de patrones. La experiencia se ha llevado a cabo utilizando concretamente la notación, inspirada en las expresiones regulares, de JavaScript, resultando viable, efectiva y bien valorada por parte de los estudiantes.