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.

Dinámica poblacional de Streptococcus mutans en niños de edad escolar de la provincia de Córdoba. Population dynamics of Streptococcus mutans in school age children in the province of Córdoba

La caries dental es una enfermedad infecciosa, crónica y trasmisible, que se caracteriza por la desmineralización de los tejidos duros del diente, producida por la acción de los ácidos resultantes de la actividad metabólica del biofilm desarrollado sobre los dientes. Si bien, la etiología de la caries sería polimicrobiana, los estreptococos del grupo mutans son señalados como los principales protagonistas en el inicio de la lesión cariosa. En la pared celular se destacan proteínas que participan en procesos de adhesión, agregación y co-agregación, además de polisacáridos que muestran distintas especificidades antigénicas, lo que permite distinguir cuatro serotipos: c, e, f y k. Es escasa la información de las características antigénicas de las cepas circulantes de estreptococos del grupo mutans y se desconoce la relación de las mismas con la actividad de caries. En este estudio nuestros objetivos son identificar y caracterizar fenotípica y genotípicamente las cepas de estreptococos del grupo mutans circulantes en la provincia de Córdoba. La población de estudio estará constituida por escolares, urbano–marginales de la capital y del interior de la provincia. Se determinarán los serotipos de las mismas a través de de amplificaciones por PCR de tipo multiplex y luego se secuenciarán 8 genes a través de la técnica de tipado multilocus, con el fin de realizar estudios de sistemática molecular, y de estimar la estructura genética de S. mutans. Una vez que se hayan caracterizado los patrones de diversidad y distribución geográfica de S. mutans del centro de Argentina, se intentará dilucidar cómo se relacionan la diversidad genética con la experiencia de caries de los niños del estudio. Se analizarán de forma conjunta nuestros resultados con los publicados por otros autores. De esta forma se logrará una mejor comprensión de los factores históricos y ecológicos que han moldeado su distribución y aportar conocimientos a la sistemática del grupo “mutans” en relación a otras bacterias del género Streptococcus. Dental caries is an infectious, chronic and transmissible disease, characterized by demineralization of the hard tissues of the teeth, produced by the action of acids resulting from the metabolic activity of biofilm developed on the teeth. Although the etiology of caries would be polymicrobial, the streptococci of the mutans group are identified as the major responsible in the initiation of the carious lesion. In the cell wall there are proteins involved in adhesion, aggregation and co-aggregation processes, as well as polysaccharides that present different antigenic specificities, which allow the distinction of four serotypes c, e, f and k. There is little information about the antigenic characteristics of the Streptococcus mutans strains and the relationship of those characteristics with the caries activity is unknown. In the present study our goals are to identify and characterize the phenotypic and genotypic strains of streptococci of the mutans group circulating in the province of Cordoba. The study population will consist of urban and rural scholar children from Cordoba city and from the interior of the province. In order to study the molecular systematic, and the genetic structure of S. mutans, different serotypes will be determined by multiplex PCR amplifications and eight genes will be sequenced by using the multilocus typing technique. Once the diversity and the geographical distribution patterns of S. mutans from the center of Argentina is characterized, we will attempt to clarify how the genetic diversity is related with the caries experience in the children of the study. Our results will be analyzed together with those published by other authors. This will achieve a better understanding of the historical and ecological factors that shaped the bacteria’s distribution and will contribute to the knowledge of the systematic of the mutans group in relation to other bacteria of the genus Streptococcus.

Problemáticas de la interacción discursiva en la enseñanza y el aprendizaje de las Ciencias Naturales. Aportes didácticos. Interaction discoursive issues in teaching and learning Natural Sciences. Didactic contributions

Las didácticas específicas de las ciencias naturales revelan diferentes problemáticas en su enseñanza y aprendizaje en los diferentes niveles del sistema educativo. En particular, en las clases de ciencias la interacción discursiva docente alumnos adquiere relevancia, ya que el proceso de comunicación del conocimiento es uno de los pilares didácticos, junto a la trasposición del mismo. Especificamente, en este proyecto nos abocamos a aquellas intervenciones de docentes y alumnos que se relacionan con la construcción del conocimiento biológico y químico. El proyecto se enmarca en una actual linea de trabajo que indaga sobre las dificultades en los abordajes del conocimiento científico en las aulas, las características del discurso entre docentes y alumnos, las habilidades y dificultades en la comprensión de los enunciados de problemas y las características de los textos que se utilizan en las clases. Se focaliza este estudio en casos que intentan dar respuesta a tres temáticas, agrupadas en un conjunto de situaciones de investigación relacionadas con la interacción discursiva docente-alumno, retomando el rol del docente al hablar, guiar o diseñar las situaciones de referencia para el aprendizaje de los alumnos. Los casos son: 1- En cuanto a las concepciones sobre diversidad biológica en estudiantes de escuela secundaria y en textos académicos, atendemos a cómo la escuela presenta los contenidos ecológicos como un conjunto de dogmas y conceptos estáticos. Además suelen simplificarse conceptualmente y presentarse poco actualizados. Es por ello que se planea estudiar las concepciones y actitudes de los alumnos de secundaria sobre la biodiversidad, cómo estas dificultan su comprensión y los textos usados en relación a la promoción de la transposición didáctica. 2- En relación a cómo se elabora el patrón temático del tema célula en clases de Biología, se analizarán las diferentes estrategias de significados y de desarrollo temático, que se emplean en la comunicación aulica. Se intentará establecer si hay cambios en el desarrollo temático a medida que se avanza en la escolaridad. Esto es porque se puede apreciar que muchos de los problemas de aprendizaje del alumnado se deben a un desconocimiento tanto del patrón temático como del patrón estructural de la ciencia, siendo preciso evocar los patrones temáticos que se quieren utilizar, para construir un conocimiento compartido. 3-Finalmente, en los enunciados de problemas de Química, se analizarán las dificultades de comprensión lectora de alumnos de Ingeniería. Los docentes frecuentemente atribuyen los problemas a deficiencias en la instrucción recibida, sin considerarse los conocimientos previos del alumno, los obstáculos conceptuales originados en el tema, las deficiencias en la habilidad lectora, el tipo textual predominante en la consigna, el formato en el que se escribió la consigna y los factores personales, etc., siendo que la comprensión del enunciado de una consigna de trabajo condiciona fuertemente la posibilidad de su resolución. Los tres casos utilizarán metodologías cualitaritas que incluyan análisis de contenido en discursos orales y escritos. Los datos se registrarán desde observación no participante, registro etnográfico y con grabaciones de audio. Se espera contribuir al conocimiento, realizando aportes a la formación docente en tanto las estrategias discursivas que se emplean en el aula, en forma oral y en la escrita, conocer concepciones que dificultan o favoren la construcción del conocimiento científico, entre otras. Los productos de estos estudios estarán integrados por nuevos desarrollos para la formación docente, publicaciones científicas de impacto nacional e internacional, presentaciones a congresos, materiales didácticos y divulgativos, dictado de seminarios y/o cursos, redacción de informes a las escuelas intervinientes.. The specific Natural Sciences didactics show different problems in teaching and learning along the school system. In particular, the discourse used to communicate knowledge in Science lessons becomes important. With this project we will focus on the teachers and students actions regarding the construction of biological and chemical knowledge. This project attempts to answer these issues and brings together a range of research situations related to teacher-student interaction, through discourse, taking up the role of the teacher to speak, to plan and to guide student learning. We will study the ideas and attitudes of high school students about biodiversity that make difficult its understanding and the textbooks used in relation to promotion of the didactic transposition. In addition, regarding how the thematic pattern in biology classes is costructed, it will be analyzed the different meaning and thematic development strategies that are used in communication. We will attempt to establish whether there are any changes in the thematic development throughout high school education. Finally, we will analyze the reading comprehension problems in engineering students. Teachers frequently attribute these issues to deficiencies in prior education, without considering the students background, the conceptual obstacles arising in the field, the format in which the prompt is written, personal factors, etc., keeping in mind that the outcome of an activity is strictly dependant con the prompt understanding. We expect to make contributions to the teacher education in both the discourse strategies used in the classroom, orally and in writing, to learn about the conceptions that hinder or favor the knowledge construction, among others. The products of this study will be national and international impact scientific publications, conference presentations, popular science publications, seminars courses and reports to the schools involeved.