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.

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.

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.

EICAR, Electrónica, Informática, Comunicaciones, Automática y Robótica para la producción de bienes y servicios (Programa de ModernizaciónTecnológica III I-P - PAE 2006)

El presente proyecto denominado “EICAR, Electrónica, Informática, Comunicaciones, Automática y Robótica para la Producción de Bienes y Servicios” asocia estratégicamente a un importante grupo de instituciones del sector científico-tecnológico, privado y gobierno con el objetivo de formar recursos humanos altamente capacitados, desarrollar conocimiento y tecnología de punta, en el campo convergente de la electrónica, informática y computación industrial, comunicaciones y automática, y su transferencia para el desarrollo activo de sectores estratégicos del país, a través de la ejecución de seis Programas: 1) Desarrollo de sistemas inteligentes para eficientizar el uso racional de la energía; 2) I+D para el desarrollo de sistemas complejos de aeronáutica y aeroespacio; 3) Desarrollos para la plataforma de TV Digital y su integración a Internet; 4) Trazabilidad de productos agropecuarios y agroindustriales; 5) Elaboración de un plan estratégico para el desarrollo de infraestructura en TICs del Corredor Bioceánico del Centro basado en sistemas GPS y Proyecto Galileo; 6) Monitoreo de las tendencias tecnológicas de los Programas propuestos.

Plataforma informática aplicada como ayuda al proceso de enseñanza-aprendizaje de la educación primaria y secundaria de la Provincia de Córdoba: La integración de las Nuevas Tecnologías (NTICs) para el proceso de enseñanza-aprendizaje en entornos virtuales y colaborativos como complemento a la enseñanza tradicional

A partir del proyecto de Responsabilidad Social Universitaria del año 2008: “Aplicaciones del Análisis Matemático para el proceso de enseñanza aprendizaje de la Matemática: Escuelas de nivel medio de población económica comprometida de la ciudad de Córdoba”, de Gustavo A. Chiodi y Aldo Chami, realizado en la Facultad de Ingeniería de la Universidad Católica de Córdoba, se pudo constatar a través de una investigación de campo las dificultades que presentaban los alumnos para realizar sus tareas extra-áulicas. Estas dificultades provenían en general de las siguientes categorías: a. alumnos que no tienen el suficiente grado de contención fuera del ámbito netamente escolar. b. alumnos que no pueden recurrir a un adulto en sus hogares para solicitarles ayuda en sus tareas escolares. c. alumnos que, estando acompañados por familiares, estos no pueden acompañar la actividad de las tareas que los alumnos deben entregar en clases siguientes. Una mirada actual y objetiva sobre esta realidad y en base a estos antecedentes permitió determinar que esta situación persiste en un gran número de familias social y económicamente comprometidas. Así la interacción efectiva entre los docentes, desde las propuestas de actividades curriculares por un lado, y los alumnos desde sus actividades extra-áulicas (deberes o tareas) por el otro, se ve afectada fuertemente. El presente proyecto, como plataforma educativa, inscripto en una realidad social compleja y de importancia vital para el desarrollo educativo de los alumnos intentará dar tratamiento a este problema ya no en forma particular para cada alumno sino en forma general y a varias disciplinas. El desafío de este proyecto multidisciplinario, en el que confluyen la Informática y la Educación, es desarrollar un espacio para que los alumnos de nivel primario y nivel medio puedan encontrar en él trayectorias formativas extra-áulicas mediadas por el conocimiento curricular y construyendo un lugar de encuentro e intercambio productivo, en este caso, en la red, en una aula virtual y en una experiencia extensionista mediada por la tecnología informática. La plataforma informática educativa permitirá al alumno poder recurrir a un acompañamiento virtual en la realización de sus tareas en el marco curricular del proceso educativo y abandonar el concepto de mero consumidor de tecnologías a utilizarlas para generar nuevas alternativas y vínculos, donde de un modo creativo pueda generar conocimiento

Libro tercero del Código Civil Argentino: transcripción paleográfica de los manuscritos del Dr. Vélez Sársfield

Los borradores manuscritos del Código Civil Argentino, redactados por el Dr. Dalmacio Vélez Sársfield, se conservan en la Biblioteca Mayor de la Universidad Nacional de Córdoba. Observados desde la óptica paleográfico-diplomática, se presentan como un material sumamente interesante, diferente a la visión histórica o la jurídica. El proyecto de investigación que presentamos es transcribir el Libro Tercero de los manuscritos, continuando el trabajo iniciado en dos etapas ya concluidas, las trascripciones de los Libros Primero y Segundo del Código Civil Argentino. Objetivo general: * Realizar la trascripción paleográfica de los manuscritos del Dr. Dalmacio Vélez Sarsfield correspondientes a los cuatro libros del Código Civil Argentino. Objetivos específicos: * Transcribir los borradores del libro III del Código Civil Argentino, ajustándose a las normas de Trascripción de Documentos Históricos aprobados en la Reunión Interamericana de Archivos, celebrada en Washington en 1961. * Continuar la publicación en etapas de los resultados del trabajo en revistas y medios científicos aprobados, para conocimiento de los especialistas.

Plataforma informática aplicada como ayuda al proceso de enseñanza-aprendizaje de la educación primaria y secundaria de la provincia de Córdoba: la integración de las nuevas tecnologías (ntics) para el proceso de enseñanza-aprendizaje en entornos virtuales y colaborativos como complemento a la enseñanza tradicional.

Desde la Facultad de Ingenierí­a de la Universidad Católica de Córdoba, se pudo constatar a través de una investigación de campo las dificultades que presentaban los alumnos de nivel primario y medio para realizar sus tareas extra-Áulicas. Estas dificultades provenían en general de las siguientes categorías: a. alumnos que no tienen el suficiente grado de contención fuera del Ámbito netamente escolar. b. alumnos que no pueden recurrir a un adulto en sus hogares para solicitarles ayuda en sus tareas escolares. c. alumnos que, estando acompañados por familiares, estos no pueden acompañar la actividad de las tareas que los alumnos deben entregar en clases siguientes. Actualmente, esta situación persiste en un gran número de familias económicamente comprometidas, impidiendo que se logre una interacción efectiva entre los docentes, desde las propuestas de actividades curriculares, y los alumnos desde sus actividades extra- Áulicas (deberes o tareas). El presente proyecto, como plataforma educativa, inscripto en una realidad social compleja y de importancia vital para el desarrollo educativo de los alumnos intentará dar tratamiento a este problema ya no en forma particular sino en forma general y a varias disciplinas. El desafío de este proyecto multidisciplinario, en el que confluyen la Informática y Educación, es desarrollar un espacio para que los alumnos de nivel primario y nivel medio puedan encontrar trayectorias formativas extra-Áulicas mediadas por el conocimiento curricular y construyendo un lugar de encuentro e intercambio productivo, en este caso, en la red, en una aula virtual y en una experiencia extensionista mediada por la tecnología informática.

Verificación Formal de Sistemas basada Formal Software Verification based on Automated Analysisen Análisis Automático.

Identificación y caracterización del problema. Uno de los problemas más importantes asociados con la construcción de software es la corrección del mismo. En busca de proveer garantías del correcto funcionamiento del software, han surgido una variedad de técnicas de desarrollo con sólidas bases matemáticas y lógicas conocidas como métodos formales. Debido a su naturaleza, la aplicación de métodos formales requiere gran experiencia y conocimientos, sobre todo en lo concerniente a matemáticas y lógica, por lo cual su aplicación resulta costosa en la práctica. Esto ha provocado que su principal aplicación se limite a sistemas críticos, es decir, sistemas cuyo mal funcionamiento puede causar daños de magnitud, aunque los beneficios que sus técnicas proveen son relevantes a todo tipo de software. Poder trasladar los beneficios de los métodos formales a contextos de desarrollo de software más amplios que los sistemas críticos tendría un alto impacto en la productividad en tales contextos. Hipótesis. Contar con herramientas de análisis automático es un elemento de gran importancia. Ejemplos de esto son varias herramientas potentes de análisis basadas en métodos formales, cuya aplicación apunta directamente a código fuente. En la amplia mayoría de estas herramientas, la brecha entre las nociones a las cuales están acostumbrados los desarrolladores y aquellas necesarias para la aplicación de estas herramientas de análisis formal sigue siendo demasiado amplia. Muchas herramientas utilizan lenguajes de aserciones que escapan a los conocimientos y las costumbres usuales de los desarrolladores. Además, en muchos casos la salida brindada por la herramienta de análisis requiere cierto manejo del método formal subyacente. Este problema puede aliviarse mediante la producción de herramientas adecuadas. Otro problema intrínseco a las técnicas automáticas de análisis es cómo se comportan las mismas a medida que el tamaño y complejidad de los elementos a analizar crece (escalabilidad). Esta limitación es ampliamente conocida y es considerada crítica en la aplicabilidad de métodos formales de análisis en la práctica. Una forma de atacar este problema es el aprovechamiento de información y características de dominios específicos de aplicación. Planteo de objetivos. Este proyecto apunta a la construcción de herramientas de análisis formal para contribuir a la calidad, en cuanto a su corrección funcional, de especificaciones, modelos o código, en el contexto del desarrollo de software. Más precisamente, se busca, por un lado, identificar ambientes específicos en los cuales ciertas técnicas de análisis automático, como el análisis basado en SMT o SAT solving, o el model checking, puedan llevarse a niveles de escalabilidad superiores a los conocidos para estas técnicas en ámbitos generales. Se intentará implementar las adaptaciones a las técnicas elegidas en herramientas que permitan su uso a desarrolladores familiarizados con el contexto de aplicación, pero no necesariamente conocedores de los métodos o técnicas subyacentes. Materiales y métodos a utilizar. Los materiales a emplear serán bibliografía relevante al área y equipamiento informático. Métodos. Se emplearán los métodos propios de la matemática discreta, la lógica y la ingeniería de software. Resultados esperados. Uno de los resultados esperados del proyecto es la individualización de ámbitos específicos de aplicación de métodos formales de análisis. Se espera que como resultado del desarrollo del proyecto surjan herramientas de análisis cuyo nivel de usabilidad sea adecuado para su aplicación por parte de desarrolladores sin formación específica en los métodos formales utilizados. Importancia del proyecto. El principal impacto de este proyecto será la contribución a la aplicación práctica de técnicas formales de análisis en diferentes etapas del desarrollo de software, con la finalidad de incrementar su calidad y confiabilidad. A crucial factor for software quality is correcteness. Traditionally, formal approaches to software development concentrate on functional correctness, and tackle this problem basically by being based on well defined notations founded on solid mathematical grounds. This makes formal methods better suited for analysis, due to their precise semantics, but they are usually more complex, and require familiarity and experience with the manipulation of mathematical definitions. So, their acceptance by software engineers is rather restricted, and formal methods applications have been confined to critical systems. Nevertheless, it is obvious that the advantages that formal methods provide apply to any kind of software system. It is accepted that appropriate software tool support for formal analysis is essential, if one seeks providing support for software development based on formal methods. Indeed, some of the relatively recent sucesses of formal methods are accompanied by good quality tools that automate powerful analysis mechanisms, and are even integrated in widely used development environments. Still, most of these tools either concentrate on code analysis, and in many cases are still far from being simple enough to be employed by software engineers without experience in formal methods. Another important problem for the adoption of tool support for formal methods is scalability. Automated software analysis is intrinsically complex, and thus techniques do not scale well in the general case. In this project, we will attempt to identify particular modelling, design, specification or coding activities in software development processes where to apply automated formal analysis techniques. By focusing in very specific application domains, we expect to find characteristics that might be exploited to increase the scalability of the corresponding analyses, compared to the general case.

Plantas nativas como fuente de biopesticidas: explorando distintas interacciones planta-organismo blanco dirigidas al control de plagas, malezas y microorganismos.

Continuando con nuestra búsqueda de biopesticidas de potencia relevante en plantas nativas, en este proyecto nos concentraremos en encontrar sustancias que controlen eficientemente hormigas cortadoras, moscas, cucarachas, mosquitos y malezas. En la primera parte del presente proyecto se determinará mediante aislamiento bioguiado, los principios activos de las plantas que en un trabajo anterior, mostraron mayor inhibición del forrajeo de la hormiga Acromyrmex lundi, Aristolochia argentina y Lantana grisebachii, como también de aquellas que inhibieron al hongo simbionte aislado del nido, A. argentina y Flourensia oolepis. Posteriromente se evaluará la efectividad de estos extractos y principios activos a campo contra A. lundi determinando dosis efectivas para inhibir el forrajeo y/o el desarrollo del hongo simbionte. Luego se extenderá los resultados a otras especies de hormigas cortadoras como A. crassispinus y A. striatus. En segundo lugar proponemos el desarrollo de una metodología para aumentar la efectividad de aceites esenciales (AE) y terpenos (T) contra distintas plagas domésticas aprovechando la interacción de componentes de aceites esenciales en la intoxicación del insecto. Hemos demostrado que Musca domestica al ser fumigada con T puros, por separado, oxida a la mayoría de ellos mediante citocromo P450. Sin embargo cuando es fumigada con AE (mezcla de T) detoxifica al T mayoritario preferentemente, mientras que los T minoritarios están en condiciones de intoxicar al insecto ya que no serían blanco del P450. En este proyecto determinaremos la DL50 de 10 T en moscas tratadas y sin tratar con un inhibidor de P450 (butóxido de piperonilo). Con estos datos podremos elegir mezclas de terpenos tales que uno de ellos sea blanco de P450 y otro/s intoxiquen al insecto. Nos proponemos verificar este mecanismo en M. domestica y luego extenderlo a otros insectos domésticos (cucarachas, mosquitos). Este estudio facilitará el desarrollo de bioinsecticidas mas eficientes para cada insecto disminuyendo sus costos y favoreciendo su aplicación futura. En la tercera parte de este proyecto proponemos aislar los principios activos fitotóxicos de Cortadeira rudiuscula y Ophryosporus charua, cuyos extractos inhibieron selectivamente la germinación de mono- y dicotiledóneas, respectivamente. También se determinará el tiempo de vida media en suelo, y la dosis efectiva a campo con el fin de evaluar a dichas especies como futuros herbicidas naturales selectivos.