SITIO DE TEST - SITIO DE TEST - SITIO DE TEST - SITIO DE TEST - SITIO DE TEST - SITIO DE TEST - SITIO DE TEST - SITIO DE TEST - SITIO DE TEST
 

FCEIA-ECEN-DCC- Trabajos Finales de Grado (trabajos finales, proyectos y tesinas)

URI permanente para esta colección

Examinar

Envíos recientes

Mostrando 1 - 20 de 82
  • ÍtemAcceso Abierto
    Mapeo denso en tiempo real sobre sistemas SLAM basados en visión estéreo
    (2017-12) D'Alessandro, Ariel; Pire, Taihú; Baravalle, Rodrigo
    Para poder navegar de manera segura en un entorno desconocido, un robot autónomo móvil debe poder construir una representación del ambiente (mapeo) en el cual se mueve, al mismo tiempo que estima su posición (localización). Este problema es conocido en la robótica móvil como SLAM por el acrónimo en inglés de Simultaneous Localization and Mapping. Un mayor nivel de detalle del entorno (mapa) resultará en una posible mejora en los algoritmos de navegación del robot, permitiéndole esquivar obstáculos con una precisión mayor, obteniendo trayectorias más seguras y óptimas. En este trabajo se propone un sistema de SLAM denso basado en visión estéreo que resulta de la inclusión de un módulo de densificación al sistema de SLAM S-PTAM (Stereo Parallel Tracking and Mapping) del estado del arte. El sistema de SLAM resultante es capaz de generar un mapa denso del entorno al mismo tiempo que estima la localización de la cámara. Los experimentos muestran que el método realiza una densificación local precisa del mapa en tiempo real. El sistema se implementó utilizando el framework ROS (Robot Operating System). El código ha sido liberado bajo licencia GPLv3, con el objetivo de facilitar el uso y modificación del sistema por parte de la comunidad robótica.
  • ÍtemAcceso Abierto
    Formalización de mónadas concurrentes en Agda: un análisis del caso de la mónada Delay
    (2023-12) Bini, Valentina María; Rivas, Exequiel
    En los últimos años, la concurrencia ha cobrado mucha importancia en el mundo de la programación, sobre todo debido a la masificación de los procesadores con múltiples núcleos. Los lenguajes de programación funcional, en general, proveen la capacidad de concurrencia mediante funciones ad-hoc, y no mediante primitivas bien fundadas del lenguaje. En este trabajo se presenta una formalización del concepto de mónada concurrente en el lenguaje y asistente de pruebas Agda, así como también otras formalizaciones de conceptos previos como las mónadas, los funtores monoidales y los monoides concurrentes. Luego se analiza el caso particular de la mónada delay, con el objetivo de probar o refutar que esta puede dotarse de una estructura de mónada concurrente. La principal dificultad que se encontró a la hora de realizar esta prueba es la demostración de la ley de intercambio. Se buscó entonces una simplificación del problema y se demostró que los números conaturales forman un monoide concurrente, obteniendo luego una mónada concurrente alternativa a delay: la mónada writer con los conaturales como monoide.
  • ÍtemAcceso Abierto
    Compilación del lambda cálculo con matrices densidad en la máquina cuántica IBM-Q
    (2023-12) Villagra, Martín; Díaz-Caro, Alejandro; Martínez López , Pablo E.
    El cálculo λρ introducido por Díaz-Caro en 2017 es un lenguaje basado en el lambda cálculo con extensiones para la computación cuántica donde se utiliza un modelo de control clásico y datos cuánticos. Los estados cuánticos se describen mediante matrices de densidad, que permite operar con estados cuánticos mixtos. En esta tesina se provee un algoritmo para tipar λρ. Utilizando este algoritmo probamos que el tipado es NP-completo bajo condiciones de minimización de los tipos. Seguidamente analizamos la relación entre λρ y las aplicaciones actuales de la computación cuántica al definir una traducción de una versión modificada de λρ a Python y haciendo uso de la biblioteca de Qiskit. Además de probar su correctitud, implementamos estos algoritmos en el lenguaje funcional Haskell.
  • ÍtemAcceso Abierto
    Formalización de Sistema I con tipo Top
    (2023-11) Settimo, Agustín Francisco; Manzino, Cecilia; Sottile, Cristian
    Los sistemas de tipos desempeñan un papel esencial en la garantía del comportamiento adecuado de los programas. Sin embargo, estos imponen cierta rigidez a la hora de escribir dichos programas, ya que se deben adherir estrictamente a las reglas de tipado establecidas. Existen una serie de “sistemas módulo isomorfismos” [DD19; DD23; AD20; DM15; Sot20; SDM20] que proponen flexibilizar esta restricción considerando aquellos tipos que sean isomorfos como idénticos. En simples palabras, dos tipos se consideran isomorfos cuando es posible convertir uno en el otro, y viceversa, sin perder información en el proceso. Es decir, si dos tipos A y B son isomorfos, es posible usar un término de tipo A en cualquier lugar que se espere un término de tipo B aplicando la conversión correspondiente. Trabajar con tipos isomorfos provee mayor flexibilidad en la construcción de programas y permite combinarlos de formas que normalmente no serían posibles. Este trabajo se centra principalmente en el primero de estos sistemas, llamado Sistema I. Aquí, se presenta una formalización de una adaptación de dicho sistema en el lenguaje Agda, además, se añade el tipo Top y los isomorfismos correspondientes para ampliar aún más la flexibilidad del sistema. Esta formalización va acompañada de pruebas formales que demuestran el cumplimiento de diversas propiedades, siendo la normalización fuerte una de las más cruciales. Es importante destacar que la prueba de normalización fuerte utiliza la técnica de logical relations pero con predicados distintos a los presentados en la prueba de candidatos de reducibilidad de Girard.
  • ÍtemAcceso Abierto
    Control de trayectoria tolerante a fallas para sistemas discretos con aplicación a un robot agrícola
    (2021-05-14) Soncini, Nicolás; Kofman, Ernesto
    En esta tesis se desarrolla una nueva técnica de técnica de control tolerante a fallas para sistemas de tiempo discreto. Se demuestran sus principales propiedades teóricas y se aplica sobre un sistema complejo consistente en el modelo de un robot agrícola. La técnica de control desarrollada, basada en una técnica existente para sistemas de tiempo continuo, utiliza el concepto novedoso de conjuntos invariantes probabilísticos. Los mismos se utilizan para detectar la presencia de diversas fallas en el sistema, en función de la pertenencia de ciertas variables a dichos conjuntos. La aplicación de esta técnica a un caso realista, en tanto, se realizó en el control de trayectorias de un modelo de robot agrícola. Si bien no se probó el sistema sobre el robot real, sí se lo hizo sobre simulaciones en tiempo real del mismo, incluyendo variaciones de parámetros y retardos que demuestran la robustez del esquema propuesto.
  • ÍtemAcceso Abierto
    Simulación de robot desmalezador y planificación de trayectorias en entornos agrícolas
    (Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario, 2021-09) Ait, Ismael; Pire, Taihú; Kofman, Ernesto
    En los últimos años el uso de robots autónomos móviles ha experimentado un crecimiento considerable en diferentes sectores de la industria. La inevitable necesidad de aumentar la producción de alimentos debido al crecimiento en la población mundial, ha despertado en la industria agrícola un singular interés sobre estas nuevas tecnologías. Una de las partes principales de la navegación autónoma corresponde a la planificación de los caminos y trayectorias que el robot deberá seguir. Los algoritmos de planificación de caminos buscan generar una ruta puramente geométrica, libre de la colisión con obstáculos, que guíe al robot desde un punto inicial a un punto meta, mientras que la planificación de trayectorias añade la variable de tiempo a dicha ruta indicando la forma en la que el robot deberá recorrerla. En entornos agrícolas, un robot terrestre con ruedas debe recorrer el campo siguiendo las hileras de sembrado, para que de esta manera evite pisar los cultivos. Este problema puede extenderse buscando la optimización de alguna característica como ser la ruta de longitud mínima, la de menor tiempo de ejecución, la que pase lo más lejos posible de los obstáculos o la más suave, sólo por nombrar algunas. En este trabajo se presenta un sistema de navegación para el robot desmalezador de cultivos de soja desarrollado en el Centro Internacional Franco-Argentino de Ciencias de la Información y de Sistemas (CIFASIS), poniendo foco en la etapa de planificación de trayectorias. Para esto se utiliza el framework ROS (Robot Operating System) y el planificador local TEB (Timed Elastic Band). Dicho planificador optimiza las trayectorias del robot de forma iterativa partiendo de las rutas generadas por el planificador global y adaptándolas a las restricciones dinámicas y de maniobrabilidad del robot. Por otro lado, se desarrolla una simulación en Gazebo con un modelo virtual del robot desmalezador y varias configuraciones de campos agrícolas. Dicha simulación permite la prueba de las distintas partes del sistema de navegación, como ser la localización, mapeo, planificación de trayectorias y control del robot. Los resultados obtenidos muestran que el sistema es capaz de trabajar en tiempo real y con suficiente precisión para evitar el pisado de los cultivos. Adicionalmente, se estudia la generación de diferentes recorridos que le permiten al robot cubrir con sus rociadores la totalidad de las hileras de cultivos del campo de forma eficiente. Se obtienen recorridos que logran un ahorro de alrededor de un 20 % del tiempo de ejecución comparados con recorridos triviales.
  • ÍtemAcceso Abierto
    Conteo de plantas de girasol en cultivos en hileras a partir de imágenes UAV
    (Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario, 2023-03) Camussi, Fernando Javier; Larese, Mónica G.
    Las imágenes capturadas por UAV o drones se han vuelto muy útiles durante la última década en la agricultura de precisión, dada su practicidad y su bajo costo. Sin embargo, todavía queda mucho por explorar, actualmente el INTA realiza el conteo de plantas de girasol de forma manual sobre imágenes UAV pero no cuentan con una tecnología que les permita hacerlo de forma automática. En éste trabajo se propone una metodología compuesta por un conjunto de algoritmos para el conteo automático de plantas de girasol en cultivos en hileras a partir de imágenes UAV. Primero se realiza la segmentación de los objetos de plantas de girasol para separarlos del fondo utilizando el índice de vegetación ExG y el método de umbralamiento de Otsu, seguido de mejoras mediante operaciones moforlógicas a la máscara obtenida. Luego, se detecta la orientación de las hileras utilizando la imagen de autocorrelación de la máscara y se rota la imagen para que las hileras de los cultivos queden en forma horizontal. El tercer paso consiste en la detección de las hileras y el etiquetado de objetos de plantas de girasol que componen las mismas. Por último se estima la cantidad de plantas de girasol mediante regresión lineal. Para ello se entrenaron modelos utilizando las características de tamaño y forma de los objetos, tales como el área, el perímetro y la compacidad, que son calculadas a partir de un conjunto de coordenadas de plantas generado manualmente sobre un ortomosaico con plantas de girasol en el estadio 19 DDE. Para la detección de objeto de plantas de girasol se obtuvo una precision y recall de 0.95 y 0.94, respectivamente. En la etapa de testeo se obtuvieron valores de R2 de 0.96 para el conjunto de coordenadas de plantas y de 0.86 para el conteo realizado por el INTA. También se testeó en el estadio de crecimiento 27 DDE, cuando las plantas son más grandes y complejas, y se obtuvieron valores de R2 de hasta 0.80. La metodología propuesta resultó ser eficiente para el conteo de plantas de girasol, por lo que podemos imaginar un futuro prometedor, en el campo de la agricultura de precisión, para las tecnologías que combinen imágenes UAV con técnicas de procesamiento digital e inteligencia artificial.
  • ÍtemAcceso Abierto
    Una Infraestructura para la Inyección de las propiedades de la EBC en un sistema ERP
    (2018-04) Marchionno, Pablo Damián; Sartorio, Alejandro; Rocha, Cristian
    Este trabajo propone una solución de diseño e implementación para la inyección de propiedades funcionales de la Economía del Bien Común (EBC), propuesta por Christian Felber, en un sistema de gestión financiera y planificación (ERPm) de Municipios. Para este propósito se utilizaron técnicas y buenas prácticas de Ingeniería de Software que permitieron consolidar y mostrar el secreto de una metodología de trabajo basada en ICONIX y utilizando parte de la framework del proyecto open source Odoo para sus servicios de ERP. De esta manera se construyó una infraestructura de aplicación directa en las herramientas de sistemas informáticos, que utilizan Municipios y Comunas, para incorporar funcionalidades y propiedades de la EBC con el menor impacto técnico posible. Se expone un caso de uso real de aplicación donde quedará reflejado el alcance de esta solución.
  • ÍtemAcceso Abierto
    Detección de ataques maliciosos con aprendizaje automatizado
    (2018-07) Perrone, Gustavo Andrés; Grieco, Gustavo; Grinblat, Guillermo
    Año a año nuestras vidas dependen cada vez más de la tecnología, y de estar conectados a través de Internet. Progresivamente más y más objetos se conectan a Internet para facilitarnos diferentes funcionalidades. Celulares, autos, heladeras, cuentas bancarias, luces, casas, cámaras, televisores, etc. Estas conexiones nos brindan muchas ventajas y facilidades, pero a su vez aumentan la vulnerabilidad frente a ataques cibernéticos maliciosos. Estos pueden hacer caer sistemas, causar perdidas de datos, robar información privada, mover dinero, y muchos otros problemas. En los últimos años han surgido nuevos ataques sofisticado, persistentes y con objetivos concretos. Estas nuevas amenazas son denominadas Advanced Persistent Threats (Amenazas Persistentes y Avanzadas), también llamados APT. Estos ataques pueden perseguir objetivos económicos (espionaje), militares (búsquedas de debilidades, revelación de información), técnicos (credenciales, código fuente) o políticos (provocar desestabilización o desorganización, debilitar misiones diplomáticas). En vista de esta situación, y con el propósito de detectar y protegerse de estos ataques, ya no alcanza con programas tales como sistemas de detección de intrusos o antivirus que utilizan sistemas de reglas para detectar amenazas conocidas, si no que es necesario intentar prever lo desconocido. Día a día se investigan nuevas formas de detectar y prevenir amenazas en la red, generalmente utilizando técnicas de Aprendizaje Automatizado. Desgraciadamente, la detección de estos ataques altamente dirigidos requiere de grandes cantidades de datos que no están disponibles públicamente. Es por eso que esta tesina se centra en la detección de tráfico malicioso más general. Pero ¿qué técnicas son realmente efectivas en la práctica?, ¿son realmente implementables?, ¿qué se necesita para utilizarlas con éxito? En este trabajo muestro los resultados de investigar, probar y analizar varios de los algoritmos publicados, comprobando si son realmente aptos para utilizarse en situaciones reales.
  • ÍtemAcceso Abierto
    Redes neuronales adversarias para el reconocimiento de malezas
    (Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario, 2018-02) Baruffaldi, Juan Manuel; Uzal, Lucas
    Se aborda el problema de reconocimiento de malezas en video para poder realizar una aplicación de herbicidas selectiva de la maleza sobre campo con cultivo de soja. El sistema de reconocimiento propuesto es compatible además con la implementación de técnicas de robótica para remover la maleza con actuadores mecánicos sin el uso de agroquímicos. El problema es abordado con técnicas de Deep Learning, donde los datos de entrenamiento son filmaciones del campo con la presencia de cultivo y maleza. El sistema de visión propuesto está basado en Convolutional Neural Networks (CNN). Se utilizó la técnica de Generative Adversarial Networks (GAN) para hacer un pre-entrenamiento no supervisado del modelo de modo de explotar la gran cantidad de imágenes que se obtienen a partir de secuencias de video. Luego se entrena en forma supervisada con una mínima cantidad de datos etiquetados para especializar el modelo. Se analizan y comparan resultados de distintos métodos utilizados y su aporte en el reconocimiento. Se combinan dos redes discriminantes de Deep Convolutional Generative Adversarial Networks (DCGAN) y se utiliza una Support Vector Machines (SVM) en la última capa de la red entrenada sobre datos etiquetados utilizando Data Augmentation para lograr mayor robustez. Como resultado final se obtuvo un precisión sobre el conjunto de test de 91 %.
  • ÍtemAcceso Abierto
    Modelo de negociación multilateral basada en argumentación
    (Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario, 2018-07) Gorr, Emiliano D.; Casali, Ana; Pilotti, Pablo
    La negociación automática se presenta como una forma de interacción entre agentes autónomos con deseos de cooperar y alcanzar acuerdos para poder cumplir sus objetivos o para aumentar sus utilidades. En las ciencias de la computación la negociación automática se suele estudiar desde distintos enfoques y en diversos escenarios. Este trabajo hace un aporte a la negociación automática basada en argumentación en entornos multilaterales presentando un modelo de negociación sobre un escenario compuesto por múltiples agentes bilaterales al que se incorpora un agente especial denominado mediador. Estos agentes bilaterales, que son colaborativos y honestos, no pueden cumplir con sus objetivos por no contar con los recursos necesarios, por lo que deben negociar un intercambio de recursos que les permita conseguir lo necesario para alcanzar su objetivo. Estos agentes pueden tener conocimiento incompleto o incorrecto acerca del entorno de negociación. Al ser bilaterales, los agentes no pueden negociar simultáneamente con más de una contra-parte imposibilitando una negociación multilateral, por consiguiente se introduce en el entorno multiagente al agente mediador cuyo rol es el de ser la contra-parte de todos los agentes bilaterales que participan en la negociación. En este trabajo, se introduce el modelo multilateral junto a una primera versión del agentemediador. Luego se presenta una segunda versión de agente mediador que incorpora un motor de inferencia. Ambas versiones utilizan revisión de creencias para actualizar su estado mental. Se realizan simulaciones para comparar las dos versiones, resultando ser la segunda versión con la que se logra mayor cantidad de acuerdos pero a un costo computacional mayor.
  • ÍtemAcceso Abierto
    Concretización a Perl de casos de prueba abstractos generados a partir de especificaciones Z
    (Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario, 2020-11) Bonet, Javier; Cristiá, Maximiliano
    La investigacíón entorno a la especificación de sistemas de software se ha acrecentado los últimos años y se debe a la importancia que tienen éstas tanto para la construcción como para el mantenimiento de sistemas. La característica que hace a las especificaciones un punto clave en el desarrollo de software es la de proveer las herramientas necesarias para formalizar los requerimientos funcionales, comúnmente expresados en lenguaje natural y, por lo tanto, muy propensos a contener ambigüedades. La etapa de testing de software es otra de las áreas que se ve beneficiada por las especificaciones funcionales ya que el testing basado en modelos (MBT la siglas de su traducción del inglés Model-Based Testing) permite la generación de casos de prueba a partir de una especificación del sistema que se desea testear. Para su tesina de grado Pablo Rodríguez Monetti presenta una primera implementación de TTF (Test Template Framework) llamada Fastest. Esta herramienta es un framework de MBT que toma especificaciones en lenguaje Z como punto inicial del proceso. Esta implementación permite generar casos de prueba abstractos partiendo de una especificación Z. En sus respectivas tesinas de grado Diego Ariel Hollmann y Pablo Damián Coca extienden Fastest con módulos que permiten el refinamiento de casos de prueba abstractos, generados por Fastest, a casos concretos en los lenguajes C y Java, respectivamente. En su tesina Diego Ariel Hollmann presentó Test Case Refinement Language (TCRL de ahora en más), un lenguaje de refinamiento utilizado en ambos trabajos para establecer la correspondencia entre las variables de especificación y las de implementación. En esta tesina se presenta el lenguaje de refinamiento ATCAL, creado por el actualmente graduado en Licenciatura en Ciencias de la Computación Cristian Rosa como parte de un trabajo realizado para un post-doctorado. A éste, el autor hizo los agregados necesarios para completar su definición. En comparación con TCRL, se simplifican algunas de sus estructuras y se extiende su expresividad. Además, se implementa un nuevo módulo de Fastest que refina los casos abstractos de prueba a casos concretos en Perl. Junto con este desarrollo se presentan casos de estudio para ejemplificar el uso del lenguaje ATCAL como medio para describir los mapeos entre especificación funcional e implementación, además de los casos concretos generados, de modo tal que se hace posible realizar una comparación directa respecto a sus correspondientes casos abstractos.
  • ÍtemAcceso Abierto
    Generación de monitores C embebidos para especificaciones Lola
    (Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario, 2022-06) Ramirez, Aldana; Sánchez, César; Ceresa, Martin
    En las últimas décadas se ha experimentado un gran crecimiento en el desarrollo de sistemas embebidos para diversas áreas de aplicación, muchas de las cuales involucran sistemas críticos donde resulta imprescindible proveer garantías de correctitud. Las técnicas de verificación formal clásicas, que permiten demostrar matemáticamente propiedades de correctitud de un modelo, si bien proveen garantías fuertes, pueden resultar imprácticas o incluso imposibles de aplicar en sistemas completos de escala industrial. Como respuesta a este problema, el área de Runtime Verification estudia cómo generar monitores a partir de especificaciones declarativas, con el objetivo de analizar la traza de una (única) ejecución para verificar su correctitud. Con el tiempo, fueron surgiendo enfoques más expresivos que permiten realizar análisis más complejos, como es el caso de Lola, un lenguaje de especificación junto con algoritmos para el monitoreo de sistemas síncronos. Desde su publicación en 2005, han surgido numerosos trabajos basados en este lenguaje. Uno de los más recientes es hLola, un lenguaje de dominio específico embebido en Haskell para escribir especificaciones junto con un motor para ejecutar los monitores. Esta implementación presenta varias características atractivas, entre las que se destaca la extensibilidad del lenguaje a nuevos tipos de datos, algo no muy habitual en la mayoría de los lenguajes de Runtime Verification. A partir de estos antecedentes y de la experiencia de uso del lenguaje C en sistemas críticos, esta tesina presenta un lenguaje de dominio específico embebido en Haskell, llamado MCLola, para la síntesis de monitores C a partir de especificaciones de alto nivel basadas en el lenguaje Lola.
  • ÍtemAcceso Abierto
    Hacia un prototipo certificado del sistema de permisos de Android 10
    (Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario, 2022-11) De Luca, Guido; Luna, Carlos; Zanarini, Dante
    Android es un sistema operativo para dispositivos celulares que actualmente, acapara más del 85% del mercado. Permite a sus usuarios realizar múltiples tareas a través del uso de apps. Sin embargo, el fácil uso de las mismas y de la plataforma en general, se ve contrarrestado por una escalada en los riesgos en cuanto a confidencialidad de los datos y a la falta de garantías a la hora de proteger información delicada. Por este motivo, el sistema encargado de arbitrar los accesos a la información del usuario se convierte en un objetivo principal para la verificación de software usando métodos formales. En este trabajo, extendemos una formalización existente del sistema de permisos de Android 6, incorporando nuevas funcionalidades y demostrando nuevas propiedades para las versiones 7, 8, 9 y 10 de la plataforma. El resultado es un framework sobre el cual es posible razonar, de manera formal, sobre propiedades de safety y security de Android 10.
  • ÍtemAcceso Abierto
    EDSL en Haskell para la programaci ́on segura respecto a la propiedad Delimited Release
    (Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario, 2022-05) Latorre, Gonzalo de; Manzino, Cecilia
    La confidencialidad de la información manipulada por sistemas informáticos ha tomado mayor importancia con el uso creciente de aplicaciones a través de internet. Los mecanismos de seguridad tradicionales como control de acceso o criptografía no proveen protección punta a punta de los datos: funcionan eficientemente en limitar su acceso, pero no pueden hacer nada para evitar su propagación. Para complementar estos mecanismos de seguridad, surgen las técnicas de control de flujo de información (IFC, Information-Flow Control), las cuales permiten establecer garantías sobre la confidencialidad e integridad de los datos. analizando cómo fluye la información dentro del programa. En este contexto surgen políticas de confidencialidad que garantizan que la información confidencial no puede ser inferida a partir de los datos públicos. No-interferencia es un ejemplo de una política de seguridad. Lo interesante de esta propiedad es que puede ser chequeada de manera estática mediante un sistema de tipos, por lo tanto, cuando un programa tipa en ese sistema de tipos, significa que satisface la propiedad de seguridad. Para que los lenguajes de seguridad tengan utilidad práctica necesitamos mecanismos de desclasificación, en los cuales el flujo de información sea controlado y al mismo tiempo se permita liberar información confidencial a canales públicos, pero solo de manera permitida y controlada, la cual la propiedad de no-interferencia resulta ser demasiado restrictiva. Delimited Release es una propiedad de seguridad que garantiza que la desclasificación no puede ser usada para filtrar información de manera no deseada. El objetivo de esta tesina es desarrollar un lenguaje de dominio específico embebido en Haskell para escribir programas seguros respecto a la propiedad Delimited Release.
  • ÍtemAcceso Abierto
    String Matching Aproximado mejorado con SIMD
    (Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario, 2019-12) Fiori, Fernando Jesús; Tarhio, Jorma
    Consideramos la versión de k sustituciones de String Matching Aproximado (o búsqueda aproximada de cadenas) para uno solo y múltiples patrones. El problema básicamente consiste en encontrar todas las ocurrencias de uno o más patrones con a lo sumo k sustituciones de caracteres en un texto. Dada la gran popularidad de las extensiones de conjuntos de instrucciones SIMD (Single Instruction Multiple Data) en las CPUs actuales, presentamos nuevos algoritmos eficientes para este problema que las aprovechan. Medimos el rendimiento de cada nuevo algoritmo mediante pruebas exhaustivas en diferentes textos de la vida real comparándolo con los algoritmos más competitivos conocidos hasta la fecha. Tomamos un enfoque práctico al tratar de mejorar el tiempo promedio de cada algoritmo.
  • ÍtemAcceso Abierto
    Aplanado eficiente de grandes sistemas de ecuaciones algebraico-diferenciales
    (Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario, 2020-12) Marzorati, Denise; Kofman, Ernesto; Fernandez, Joaquín
    Diversas ramas de la ciencia y de la técnica utilizan modelos matemáticos de los sistemas que estudian. Sobre estos modelos matemáticos se realizan simulaciones para analizar el comportamiento de dichos sistemas. Dado que estas técnicas son aplicadas a sistemas cada vez más complejos y grandes, permanentemente surgen nuevos desafíos. Los sistemas dinámicos continuos suelen ser representados mediante sistemas de ecuaciones diferenciales algebraicas (EDAs), y su simulación requiere de la resolución numérica de dichas ecuaciones, que puede hacerse a través de algoritmos específicos conocidos como solvers. Los solvers requieren que los sistemas de ecuaciones estén escritos y ordenados de cierta forma, que generalmente no coincide con la manera en la que un/una especialista describe los modelos. Para convertir los modelos desde una representación orientada a objetos, tal como la usada por los lenguajes de modelado modernos, en una representación de ecuaciones ordenadas y estructuradas, como la requieren los solvers, se recurre a diversos algoritmos que conforman un "compilador de modelos". Estos algoritmos están basados, en su mayor parte, en la Teorı́a de Grafos. En esta tesina se describe la formulación e implementación de nuevos algoritmos para convertir modelos orientados a objetos de gran escala en sistemas de ecuaciones. Estos algoritmos están principalmente basados en la teorı́a de grafos y tienen la propiedad de lograr un costo computacional constante con respecto al tamaño de los arreglos involucrados. Para esto, hacen uso de una nueva categoría de grafos denominados "Grafos Basados en Conjuntos", que permiten representar y manipular conjuntos de vértices y aristas de manera compacta.
  • ÍtemAcceso Abierto
    Invertibilidad de un generador entrenado adversariamente
    (Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario, 2019) Pividori, Marcos; Uzal, Lucas; Grinblat, Guillermo
    Las Redes Adversarias Generativas (GAN) han demostrado resultados excepcionales en el modelado de la distribución de imágenes naturales, aprendiendo representaciones latentes que capturan variaciones semánticas sin supervisión. Además de la generación de imágenes nuevas, es de especial interés explotar la capacidad del generador GAN para modelar el manifold de las imágenes naturales y, por lo tanto, generar cambios creíbles al manipular imágenes. Sin embargo, esta línea de trabajo está condicionada por la calidad de las reconstrucciones obtenidas sobre las imágenes reales al proyectarlas al espacio latente. Mientras que trabajos previos solo han considerado la inversión hasta el espacio latente, en este trabajo proponemos explotar la representación en las capas intermedias del generador, y mostramos que esto conduce a una mayor capacidad. En particular, observamos que la representación después de la primera capa densa, presente en todos los modelos GAN del estado del arte, es lo suficientemente expresiva como para representar imágenes naturales con gran fidelidad visual. Es posible interpolar entre estas imágenes obteniendo una secuencia de nuevas imágenes sintéticas de gran calidad que no se pueden generar desde el espacio latente. Finalmente, como ejemplo de aplicaciones potenciales que surgen de este mecanismo de inversión, mostramos que se puede explotar la representación aprendida en el mapa de atención del generador para obtener una segmentación no supervisada de imágenes naturales.
  • ÍtemAcceso Abierto
    Codificación y reconstrucción de rostros con redes adversarias generativas
    (Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario, 2020) Zanetti, Álvaro; Uzal, Lucas
    Se ha observado que en una arquitectura GAN en general es difícil obtener una función inversa del generador (G), es decir, una función tal que dada una imagen se obtenga el vector Z que le permita al generador reconstruir tal imagen. El objetivo de esta tesina es estudiar este procedimiento de inversión considerando un dataset de rostros conformado por una única identidad, entendiendo que esta restricción simplificaría dicho proceso. Además, se desea comparar los resultados obtenidos con otros datasets de identidades diversas y mayor complejidad. Se desea investigar si esta simplificación del dataset permite lograr mejores reconstrucciones con el procedimiento anteriormente descripto. Por otro lado, e independientemente de lo anterior, el entrenamiento adversario de un generador que permita obtener imágenes de una determinada identidad abre la posibilidad de diversas aplicaciones como la generación y animación de rostros sintéticos de una determinada persona, representación visual de chatbots, y en términos de seguridad informática, suplantación de identidad en sistemas de validación por reconocimiento facial en video. Por lo tanto, un objetivo secundario, es evaluar el potencial de estas técnicas para las mencionadas aplicaciones.
  • ÍtemAcceso Abierto
    Odometría visual monocular basada en redes adversarias generativas
    (Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario, 2019) Cremona, Javier Alejandro; Pire, Taihú; Uzal, Lucas C.
    Uno de los principales desafíos a resolver en el campo de la robótica móvil es el de lograr que un robot autónomo pueda estimar su posición y orientación en el entorno que se encuentra navegando. Al problema de estimar el desplazamiento de un robot incrementalmente a partir de una secuencia de imágenes entrante se lo denomina Visual Odometry (VO). En los últimos años las redes neuronales convolucionales (CNN) han sido aplicadas a diversos problemas de Computer Vision, y VO no fue la excepción. En este trabajo se propone el uso de una CNN para resolver el problema de VO. Para esto, se emplea un tipo particular de CNN conocido como Generative Adversarial Network (GAN) que permite realizar su entrenamiento mediante una técnica semi-supervisada, la cual incluye imágenes reales e imágenes generadas artificialmente por la propia red. Se evaluó la performance y la precisión de dicho sistema en datasets de dominio público. Concretamente, la propuesta se centra en vehículos autónomos, pero la solución podría extrapolarse a otros tipos de robots. Los resultados obtenidos muestran que el sistema es capaz de trabajar en tiempo real y su precisión es comparable con sistemas similares del estado del arte. El método propuesto recibe el nombre de WGANVO y su código se libera junto con todo el software desarrollado como software libre para facilitar su uso por la comunidad de Robótica Móvil y de Aprendizaje Profundo.