Herramientas para el relevamiento masivo de germoplasma de gramíneas forrajeras para tolerancia a la salinidad

La salinidad es una de las principales limitantes edáficas para la implantación de pasturas en el Chaco semiárido. En conjunto, la superficie salina del norte cordobés, de Santiago del Estero, Salta y el norte santafesino suma varios millones de hectáreas cuyo clima es apto para la producción de pasturas. Uno de los requisitos fundamentales para tal expansión es contar con especies forrajeras aptas para crecer bajo tales condiciones climáticas, pero en suelos afectados por salinidad. En los ambientes salinos con posibilidades ganaderas la especie forrajera Chloris gayana (Grama Rhodes) cv común ha mostrado la mejor adaptación, medida ésta como producción de materia seca y superficie ocupada en una cadena de alimentación. (...) Sin embargo no se ha explorado la variabilidad intracultivar para tolerancia a la salinidad, ni su asociación con la productividad. El objetivo general del trabajo es desarrollar herramientas para el relevamiento masivo de germoplasma de Chloris gayana para tolerancia a la salinidad, basadas en variables fisiológicas asociadas al funcionamiento del sistema antioxidante. Se propone validar el uso tecnológico de dos herramientas fisiológicas: contenido de clorofilas u malondialdehido para la distinción entre germoplasma con diversos grados de tolerancia a la salinidad. Asimismo, se estudiará la reacción ante la salinidad del sistema enzimático antioxidante (superóxido dismutasa y ascorbato peroxidasa) a fin de obtener información básica acerca de los mecanismos que median la respuesta a la salinidad en esta especie.

La responsabilidad civil del Estado: tendencias actuales y herramientas a fin de garantizar una reparación plena

En base a la selección y estudio de la legislación, doctrina y jurisprudencia locales y nacionales, se determinará el estado actual relativo a la responsabilidad civil del estado, a fin de establecer si en este contexto se brinda adecuada satisfacción al derecho constitucional a la reparación plena de los daños sufridos por los particulares. A esos efectos, se realizará un test de reparabilidad plena, resultante de verificar si en general las decisiones jurisdiccionales rechazan o tienden a rechazar demandas de daños contra el estado siendo que (1) serían admitidas en caso de que el causante del daño fuera un particular (no estatal); (2) de acuerdo a criterios doctrinarios (cualitativos), ese rechazo de demandas es contrario al principio de reparación plena. Se elaborará un informe final sobre el tema y, en caso de resultar que no se satisface plenamente el derecho a la reparación plena, se desarrollarán propuestas hermenéuticas (dirigidas a la doctrina y la jurisprudencia) y eventualmente proyectos de reforma legislativa, que tiendan a maximizar la satisfacción de ese derecho

Acciones tróficas de GABA: implicancias en la diferenciación sexual del cerebro. Trophic actions of GABA: Implications for sexual differentiation of the brain.

En el hipotálamo en desarrollo, el ácido gamma-amino butírico (GABA) produce depolarización neuronal, pudiendo incluso disparar potenciales de acción y causar la apertura de canales de calcio dependientes de voltaje. Esto se debe a que la concentración intracelular de Cl- es alta respecto al medio extracelular, por lo que en reposo el potencial de equilibrio de GABA es más positivo que el potencial de membrana. A medida que el desarrollo transcurre, la concentración intracelular de Cl- disminuye y se produce un cambio en la respuesta de depolarizante (etapa excitatoria) a hiperpolarizante (etapa inhibitoria). Se ha demostrado que este cambio ocurre también en neuronas hipotalámicas in vitro. El dimorfismo sexual del cerebro de los vertebrados es consecuencia de la acción del estrógeno aromatizado a partir de andrógenos segregados por el testículo durante el "periodo crítico" del desarrollo cerebral. Evidencias previas de nuestro y otros laboratorios pusieron de manifiesto diferencias en el crecimiento y diferenciación de neuronas que no podían atribuirse a la acción hormonal, ya que ocurren antes que se inicie el brusco aumento de la secreción gonadal, alrededor del día 18 de desarrollo embrionario en la rata (E18). Además de las diferencias morfológicas, encontramos diferencias sexuales en la forma que las neuronas hipotalámicas responden a muscimol, un agonista específico del receptor GABAA. A los 9 días in vitro (9 DIV) la respuesta a muscimol fue hiperpolarizante (etapa inhibitoria) y además fue de mayor amplitud, área y duración en machos respecto a hembras. Esto nos indica que las neuronas provenientes de embriones machos son intrínsecamente diferentes a las de embriones hembra aún antes de la acción organizadora de los esteroides sexuales. En base a estas evidencias nos propusimos continuar nuestros estudios sobre la participación de GABA en la determinación de diferencias sexuales en el cerebro antes de la acción organizadora de los esteroides gonadales. Para ello, en cultivos de neuronas hipotalámicas de E16 separados por sexos, estudiaremos:- la respuesta a muscimol de las neuronas, en la etapa excitatoria (2 DIV) de la acción de GABA.- las composición de subunidades de los receptores GABAA en la etapa excitatoria/inhibitoria de la acción de GABA.- la participación de los receptores GABAA sobre el crecimiento neurítico.- la activación de la vía de las MAP quinasas por muscimol.- la participación de los receptores GABAA sobre el crecimiento axonal inducido por estradiol in vitro.Toda la metodología propuesta es de uso habitual en nuestro laboratorio e involucra herramientas de la electrofisiología y la biología celular-molecular; como patch-clamp, cultivo de neuronas hipotalámicas, Western blot, RT-PCR, entre otras. Esperamos encontrar diferencias sexuales en la amplitud, área y duración de la respuesta de las neuronas hipotalámicas al muscimol a los 2 DIV, y que éstas se deban a una diferente composición de subunidades del receptor GABAA. En cuanto a la participación del receptor GABAA en la neuritogenesis, esperamos encontrar mayor longitud neurítica en neuronas macho como así también una activación sexualmente dimórfica de la vía de las MAP quinasas. Además esperamosque la acción de un antagonista del receptor GABAA interfiera con la axogénesis inducida por estradiol in vitro, característica que muestra diferencia sexual también a favor de los machos, lo que reforzaría nuestra hipótesis. La importancia y originalidad de este proyecto reside en la evaluación de la participación del sistema GABAérgico en la determinación de características que durante el desarrollo, podrían estar involucradas en la determinación de diferencias sexuales permanentes en el cerebro adulto independientemente de la acción de los esteroides sexuales. Hasta la fecha, no ha sido evaluada la influencia de los receptores GABAA en la diferenciación sexual del cerebro antes de la acción organizadora de los esteroides gonadales.

DENSIFICACION URBANA: POTENCIAL DE DESARROLLO DE AREAS VACANTES.PROPUESTA DE NUEVAS HERRAMIENTAS VALORATIVAS. Acercamientos alternativos al fenómeno del crecimiento. Estudio de casos. Relevamiento y registro gráfico-conceptual.

La ciudad compacta, se ha dispersado en fragmentos deshilvanando el tejido social en fracciones desconectadas del sentido más profundo de lo urbano. Una realidad plena de contradicciones acumula experiencias ajenas a los modelos teóricos de profesionales y de la gestión pública. Los conflictos de la ciudad superan la planificación, siendo la renta del suelo el único paradigma del desarrollo urbano. La presente Investigación pretende reflexionar acerca de las metodologías de trabajo y los instrumentos posibilitantes de una urbanidad sustentable abordando una crítica al actual paradigma de desarrollo urbano. Se pretende el relevamiento de los sectores conpotencial de cambio (fragmentos urbanos, espacios vacantes, áreas degradadas, etc.) transfiriéndolos a una base de datos digitalizada, que pueda convertirse en un instrumento disciplinar y académico Hipótesis Las posibilidades de revisión del modelo de crecimiento extensivo de baja densidad se producen con mayor intensidad en las áreas vacantes de la ciudad. El potencial de los grandes espacios vacantes de la ciudad es definido por la especulación e intereses de los emprendedores que actúan en el mercado. El Código Normativo es el instrumento que consolida este modelo operativo Objetivos �Promover el análisis y crítica de la ciudad y su territorio, a los efectos de posibilitar un proyecto disciplinar con una urbanidad sustentable. �Proponer herramientas de análisis que permita operar de manera eficiente sobre la dinámica de crecimiento. �Elaborar una base digital de datos como instrumento operativo, que favorezca a la comprensión de fenómenos complejos Materiales y métodos a utilizar 1. Recopilación de datos y estudios bibliográficos para definir el marco conceptual y elaboración de metodos de análisis de espacios vacantes. 2. Estudio y análisis de las normativas vigentes 3. Identificación de espacios vacantes de la ciudad de Córdoba, identificando problemas de fragmentación y dispersión urbana y social: técnicas de muestreo. 4. Relevamiento y registro de campo. 5. Experiencia proyectual en la carrera Resultados esperados -Caracterización de fragmentos urbanos de la ciudad de Córdoba -Registro en base de datos identificando fragmentos urbanos de la Ciudad de Córdoba -Elaboración gráficos conceptuales y modelización en 3D -Resultados de experiencia piloto Importancia del proyecto Considerando el crecimiento de la ciudad de Córdoba, la crisis de las infraestructuras a la degradación de los espacios urbanos, la falta de una planificación sustentable y la desactualización de las Normativas Vigentes, se hace necesario la reflexión en el ámbito académico Pertinencia Contar con documentación real y confiable es prioritaria para la gestión de la ciudad, posibilitando articular problemas y oportunidades. Desde el campo metodológico brinda la posibilidad de formar una base teórica suceptible de relacionar la crítica y el proyecto.

Efectos de Territorio y Estrategias Familiares de Reproducción Social. El caso del Barrio Las playas de la ciudad de Villa María - Córdoba. Effects of Land and family strategies of social reproduction. The case of the neighborhood ´Las Playas´ in the city of Villa María - Córdoba.

Nuestro proyecto plantea analizar los recursos materiales y simbólicos que ponen en juego las familias pobres, en el marco de su reproducción social, a fin de evaluar en qué medida sus estrategias contribuyen a superar o reproducir las condiciones de pobreza hipotetizando que las prácticas sociales de las agentes en situación de pobreza, incluyen limitaciones conformadas por la estructura patrimonial disponible, como potencialidades inscriptas en la trayectoria colectiva y el estado de los instrumentos de reproducción del barrio, considerado como parte del sistema de estrategias de reproducción de sus unidades domésticas. En ese sentido la comprensión de las estrategias materiales y simbólicas que ponen en juego las familias pobres, nos ofrecerá una comprensión acabada de la problemática en cuestión a los efectos de lograr una incidencia mayor a la hora de la implementación de políticas públicas destinadas a este grupo poblacional, y grupos poblacionales similares. La inteligibilidad de este escenario social, puede ser aprehendida fundamentalmente, desde las posibilidades abiertas por las herramientas de tipo cualitativas, sin embargo la metodología utilizada en este proyecto de investigación considera la triangulación de inter-metodológica como recurso fundamental a fin de dar cuenta tanto de la dimensión explicativa como comprensiva de los problemas sociales a estudiar. La muestra es teórica intencional, sus alcances se definen por criterio de saturación teórica. Unidades de recolección: unidades familiares en situación de pobreza que viven en el barrio Las Playas, instituciones formales y no formales que conforman los instrumentos de reproducción social. En el trabajo de campo se profundizarán las estrategias de: 1- Observación a partir de la construcción de guías para la mayor precisión de un registro de tipo etnográfico; 2- Entrevistas semi-estructuradas y abiertas a diferentes familias del barrio seleccionadas a partir de la técnica denominada "Bola de Nieve" la cual provee un alcance exhaustivo en el territorio determinado; 3- Entrevista a informantes clave relacionados con ONGs e Instituciones Estatales actuantes en el barrio, referentes barriales y sindicales, punteros políticos, etc. Los datos obtenidos en el trabajo de campo deben relevar información que garantice el registro de las diversas miradas de los participantes y controlar la diferenciación entre los datos originales y las propias interpretaciones (Mendizábal, 2006). por lo cual la triangulación inter-metodológica, posibilitará articular reflexivamente los resultados cuantitavos y cualitativos. Se prevé la transferencia de resultados a través de publicaciones individuales o colectivas sobre los resultados obtenidos así como la presentación preliminar de los mismos en congresos y conferencias. Asimismo, se organizarán seminarios con los sectores de la sociedad civil que se trabaje en los que se espera discutir los resultados obtenidos.

Herramientas de la investigación proyectual para el diseño del espacio público: inputs y outputs.

La investigación proyectual ha demostrado ser una valiosa forma de adquirir conocimientos a partir de la disciplina del diseño. Esta es una metodología derivada del método fenomenológico que busca primero acercarse al fenómeno para luego extraer conclusiones. Es decir, que la realidad con la que se encuentra el diseñador es un importantísimo componente del sistema. En el período previo (2008-2009), nos hemos dedicado a observar preferentemente la personalidad creativa del diseñador. Durante el período informado discutimos sobre cómo esta metodología incorpora los inputs del contexto de producción. ¿Cómo participan estos contenidos en las 3 fases fases detectadas en el período anterior: descriptiva, estructural y exponencial. La segunda preocupación con respecto a esta metodología es sobre lo que llamamos el output, es decir, cómo se comunica y como se transfieren los resultados. Intuimos aquí que difícilmente sea una transpolación de otras disciplinas científicas. ¿cómo se comunican los resultados? ¿cómo se aplican los resultados? ¿cómo se integran investigación y transferencia?

Auditoria basada en riesgos modelo integrado de cuantificación de riesgos de auditoria.

La contabilidad a través de los estados financieros, concebidos como instrumentos que proporcionan un resumen de la situación patrimonial de las organizaciones y de sus evoluciones económicas y financieras, cumple un trascendente rol en la sociedad que consiste en suministrar información a ser utilizada en los procesos decisorios de los principales agentes que intervienen en la economía (inversores, acreedores, empleados, sindicados, mercados de valores, clientes, proveedores, estado, etc.). La importancia que fueron adquiriendo los estados financieros, como satisfactores de las demandas informativas de los interesados en su contenido, produjo la imperiosa necesidad de contar con una seguridad razonable de que la información incorporada en los mismos se encuentre libre de errores u omisiones significativos, que pudieran distorsionar las decisiones a ser tomadas por sus usuarios. Fue de este modo que la auditoría de estados financieros, dentro de los servicios de que agregan credibilidad a la información, se erigió en el proceso destinado a tal fin. En este contexto, la auditoría de estados financieros se convirtió en el proceso estructurado, llevado a cabo por un auditor independiente, con vistas a arribar a una conclusión respecto a si la información contenida por los estados financieros, refleja razonablemente o no la situación patrimonial y la evolución económica y financiera de una organización por el período que abarcan, conforme a las disposiciones consagradas en ordenamiento contable utilizado como referencia. El riesgo de auditoría, concebido como la medida que refleja la posibilidad de que el auditor arribe a una conclusión equivocada respecto de la forma en que los estados contables reflejan la situación patrimonial y la evolución económica y financiera por el período que comprenden, adquiere una relevancia inusitada dentro del proceso de auditoría de estados financieros. Los principales ordenamientos en materia de auditoría de estados financieros proponen una metodología de cálculo del riesgo de auditoría en donde el mismo se concibe como el producto de los siguientes componentes: a) riesgo inherente (posibilidad de que la información contenida por los estados financieros contenga errores u omisiones significativas en si misma), b) riesgo de falta de control (posibilidad de que el sistema de control interno no prevenga, detecte o corrija errores u omisiones propios de la información contenida por los estados financieros en si misma), y c) riesgo de falta de detección (posibilidad de que información con errores u omisiones no siendo prevenida, detectada o corregida por el sistema de control interno tampoco sea advertida como consecuencia de la aplicación de los procedimientos de auditoría). Existió un primer enfoque en relación a forma de determinación del riesgo de auditoría que se caracterizó por: a) una concepción reducida de los posibles factores determinantes de los diferentes tipos de riesgos, b) una visión transaccional y desintegrada de la organización y de la información, y c) una valoración de los riesgos apoyada fuertemente en el criterio profesional del auditor. La referida orientación en relación a los aspectos metodológicos de determinación del riesgo de auditoría, denominada “enfoque tradicional”, fue identificada por académicos y profesionales, como la principal causa del fracaso de la auditoría de estados financieros en reconocidos escándalos financieros (casos: Enron, Worldcom, Parmalat, etc.) que trajeron aparejadas un conjunto de consecuencias sociales de profundo impacto (cuantiosas pérdidas económicas, descrédito de la auditoría como proceso que agrega credibilidad a la información contenida en los estados financieros, sanciones de naturaleza penal, civil y profesional a auditores e integrantes de organismos encargados de controlar la ejecución de auditorias, etc.) A los efectos de superar las deficiencias del enfoque tradicional, relacionado con la metodología de determinación del riesgo de auditoría, se desarrolló un nuevo enfoque, conocido como auditoría basada en riesgos, el cual se caracteriza por: a) una concepción amplia de los posibles factores que inciden sobre los componentes del riesgo de auditoría, b) una visión estratégica, sistémica e integrada de la organización y de la información generada por ella y c) la pretensión de la utilización de herramientas objetivas en la valoración de riesgos. La auditoría basada en riesgos ataca el corazón mismo de la auditoría de estados financieros que es el modelo de riesgos de auditoría, haciendo foco en los riesgos de negocio de las organizaciones. El presente proyecto de investigación tiene la pretensión de colaborar como un eslabón más en la instauración del enfoque de auditoría basada en riesgos, aportando un modelo integrado de cuantificación de riesgos que identifique el grado de influencia que cada uno de los factores determinantes del riesgo de negocio tiene respecto de cada uno de los componentes que definen al riesgo de auditoría.

Disposición final de residuos sólidos en el ejido municipal de la ciudad de Córdoba: una oportunidad para el desarrollo de herramientas de gestión ambiental municipal participativa.

Identificación y caracterización del problema objeto del estudio. La gestión ambiental es un proceso continuo y dinámico cuyo fin es la implementación de políticas ambientales. Es clave en un municipio la gestión de los residuos sólidos urbanos (RSU) ya que requiere que se consideren aspectos tales como su recolección, tratamiento, disposición final y la participación social. La insuficiencia de datos vinculados a su disposición final dificulta el diseño y establecimiento de planes y su seguimiento. Tampoco se considera prioritaria la incorporación de los vecinos en la construcción de estrategias de gestión lo que genera resistencia hacia las mismas. Hipótesis. La problemática de los RSU es una manifestación particular de la interacción entre el medio físico y los actores sociales que en él se asientan y desarrollan sus actividades. El estudio de conocimientos, percepciones y valoraciones sobre el ambiente es vital para conocer la implicación social en los temas ambientales. Objetivos. Desarrollar herramientas técnico-científicas que orienten la gestión ambiental participativa escala municipal. Como objetivos específicos: analizar la situación ambiental en el área afectada por la disposición final de residuos de la ciudad de Córdoba; valorar la perspectiva ambiental de los habitantes del sector en relación a los RSU; analizar y valorar las estrategias de gestión ambiental municipal asociadas a su disposición final; relacionar las estrategias ambientales aplicadas con las condiciones socio-ambientales identificadas. Materiales y Métodos. El área de estudio se localiza en el sector sur de la ciudad de Córdoba, donde se halla el actual enterramiento sanitario transitorio. Su caracterización socio-ambiental comprenderá: Análisis y Diagnóstico Ambiental. Se utilizará el esquema Presión-Estado-Respuesta para estructurar la aplicación de indicadores ambientales. Para la interpretación de la información ambiental y su expresión espacial se utilizará ArcGIS. Ésta se incorporará a un video documental que servirá como disparador de los grupos focales. Análisis de la Perspectiva Ambiental. Las fuentes secundarias permitirán contextualizar los procesos estudiados. Se consultarán censos nacionales y provinciales, y otros documentos e informes técnicos. La recolección de información primaria se realizará mediante grupos focales y entrevistas semi-estructuradas. Éstas se harán mediante la estratificación de los actores sociales según composición del ingreso, e identificando otros referentes que aporten a la comprensión del proceso. El número de entrevistas se determinará mediante la obtención del punto de saturación teórica. El instrumento para llevar adelante estas entrevistas será una Guía de Pautas. Resultados esperados. Se obtendrá un documento organizado en tres secciones. La primera presentará el diagnóstico, los indicadores y los instrumentos para la valoración ambiental de los vecinos. La segunda plasmará los resultados obtenidos a través de cartografía elaborada con los datos de campo relevados, el registro, sistematización y síntesis de los datos analizados. En la última sección se formularán propuestas desde el punto de vista de la gestión ambiental municipal participativa. Importancia del proyecto. La gestión de los RSU es de incumbencia municipal. Los avances en política ambiental generan la necesidad de identificar sitios para la localización de infraestructuras para su tratamiento y disposición final. Esta situación, sin un adecuado proceso de participación pública, puede desencadenar conflictos evitables, como el traslado del enterramiento sanitario de Bower a uno transitorio en el ejido de la ciudad de Córdoba. Allí se generó un proceso que evidenció los inconvenientes de la toma de decisiones sin participación ciudadana. En abril de 2011 éste se trasladará a una nueva localización, situación que se presenta como un caso de análisis válido de abordar detalladamente y ahondar en los procesos de gestión ambiental urbana.

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.