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.

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.

Participación del tráfico y la distribución de proteínas en la polaridad y el desarrollo de procesos neuronales. Protein sorting and trafficking participation in neuronal processes polarity and development.

El estudio del tráfico intracelular en neuronas ha despertado gran interés en los últimos años, debido a que un gran número de enfermedades neurodegenerativas y neuropsiquiátricas parecen tener origen en en el transporte defectuoso de proteínas en estos tipos celulares. Mediante el uso de técnicas de biología celular y molecular, fuimos capaces de describir una de las vías que regula la fisión de las vesículas que llevan su cargo desde la última cisterna del Aparato de Golgi hacia la superficie celular en células epiteliales no polarizadas. Uno de los componentes clave de esa vía resultó ser la Proteina Kinasa D1 (PKD1), cuya actividad en el Aparato de Golgi es esencial para un normal transporte intracelular. Sorprendentemente, observamos que la PKD1 en neuronas con polaridad establecida no regula la fisión en el Golgi, pero si estaría involucrada en la selectividad y distribución (sorting) de vesículas cuyo cargo debe ser específicamente dirigido a las membranas dendríticas. El bloqueo de la actividad de la PKD1 no solamente cambia el destino final de estos cargos, que son enviados de esta forma a la membrana terminal del axón, sino que también es capaz de inducir defectos en el desarrollo y crecimiento de los procesos dendríticos a largo plazo. En este proyecto estudiaremos de que manera influye la perturbación del sorting, en ausencia de PKD1 activa y de otros componentes que la regulan, en la distribución de receptores de factores neurotróficos y de neurotransmisores glutamatérgicos, y cómo estos cambios en su distribución afectan el número, tamaño, y funcionalidad de los procesos neuronales (axones y dendritas). Estos resultados contribuirán a adquirir mayores conocimientos de los mecanismos dependientes del transporte y sorting de proteínas de membrana que participan en la regulación del crecimiento neuronal, los cuales a su vez aportarán información valiosa en la comprensión de un gran número de enfermedades neurológicas. The study of intracellular trafficking in neurons has arisen a great deal of interest in the last years, since a great number of neurodegenerative and neuropsychiatric disorders seem to be originated in abnormal protein transport in these type of cells. Using cell and molecular biology methodologies, we have been capable of describe one of the pathways that regulate the fission of vesicles that carry their cargo from the last Golgi Apparatus cisternae to the cell surface in non-polarized epithelial cells. One of the key components in this pathway is the Protein Kinase D1 (PKD1), whose activity in the Golgi Apparatus is essential for a normal intracelular transport. Surprisingly, we have observed that PKD1 does not regulate fission in neurons with established polarity, but it would be involved in vesicles' sorting at Golgi, particularly of those that carry specific dendritic cargo. Blocking PKD1 activity changes the final destination of these cargoes, which is now sent to the axons' terminal membranes, and also produces late dendritic development and growing defects. In this project we will study how sorting perturbation in absence of PKD1 and its regulators activities influences selectivity and distribution of neurotrophic and neurotransmitter receptors, and how these sorting changes affect number, size and functionality of neuronal processes (axons and dendrites). These results will help to acquire greater knowledge about transport and sorting mechanisms of neuronal growth regulatory membrane proteins. In addition, these studies will contribute with new valuable information necessary to understand numerous neurological diseases.

Fragmentos de bosque nativo como nodo para la restauración, conservación dinámica de la biodiversidad y educación para el desarrollo sostenible de la región centro.

El proyecto se asienta en la Estrategia Mundial para la Conservación de las Especies Vegetales (GSPC), asumido por el gobierno como un programa más dentro del Convenio de Diversidad Biológica (CDB); la cual incluye 5 objetivos y 16 metas para lograr la conservación vegetal hacia el 2020. En este contexto se propone trabajar en los objetivos II, IV y V referentes al % de conservación in-situ de flora nativa y al % de material disponible para restauración y recuperación. En la faz educativa re refiere a las acciones para promover la educación y la concienciación sobre la diversidad de las especies vegetales, su papel en los medios de vida sostenible y su importancia para el mantenimiento de la vida en la Tierra; así como el último objetivo apunta a incrementar la cantidad de personas dedicadas al estudio y conservación de la flora regional. En este contexto se realizará investigación, restauración, valorización y cuidado de fragmentos de bosque nativo, ubicados en el Campus universitarios, entendidos como nodos de conservación dinámica de la biodiversidad tanto como al intercambio y utilización de nuevos conocimientos, basados en la educación ambiental. Con respecto a los fragmentos se realizarán acciones tendientes a unificarlos para estabilizar el sistema. Se relevará la presencia de avifauna a fin de determinar la importancia de la preservación de estos relictos en el mantenimiento de la biodiversidad y se estudiará la expansión del bosque en el área de clausura. Por otra parte se relevará el efecto del fuego en una forestación de algarrobos de 7 años vecino a los fragmentos. Por último, el diálogo sobre la ciencia y la tecnología se plantea hoy como una necesidad ligada a los procesos de democratización, la ciencia no tiene sentido si no llega a los ciudadanos por lo que se realizarán visitas educativas destinadas a alumnos de nivel primario y medio. Por otra parte, el proyecto se basa en el trabajo de los educadores extraescolares, cuyo papel resulta esencial para vitalizar a unas sociedades necesitadas de permanente reflexión acerca de los objetivos que persiguen, la sustentabilidad de las estrategias que utilizan para conseguirlos, y la equidad en su reparto y utilización.