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.

Terapéutica racional, mediante indicadores de eficacia antimicrobiana, de la mastitis caprina utilizando marbofloxacina y cefquinoma. Rational therapeutics, indicators of antimicrobial efficiency in the mastitis goats using marbofloxacine and cefquinome

La producción de leche de cabra es considerada en nuestro país, y en la provincia de Córdoba, una alternativa productiva para el desarrollo sustentable y socio – económico de la población. Por otra parte, existe una mayor demanda del mercado nacional e internacional de esta leche, por lo que los productores deben garantizar la seguridad y calidad de la misma de acuerdo a las normas vigentes. Es por ello que el control y tratamiento de las diferentes enfermedades es de vital importancia tanto para maximizar la producción del hato como para cumplir con los cánones de seguridad exigidos. En este contexto la mastitis caprina es una de las enfermedades que afecta la productividad del sector, y para controlarla una de las medidas a emplear es la terapéutica con antimicrobianos. Se trabajará en este proyecto con marbofloxacina y cefquinoma, estableciendo pautas racionales (eficaces y seguras) para su empleo en la afección a nivel regional. Los indicadores de eficacia estarán fijados de acuerdo a los parámetros integrados de farmacocinética (FC) y farmacodinamia (FD). Estos últimos (FD) serán calculados a través de la determinación concentraciones inhibitorias mínimas de cepas bacterianas aisladas de mastitis caprinas en Córdoba. Se establecerán los parámetros farmacocinéticos a dosis únicas y múltiples para la marbofloxacina (5 mg/kg IV, IM) y cefquinoma (2 mg/kg IV, IM e IMM) a partir de muestras de suero y leche de cabras Anglo Nubian (n = 6 por antimicrobiano; diseño cruzado en función de la ruta de administración). Se determinarán sus concentraciones en dichos fluidos, por cromatografía líquida de alta precisión. Los resultados FC/FD para ambos medicamentos se compararán con parámetros recomendados por expertos para cada tipo de antimicrobiano y se utilizarán como medida para recomendar una terapéutica racional, fundamental para optimizar la posología, garantizar la eficacia clínica, y reducir al mínimo la selección y propagación de cepas resistentes de agentes patógenos. The production of milk of goat is considered the province of Cordoba, a productive alternative for the sustainable development and partner - economically of the population. There is a major demand of the domestic and international market of this milk, for what the producers must guarantee the safety and quality of the same one of agreement to the in force procedure. It is for it that the control and treatment of the different diseases performs vital importance so much to maximize the production of the herd as to expire with the safety demanded. In this context the mastitis goat is one of the diseases that affect the productivity of the sector, and to control her one of the measures to using is the therapeutics with antimicrobial. One will be employed at this project with marbofloxacine and cefquinome, establishing rational guidelines (effective and sure) for his employment in the affection to regional level. The indicators of efficiency will be fixed in agreement to the integrated parameters of pharmacokinetics (PK) and pharmacodinamics (PD). The latter (PK) will be calculated across the determination inhibitory minimal concentrations of bacterial strains isolated of mastitis goat in Córdoba. The parameters will be established pharmacokinetics to the only and multiple doses for the marbofloxacine (5 mg/kg the IV, IM) and cefquinome (2 mg/kg the IVth, IM and IMM), From samples of whey and milk of goats Anglo Nubian (n = 6 for antimicrobial; design crossed depending on the route of administration). Its concentrations will decide in the above mentioned fluids, for liquid chromatography of high precision. The results PK/PD for both antimicrobial will be compared with parameters recommended by experts for every type of antimicrobial and will be in use as measure for recommending a rational, fundamental therapeutics for optimizing the dosage, for guaranteeing the clinical efficiency, and to reduce to the minimum the selection and spread of resistant of pathogenic agents.

Caracterización de moléculas de rizobacterias y de leguminosas con alto impacto productivo y tecnológico en la provincia de Córdoba. Characterization of rhizobacteria and legumes molecules with high production and technological impact in the province of Córdoba.

La provincia de Córdoba cuenta con alto desarrollo agrícola a base de cereales y leguminosas, como por ejemplo el maní. Pero este cultivo con los años ha trasladado su zona de siembra original y se ha extendido hacia otras áreas de mayor riesgo ambiental a raíz de la implantación de la soja. Diversas son las consecuencias de estas dos acciones y que se extienden desde lo agroecológico hasta lo científico-técnico. Este previo estado del arte y las referencias bibliográficas que apuntan a la necesitad de aumentar el valor agregado de los cultivos, nos ha llevado a formular una hipótesis de trabajo y es que las plantas de maní y soja así como las rizobacterias que se asocian con ellas, son productoras de diversas moléculas con potencial uso biológico en la productividad del cultivo y en aplicaciones tecnológicas, biológicas e industriales. Sumado a lo anterior y a las ideas gubernamentales de la necesidad de obtener conocimiento y capitalizarlo como riqueza, y la imperiosa urgencia de responder a demandas regionales, se presenta este proyecto cuyo objetivo general apunta a estudiar la producción de diversas moléculas de rizobacterias y leguminosas con el fin de mejorar la productividad de los cultivos y desarrollar nuevas aplicaciones tecnológicas en la provincia de Córdoba. Para cumplir dentro de los dos años de trabajo solicitados con lo expuesto anteriormente, la investigación será dividida en objetivos específicos y que consisten en investigar la producción de moléculas de raíces de maní y soja, analizar la respuesta microbiana a las rizodeposiciones de ambas leguminosas y evaluar el posible papel biológico y aplicación tecnológica de moléculas de ambos tipos de organismos. Nuestro grupo es de caracter multidisciplinar y ahondará en la diversidad molecular producida por raíces de maní y soja en direfentes días y la respuesta de las rizobacterias que se asocian ellas utilizando técnicas químicas (HPLC, GC, GC-masa) y herramientas microbiológicas y bioquímicas clásicas. Con fines de aplicación tecnológica se determinará la posible acción antioxidante de los extractos vegetales sobre sistemas modelos de ensayo así como la búsqueda de enzimas y hormonas microbianas aplicables en otros campos de la ciencia. De esta forma se pretende atender algunas demandas de diferentes sectores del centro sur de Córdoba y del país pero fundamentalmente posibilitar nuevas aplicaciones de las leguminosas y de las rizobacterias además de permitir la formación académicas de alumnos de grado y posgrado de la UNRC. The province of Cordoba has high agricultural development based on cereals and legumes such as peanuts. But the crop over the years has transferred his original planting area and has spread to other areas of greatest environmental risk following the introduction of soybeans. The previous state and regional art references that point to the necessity of increasing the value-added crops, has led us to formulate a working hypothesis is that the peanut and soybean plants and rhizobacteria associated with they are products of various biological molecules with potential use in crop productivity and biological technology and industrial applications. The general objective is aimed at studying the production of various molecules and legumes rhizobacteria to improve crop productivity and develop new technological applications in the Cordoba province. This form is intended to meet some demands of different sectors of the center south of Cordoba and the country but enabling new applications of legumes and rhizobacteria in addition to allowing the academic training of undergraduates and graduate of the UNRC.

Caracterización de las interacciones allium cepa - microorganismos beneficiosos y generación de estrategias de bajo impacto ambiental para el manejo sustentable de enfermedades de cebolla causadas por hongos de suelo.

La cebolla es una de las hortalizas más importantes a nivel mundial y uno de los principales rubros dentro de las exportaciones de hortalizas frescas de Argentina. Las pérdidas causadas por enfermedades por hongos de suelo constituyen una limitación en la productividad de este cultivo. El rol de las bacterias promotoras de crecimiento vegetal (Plant Growth Promoting Rhizobacteria, PGPR) en protección biológica contra patógenos ha sido ampliamente descripto en diferentes sistemas vegetales. En la última década, un particular interés ha sido enfocado a la comprensión y el estudio de los mecanismos de defensa de las plantas. Sin embargo, los procesos de bioprotección durante la interacción entre estos microorganismos benéficos y diversos patógenos aún son escasamente abordados a niveles moleculares y fisiológicos. Las vías de señalización en las plantas han sido propuestas como actores importantes en los mecanismos de control biológico de enfermedades. Numerosos estudios han demostrado la complejidad de los cambios transcripcionales que ocurren en una planta durante la colonización de raíces por PGPR, remarcando que un mejor conocimiento de los eventos moleculares desencadenados resultaría en una profunda comprensión del potencial bioprotector de estos microorganismos beneficiosos presentes en el suelo. Por otro lado, la creciente necesidad de disminuir el impacto ambiental que implica el uso masivo de productos químicos para el control de plagas en general (patógenos, artrópodos y malezas) en cultivos ha direccionado los esfuerzos hacia el desarrollo de estrategias capaces de minimizar el efecto nocivo que los compuestos químicos pueden tener sobre el ecosistema, contribuyendo de esta manera a la sustentabilidad de la agricultura. Es por lo expuesto que este proyecto nos planteamos el objetivo de general conocimientos útiles para desarrollar herramientas que permitan ejecutar estrategias de manejo de hongos de suelo patógenos para cultivos de cebolla, utilizando el biocontrol como medio de bajo impacto ambiental.

Evaluación de recursos forrajeros promisorios para áreas desfavorecidas.

En la región árida y semiárida del país, los pastizales naturales son la base de la alimentación animal en un 90 % y de ese porcentaje se estima que un 10 % se encuentra en buena condición y el resto muestra algún grado de deterioro. Esta situación de deterioro prevalece hoy en día en el 70% del territorio argentino. Una de las más graves preocupaciones acerca de la desertificación es el extenso daño causado al suelo. Estos suelos en todas estas regiones tienen un cierto grado de degradación, lo que los hace susceptibles a pérdidas por erosión eólica e hídrica. La mitigación de la degradación casi generalizada que presentan los recursos pastoriles en la zona árida y en menor medida en la zona semiárida argentina podría lograrse mediante la revegetación con especies herbáceas nativas y exóticas, así como la implantación de arbustos forrajeros exóticos. La utilización de nuevos recursos forrajeros evaluados y/o mejorados en los sistemas de producción de áreas desfavorecidas, permitirá mejorar e incrementar la productividad sustentable de las mismas. El presente proyecto plantea el objetivo general de generar conocimientos sobre adaptación, caracterización morfológica, productividad y calidad de germoplasma forrajero introducido en áreas ecológicamente desfavorecidas para incrementar la oferta forrajera, la producción y la estabilidad de los sistemas ganaderos. Se caracterizarán adecuadamente las especies en estudio (arbustos, subarbustos y herbáceas), de las familias Chenopodáceas y Fabáceas a través de la fenotipización de caracteres específicos de las especies promisorias. Se evaluará la persistencia, el crecimiento, la producción y la calidad de las accesiones adaptadas a las diversas condiciones ambientales (tres sitios de estudio). Además, el proyecto se vinculará con las redes de evaluación de gramíneas megatérmicas (INTA) con metodología estandarizada, estableciendo nexos entre proyectos similares con la institución relacionada y evaluará la calidad de genotipos mejorados de gramíneas megatérmicas con la institución relacionada (INTA). Este proyecto generará conocimientos que permitirán incrementar la oferta forrajera, la producción y la estabilidad de los sistemas ganaderos de dichas áreas. Esto permitirá paliar las necesidades de los productores de las áreas desfavorecidas y por ende su calidad de vida.

Evaluación de recursos forrajeros promisorios para áreas desfavorecidas.

En la región árida y semiárida del país, los pastizales naturales son la base de la alimentación animal en un 90 % y de ese porcentaje se estima que un 10 % se encuentra en buena condición y el resto muestra algún grado de deterioro. Esta situación de deterioro prevalece hoy en día en el 70% del territorio argentino. Una de las más graves preocupaciones acerca de la desertificación es el extenso daño causado al suelo. Estos suelos en todas estas regiones tienen un cierto grado de degradación, lo que los hace susceptibles a pérdidas por erosión eólica e hídrica. La mitigación de la degradación casi generalizada que presentan los recursos pastoriles en la zona árida y en menor medida en la zona semiárida argentina podría lograrse mediante la revegetación con especies herbáceas nativas y exóticas, así como la implantación de arbustos forrajeros exóticos. La utilización de nuevos recursos forrajeros evaluados y/o mejorados en los sistemas de producción de áreas desfavorecidas, permitirá mejorar e incrementar la productividad sustentable de las mismas. El presente proyecto plantea el objetivo general de generar conocimientos sobre adaptación, caracterización morfológica, productividad y calidad de germoplasma forrajero introducido en áreas ecológicamente desfavorecidas para incrementar la oferta forrajera, la producción y la estabilidad de los sistemas ganaderos. Se caracterizarán adecuadamente las especies en estudio (arbustos, subarbustos y herbáceas), de las familias Chenopodáceas y Fabáceas a través de la fenotipización de caracteres específicos de las especies promisorias. Se evaluará la persistencia, el crecimiento, la producción y la calidad de las accesiones adaptadas a las diversas condiciones ambientales (tres sitios de estudio). Además, el proyecto se vinculará con las redes de evaluación de gramíneas megatérmicas (INTA) con metodología estandarizada, estableciendo nexos entre proyectos similares con la institución relacionada y evaluará la calidad de genotipos mejorados de gramíneas megatérmicas con la institución relacionada (INTA). Este proyecto generará conocimientos que permitirán incrementar la oferta forrajera, la producción y la estabilidad de los sistemas ganaderos de dichas áreas. Esto permitirá paliar las necesidades de los productores de las áreas desfavorecidas y por ende su calidad de vida.