GESTIÓN DEL DISEÑO Y LA INNOVACIÓN EN LA RELACIÓN UNIVERSIDAD - ENTRAMADO SOCIO-PRODUCTIVO

PROBLEMA DE INVESTIGACION El problema que aborda la investigación es la falta de transferencia de conocimientos de diseño + innovación (arquitectura, diseño industrial, diseño gráfico, etc.) al sistema socio productivo de la provincia de Córdoba, lo cuál afecta la productividad y la competitividad de las empresas y, por otra parte, dificulta la inserción laboral de los profesionales formados en las universidades del medio. La provincia de Córdoba posee un importante potencial industrial que intenta contrabalancear el predominio de la región metropolitana de Buenos Aires. Las áreas de mayor desarrollo son la automotriz, metal-mecánica, agro-industrial, la construcción y la alimentaría. El diseño correctamente gestionado, constituye una fuente de ventajas comparativas, una eficaz metodología para la innovación de productos y procesos y un factor de rentabilidad económica. Por otro lado, existe una falta de respuesta a problemas relacionados al diseño, (como los aspectos relativos a la calidad de vida, la responsabilidad social y la protección del ambiente, por mencionar algunos) que no son formulados como prioridades cuantitativas en los productos de diseño promovidos por las empresas. En este sentido, las Universidades de la Red, cuentan con instrumentos específicos a nivel de grado y postgrado para promover la interrelación entre Universidad, Empresas y Ongs de la Provincia. La carrera de Diseño Industrial de la Universidad Nacional de Córdoba y la Maestría en Diseño de la Universidad Católica de Córdoba han estado cooperando desde inicios del 2009 en la conformación del Programa Córdoba Diseña del Ministerio de Ciencia y Tecnología de la Provincia de Córdoba, que tiene el objetivo de "desarrollar y orientar las capacidades de análisis, evaluación y asistencia técnica en temas referidos al Diseño, para el gobierno, las empresas, las universidades y centros de investigación". En el marco de ese programa del que las universidades participantes son miembros, existe un diagnóstico incipiente de los requerimientos de las empresas, y de la actividad de los diseñadores en la provincia. Al mismo tiempo, se ve necesario recabar datos sobre los requerimientos de diseño desde el sector de organizaciones no gubernamentales y sin fines de lucro. A los efectos de contar con un relevamiento que posibilite un diagnóstico más preciso, es necesario sistematizar y cruzar los datos que se derivan de: la conformación del entramado socio-productivo de la provincia, la oferta académica y el capital humano que estamos formando en las Universidades. Ambas universidades integrantes de la Red, cuentan con una reconocida trayectoria en el Área de Diseño y con capital humano de diferentes disciplinas (diseño industrial, arquitectura, gestión pública, sociología, etc.) para llevar adelante el proyecto. Los resultados del proyecto servirán para formular un marco teórico específico, fundamentar estrategias de mejoramiento de la calidad académica, delinear propuestas de sistemas asociativos y definición de prioridades de líneas de investigación para mejorar la eficiencia de la relación Universidades-Empresas-Sociedad. Por otra parte, posibilitarán relevar las demandas del medio-socio productivo en términos de la formación profesional requerida, la inserción de los profesionales y la importancia de la innovación en tanto valor agregado a productos y procesos en el entramado socio-productivo de la provincial de Córdoba. OBJETIVOS - Analizar, sistematizar y consolidar información respecto a la experiencia acumulada, las capacidades actuales y las potencialidades en materia de diseño e innovación en Córdoba. - Identificar las empresas del medio productivo local y las organizaciones del tercer sector que demandan profesionales formados en diseño e innovación, e indagar sobre los requerimientos que plantean en términos de competencias y formacion académica. -Identificar los desfasajes que pudieran existir en relación a la demanda que plantea el medio productiv

ESTUDIOS E INVESTIGACIONES APLICADAS A LA GESTIÓN INTEGRAL DE LOS RESIDUOS SOLIDOS URBANOS EN PEQUEÑAS POBLACIONES DE LA REGIÓN CENTRAL DE LA PROVINCIA DE CÓRDOBA.

El presente proyecto se propone investigar de modo integral el problema de los residuos sólidos en varios municipios de la zona centro de la Provincia de Córdoba, elaborar y colaborar con la ejecución de soluciones concurrentes al manejo, atenuación o resolución del problema. La filosofía tecnológica que se asume frente al problema de los residuos sólidos urbanos (RSU) es la de investigar formas y procesos tendientes a aplicar en sitios concretos políticas propuestas a nivel nacional (Estrategia Nacional para la Gestión Integral de Resíduos Sólidos Urbanos, ENGIRSU), consistentes en promover la separación de los resíduos en su lugar de origen, en diferentes categorías que permitan su manejo; su clasificación en aquellas que permitan su reciclado o utilización; y la disposición final del resto mediante técnicas ambientalmente adecuadas. Este tipo de procesos está bastante estudiado en el caso de ciudades grandes (n>200.000 habitantes), pero sus propuestas no son facilmente adaptables a pequeñas poblaciones, principalmente por una cuestión de escalas. Sin embargo, éstas últimas pueden tener a su favor una respuesta social más fácil de construir, sobre todo a partir de la comprensión del problema que representan los RSU y el costo que involucra su gestión, teniendo además como fortaleza adicional la disponibilidad de terrenos libres en sus cercanias. El desarrollo del proyecto incluye tareas de relevamiento y estudio de las situaciones existentes en las diferentes poblaciones y el establecimiento de una linea de base para cada una de ellas. Como aplicaciones surgidas de lo anterior, se llevarán a cabo actividades de tipo socio cultural para promover la conciencia de la separación de los resíduos en los hogares; el diseño y desarrollo de manuales e instructivos para facilitar la tarea; la capacitación de jóvenes estudiantes secundarios en las diferentes localidades, para sumarlos como gestores culturales en el tema; el diseño de sistemas asociativos para las tareas de clasificación y reciclaje; la asistencia técnica para integrar sistemas de manejo y/o comercialización conducentes a la sustentabilidad del proceso (al menor costo posible para los municipios); el diseño y desarrollo de tecnologías simples para las operaciones que requiera el manejo de cada categoría; el estudio -en cada caso- del mejor proceso de disposición final de los residuos remanentes; el estudio de la posible presencia de contaminantes o tóxicos; la elaboración de documentos que posibiliten extender los resultados alcanzados a otras localidades. Se trata de un proyecto de investigación aplicada a la búsqueda de soluciones adaptadas para cada uno de los municipios seleccionados. Entre ellos podemos encontrar algunos que ya han iniciado con relativo éxito la etapa de separación en origen y requieren apoyo tecnológico y organizacional para las etapas siguientes y otros que aún no tienen nada iniciado. Hay municipios de diferente tamaño y naturaleza, unos con presencia industrial, otros principalmente agropecuarios. El proyecto se propone dos grandes objetivos generales: por un lado, operar sobre la conciencia social para sumar voluntades y conductas tendientes a simplificar el problema; reducir la generación de resíduos, clasificarlos y separarlos en origen según diferentes categorías y facilitar la gestión de recolección. Por otro lado se plantean desarrollos tecnológicos (ingenieriles) conducentes a simplificar y disminuir los costos de las operaciones de clasificación, recuperación o reciclado, o resolviendo aspectos que faciliten su transporte a los centros de recepción de cada categoría. Paralelamente se estudiarán temas particulares como son el manejo de residuos peligrosos y/o tóxicos; los residuos electrónicos; las sustancias químicas; los agroquímicos (abundantes en la región), etc.

Plataforma Framework distribuida para detección temprana de trastornos de déficit de atención en escuelas de nivel primario.

El desarrollo de dicho proyecto intenta dar solución a la problemática de la detección temprana y eficiente de los Trastornos de Déficit de Atención en las escuelas primarias, mediante la construcción de una plataforma informática framework segura, portable y con una interfaz simple y amigable, en entornos distribuídos para el armado de diferentes escenarios de evaluación, test y encuestas para el alumno, la familia y los educadores, que con un enfoque multidisciplinario recaba información permitiendo al profesional a cargo realizar una detección acertada, un diagnóstico eficaz y un tratamiento acorde a las deficiencias psicológicas y de aprendizaje. Proceso lento e imposible de llevar adelante en la actualidad. Modelo: el psicopedagogo genera los test en la plataforma y los activa para que cada alumno los realice en los laboratorios, sus padres y educadores completan las encuestas activas en internet o via mobile o acceden a los laboratorios del colegio. Psicopedagogos analizan resultados obtenidos y emiten conclusión sobre cada caso, para que padres pueden verlos por cualquier medio antes mencionado, siempre con acceso seguro, y a los sectores activados. Beneficios: sociales en la detección de problemas cognitivos en los niños en escuelas primarias, mejorando problemas de los grupos escolares en donde se encuentran niños con TDA, beneficiando la comunicación con las familias con todo lo referido a sus hijos. Las empresas serían otra posible implementación..

Optimización de Arquitecturas de Procesamiento Digital de Señales en Lógica Programable para Aplicaciones en Vuelos No Tripulados

En dispositivos electrónicos de última generación destinados a funciones de comunicación o control automático, los algoritmos de procesamiento digital de señales trasladados al hardware han ocupado un lugar fundamental. Es decir el estado de arte en el área de las comunicaciones y control puede resumirse en algoritmos basados en procesamiento digital de señales. Las implementaciones digitales de estos algoritmos han sido estudiadas en áreas de la informática desde hace tiempo. Sin embargo, aunque el incremento en la complejidad de los algoritmos modernos permite alcanzar desempeños atractivos en aplicaciones específicas, a su vez impone restricciones en la velocidad de operación que han motivado el diseño directamente en hardware de arquitecturas para alto rendimiento. En este contexto, los circuitos electrónicos basados en lógica programable, principalmente los basados en FPGA (Field-Programmable Gate Array), permiten obtener medidas de desempeño altamente confiables que proporcionan el acercamiento necesario hacia el diseño electrónico de circuitos para aplicaciones específicas “ASIC-VLSI” (Application Specific Integrated Circuit - Very Large Scale Integration). En este proyecto se analiza el diseño y la implementación de aquitecturas electrónicas para el procesamiento digital de señales, con el objeto de obtener medidas reales sobre el comportamiento del canal inalámbrico y su influencia sobre la estimación y el control de trayectoria en vehículos aéreos no tripulados (UAV, Unmanned Aerial Vehicle). Para esto se propone analizar un dispositivo híbrido basado en microcontroladores y circuitos FPGA y sobre este mismo dispositivo implementar mediante algoritmo un control de trayectoria que permita mantener un punto fijo en el centro del cuadro de una cámara de video a bordo de un UAV, que sea eficiente en términos de velocidad de operación, dimensiones y consumo de energía.

Verificación de Sistemas Basada en Teoría de Tipos. System verification in type theory

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. This project is about using type theory to garantee program correctness. It follows three different directions: 1) Finding new type-checking algorithms based on normalization by evaluation. First, we would show that recent results like [16,17] extend to other type systems like: Martin-Löf´s type theory without eta rule, PTSs, type systems with variables (in addition to systems in [16,17] which are a la de Bruijn), systems with rewrite rules. This will be done by adjusting the proofs in [16,17] so that they apply to such systems as well. We will also try to obtain a more general definition of categories with families and normalization by evaluation, formulated in categorical terms. We expect this may turn proof-assistants more automatic and useful. 2) Exploring the proposal in [22] to compiler construction for Algol-like languages using functorial categories. According to [22] such approach is suitable for verifying compiler correctness, claim which was never explored. First, the language Peal [29] will be certified in type theory and we will gradually add funtionality to it until a correct compiler for the language Forsythe [23] is obtained. 3) Formilizing systems for session types. Several proposals have shown to be faulty [30]. This means that a formalization of it may contribute to the general understanding of session types.

GANADERÍA DE PRECISIÓN. DESARROLLO DE UN SISTEMA ELECTRÓNICO PARA CONSTRUIR MATRICES GENEALÓGICAS APLICABLES AL MEJORAMIENTO ANIMAL EN DIVERSAS ESPECIES.

El mejoramiento animal tiene como función modificar genéticamente una población animal con un fin económico determinado. Las herramientas que se utilizan son: evaluación genética, selección y/o esquemas de apareamiento. La evaluación genética se realiza obteniendo información (marcadores) que predice el genotipo del animal que no es registrable directamente. Estos marcadores son el fenotipo o información física del animal y algún predictor del genotipo que puede ser un marcador químico o la relación de parentesco con otro animal. El uso de los marcadores genéticos para determinar la genealogía está en desarrollo actualmente pero resulta extremadamente costoso para ciertos niveles de producción. Los dispositivos electrónicos ensayados hasta el momento no han resultado muy eficientes, por lo tanto se propone para este proyecto desarrollar un sistema electrónico de identificación animal que permita construir matrices de genealogía para la evaluación genética de reproductores de las diferentes especies en condiciones de producción extensivas. El proyecto se desarrollará entre especialistas en mejoramiento animal e ingenieros electrónicos, en un aporte multidisciplinario a la solución del problema de establecer la filiación a través del armado del para macho-hembra durante el servicio natural de las distintas especies y el par madre-cría en algún momento luego del parto. La solución propuesta consiste en la implementación de dispositivos electrónicos activos (microcontrolador y tranceptor de radiofrecuencia alimentados a batería) dispuestos como nodos de una red de sensores inalambricos. Estos dispositivos serán colocados en los animales tomados como objeto de estudio, y mediante el continuo intercambio de informacion entre ellos se genera una matriz de datos que permita a posterior establecer la relación que existe entre ellos a traves de la determinacion de la periodicidad de sus cercanias relativas.

Aceleración de Algoritmos en Procesadores Multicore, GPGPU y FPGA

El avance en la potencia de cómputo en nuestros días viene dado por la paralelización del procesamiento, dadas las características que disponen las nuevas arquitecturas de hardware. Utilizar convenientemente este hardware impacta en la aceleración de los algoritmos en ejecución (programas). Sin embargo, convertir de forma adecuada el algoritmo en su forma paralela es complejo, y a su vez, esta forma, es específica para cada tipo de hardware paralelo. En la actualidad los procesadores de uso general más comunes son los multicore, procesadores paralelos, también denominados Symmetric Multi-Processors (SMP). Hoy en día es difícil hallar un procesador para computadoras de escritorio que no tengan algún tipo de paralelismo del caracterizado por los SMP, siendo la tendencia de desarrollo, que cada día nos encontremos con procesadores con mayor numero de cores disponibles. Por otro lado, los dispositivos de procesamiento de video (Graphics Processor Units - GPU), a su vez, han ido desarrollando su potencia de cómputo por medio de disponer de múltiples unidades de procesamiento dentro de su composición electrónica, a tal punto que en la actualidad no es difícil encontrar placas de GPU con capacidad de 200 a 400 hilos de procesamiento paralelo. Estos procesadores son muy veloces y específicos para la tarea que fueron desarrollados, principalmente el procesamiento de video. Sin embargo, como este tipo de procesadores tiene muchos puntos en común con el procesamiento científico, estos dispositivos han ido reorientándose con el nombre de General Processing Graphics Processor Unit (GPGPU). A diferencia de los procesadores SMP señalados anteriormente, las GPGPU no son de propósito general y tienen sus complicaciones para uso general debido al límite en la cantidad de memoria que cada placa puede disponer y al tipo de procesamiento paralelo que debe realizar para poder ser productiva su utilización. Los dispositivos de lógica programable, FPGA, son dispositivos capaces de realizar grandes cantidades de operaciones en paralelo, por lo que pueden ser usados para la implementación de algoritmos específicos, aprovechando el paralelismo que estas ofrecen. Su inconveniente viene derivado de la complejidad para la programación y el testing del algoritmo instanciado en el dispositivo. Ante esta diversidad de procesadores paralelos, el objetivo de nuestro trabajo está enfocado en analizar las características especificas que cada uno de estos tienen, y su impacto en la estructura de los algoritmos para que su utilización pueda obtener rendimientos de procesamiento acordes al número de recursos utilizados y combinarlos de forma tal que su complementación sea benéfica. Específicamente, partiendo desde las características del hardware, determinar las propiedades que el algoritmo paralelo debe tener para poder ser acelerado. Las características de los algoritmos paralelos determinará a su vez cuál de estos nuevos tipos de hardware son los mas adecuados para su instanciación. En particular serán tenidos en cuenta el nivel de dependencia de datos, la necesidad de realizar sincronizaciones durante el procesamiento paralelo, el tamaño de datos a procesar y la complejidad de la programación paralela en cada tipo de hardware.

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.

Sistemas de diálogo con aplicaciones en Educación

En este proyecto se investigan 3 subáreas de Inteligencia Artificial y sus aplicaciones en contextos educativos. Las 3 áreas son 1) agentes conversacionales automatizados que actúan como instructores virtuales o sistemas de tutoring automatizado, 2) asistentes virtuales que llevan a cabo una tarea dada bajo la instrucción de un aprendiz avanzado, y 3) plataformas de programación de chatbots como una herramienta educativa para enseñar conceptos básicos de ciencias de la computación. La hipótesis de este proyecto es que tanto los tutores como los asistentes conversacionales automatizados deben incluir una representación contextual rica que identifique lo entendido por el aprendiz hasta el momento y ser capaces de realizar inferencias sobre ella para poder guiar mejor su aprendizaje. Los objetivos de este proyecto incluyen el desarrollo de algoritmos de inferencia contextuales apropiados para instructores y asistentes virtuales, el desarrollo de algoritmos para la programación simplificada de chatbots, la evaluación de estos algoritmos en pruebas piloto en escuelas y la realización de un curso online abierto masivo para estudiantes de secundario del programa Conectar Igualdad que quieran aprender sobre Inteligencia Artificial y Ciencias de la Computación. El método a utilizar será la realización de recolección de corpus (interacciones humano-humano de las interacciones tutor-aprendiz), la aplicación de técnicas de procesamiento de lenguaje natural como la generación por selección y la interpretación por clustering y maximum entropy models usando características sintácticas, semánticas y pragmáticas. Se desarrollarán los algoritmos siguiendo una metodología estándar de Ingeniería de Software y se evaluarán en experiencias piloto en escuelas secundarias así como en un curso online abierto y masivo. Además se dictará un curso de capacitación docente para la incorporación de las tecnologías producidas a sus cursos. Como resultado se espera la contribución al área de Inteligencia Artificial con aplicaciones en Educación de algoritmos evaluados empíricamente en entornos educativos reales del nivel medio. Además, se espera contribuir a las metodologías de enseñanza de Ciencias de la Computación en el nivel medio. Este proyecto es relevante a la realidad nacional y mundial de falta de recursos humanos formados en las Ciencias de la Computación y al crecimiento mundial que el área de Inteligencia Artificial en general y de Sistemas de diálogo (o interfaces conversacionales) en particular ha tenido en los últimos años con el crecimiento exponencial de la tecnología en la vida diaria.

Estudios experimentales y teóricos de materiales y su optimización para uso como electrodos de baterías de ión-litio.

El presente proyecto se enmarca en el contexto del desarrollo de vectores de energía, particularmente aquellos destinados a almacenar la energía captada desde fuentes alternativas y sustentables, como son las energías eólica y solar, entre otras. Uno de los vectores de energía actualmente más importante lo constituyen las baterías de ión-Litio, las que por sus características de pequeño tamaño, alta densidad de energía y potencia, y larga ciclabilidad, son ampliamente utilizadas para alimentar todos los dispositivos electrónicos de pequeño tamaño (teléfonos móviles, notebooks, etc.). Este tipo de batería es, hasta el momento, la única que puede satisfacer la demanda de voltaje e intensidad de corriente, junto con bajo peso y volumen, del motor de un vehículo eléctrico, por lo que se espera un gran crecimiento de su demanda cuando comience la consolidación del mercado de este tipo de vehículos. Sin embargo, esto sólo será posible con importantes mejoras en los materiales activos que componen ambos electrodos, ánodo y cátodo, y/o con el desarrollo de nuevos materiales activos, que incrementen aun más la densidad de energía almacenada en dichas batería. En la Universidad Nacional de Córdoba hemos constituido un grupo de trabajo abocado a la investigación y desarrollo de materiales activos para ser utilizados como electrodos en este tipo de baterías, un área de investigación que concentra cada vez más la atención de científicos y tecnólogos en todo el mundo, particularmente, de países líderes del sector de electrónica y automotriz. Entre los objetivos del proyecto se pueden mencionar la intención de desarrollar capacidades científicas y técnicas en aspectos de investigación básica y tecnológica de sistemas electroquímicos de almacenamiento de energía, mediante la instalación de un laboratorio de síntesis, caracterización, investigación y ensayo de materiales activos para electrodos de baterías de ión-Litio. Específicamente, se llevará adelante la preparación y estudio electroquímico de materiales de ánodo en base a diferentes tipos de carbonos, de diferentes compuestos de titanatos de metales alcalinos, y de materiales de cátodo en base a diferentes tipos de compuestos de espinelas de fosfato de M-Litio, donde M puede ser Fe, Mn, Ni, Co o mezclas, y el ensayo posterior de celdas prototipo. La metodología de trabajo a aplicar es la del estado-del-arte a nivel mundial, que consiste en las etapas de síntesis, caracterización y estudio de funcionamiento de diferentes tipos de materiales activos para electrodos (ánodo o cátodo) de baterías de ión-Litio. Los procesos de síntesis comprenderán métodos por vía seca desde precursores adecuados (tratamientos térmicos) o por vía húmeda (hidrotermal, sol-gel). La caracterización física, química, estructural y morfológica abarcará la aplicación de técnicas de análisis de área específica y porosidad por método BET, microscopías SEM y TEM, análisis químico EDX, difracción de rayos X, espectroscopías XPS y Raman, y RMN, entre otras. Los estudios electroquímicos se llevarán a cabo utilizando técnicas potenciodinámicas, de multipulsos de potencial, galvanostáticas a diferentes densidades de corriente, espectroscopía de impedancia electroquímica y de ciclados de carga/descarga. Con la ejecución del proyecto se espera obtener materiales activos para electrodos de baterías de ión-Litio que cumplan con características tales como: alta capacidad de carga, adecuada densidad de potencia, alto grado de ciclabilidad, alto grado de seguridad, alta resistencia al envejecimiento, tanto estático como dinámico, y bajo costo del material. Teniendo en cuenta la inminente crisis en la producción mundial de combustibles fósiles líquidos, la necesidad de mudar la tecnología de vehículos actuales a la de vehículos eléctricos, y la disponibilidad nacional de recursos minerales de litio, la importancia del proyecto es directa para avanzar hacia un desarrollo tecnológico regional propio e independiente.

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.

Mecanización de semántica de lenguajes de programación: teoría, implementación y desarrollo.

El presente proyecto se enmarca en el área de métodos formales para computación; el objetivo de los métodos formales es asegurar, a través de herramientas lógicas y matemáticas, que sistemas computacionales satisfacen ciertas propiedades. El campo de semántica de lenguajes de programación trata justamente de construir modelos matemáticos que den cuenta de las diferentes características de cada lenguaje (estado mutable, mecanismos de paso de parámetros, órdenes de ejecución, etc.); permitiendo razonar de una manera abstracta, en vez de lidiar con las peculiaridades de implementaciones o las vaguezas de descripciones informales. Como las pruebas formales de corrección son demasiado intrincadas, es muy conveniente realizar estos desarrollos teóricos con la ayuda de asistentes de prueba. Este proceso de formalizar y corrobar aspectos semánticos a través de un asistente se denomina mecanización de semántica. Este proyecto – articulado en tres líneas: semántica de teoría de tipos, implementación de un lenguaje con tipos dependientes y semántica de lenguajes imperativos con alto orden - se propone realizar avances en el estudio semántico de lenguajes de programación, mecanizar dichos resultados, e implementar un lenguaje con tipos dependientes con la intención de que se convierta, en un mediano plazo, en un asistente de pruebas. En la línea de semántica de teoría de tipos los objetivos son: (a) extender el método de normalización por evaluación para construcciones no contempladas aun en la literatura, (b) probar la adecuación de la implementación en Haskell de dicho método de normalización, y (c) construir nuevos modelos categóricos de teoría de tipos. El objetivo de la segunda línea es el diseño e implementación de un lenguaje con tipos dependientes con la intención de que el mismo se convierta en un asistente de pruebas. Una novedad de esta implementación es que el algoritmo de chequeo de tipos es correcto y completo respecto al sistema formal, gracias a resultados ya obtenidos; además la implementación en Haskell del algoritmo de normalización (fundamental para el type-checking) también tendrá su prueba de corrección. El foco de la tercera línea está en el estudio de lenguajes de programación que combinan aspectos imperativos (estado mutable) con características de lenguajes funcionales (procedimientos y funciones). Por un lado se avanzará en la mecanización de pruebas de corrección de compiladores para lenguajes Algollike. El segundo aspecto de esta línea será la definición de semánticas operacional y denotacional del lenguaje de programación Lua y la posterior caracterización del mismo a partir de ellas. Para lograr dichos objetivos hemos dividido las tareas en actividades con metas graduales y que constituyen en sí mismas aportes al estado del arte de cada una de las líneas. La importancia académica de este proyecto radica en los avances teóricos que se propone en la línea de semántica de teoría de tipos, en las contribución para la construcción de pruebas mecanizadas de corrección de compiladores, en el aporte que constituye la definición de una semántica formal para el lenguaje Lua, y en el desarrollo de un lenguaje con tipos dependientes cuyos algoritmos más importantes están respaldados por pruebas de corrección. Además, a nivel local, este proyecto permitirá incorporar cuatro integrantes al grupo de “Semántica de la programación”.