Prática de ensino supervisionado no 1.º e 2.º ciclo do ensino básico: a comunicação (em) matemática em contexto de sala de aula

Relatório de Estágio apresentado à Escola Superior de Educação de Lisboa para obtenção de grau de mestre em Ensino do 1.º e 2.º ciclo do Ensino Básico

O contributo da rotina Ler, contar e mostrar para o desenvolvimento de competências da leitura e de expressão oral

Relatório de estágio apresentado à Escola Superior de Educação de Lisboa para obtenção de grau de mestre em Ensino do 1º e 2º ciclo do Ensino Básico

A qualidade de vida dos profissionais de saúde mental

Os profissionais de saúde mental são o principal instrumento de intervenção nesta área considerada como prioridade de Saúde Pública e estão sujeitos a desgaste emocional e stress, que pode afetar negativamente a sua qualidade de vida. Com este estudo pretende-se avaliar a perceção do estado de saúde e da qualidade de vida relacionada com a saúde nos profissionais de saúde mental. Para responder ao objetivo traçado optou-se por realizar um estudo observacional analítico transversal, com abordagem quantitativa. Foi utilizado o SF36v2 como instrumento genérico de avaliação da Qualidade de Vida, que já se encontra validado para a população portuguesa, complementado por um questionário socioprofissional. A recolha de dados decorreu online, de 28 de Janeiro a 30 de Abril de 2013. A amostra foi constituída por 201 profissionais de saúde mental de Portugal Continental. Os profissionais de saúde mental que integraram a amostra revelaram pior perceção do estado de saúde e qualidade de vida, quando comparados com os valores de referência para a população portuguesa com nível de instrução alto. Em termos de domínios do instrumento, piores resultados foram encontrados para todos eles com exceção do domínio Saúde Mental. A avaliação da qualidade de vida dos profissionais de saúde mental possibilita a implementação alterações no funcionamento dos serviços de saúde mental, nomeadamente de programas de gestão de stress, de estratégias de coping e de competências de interação e comunicação entre os profissionais, podendo contribuir para uma melhoria na prestação dos cuidados de saúde aos utentes.

A high order model for piezoelectric rods: an asymptotic approach

Preprint submitted to International Journal of Solids and Structures. ISSN 0020-7683

Metáforas da crise cotidiana: os media e a veiculação da crise grega

A partir da forma como nos media portugueses são veiculadas as relações de oposição e negociação entre a Grécia e a União Europeia, pode verificar-se a importância e a força que a metáfora conceitual possui como mecanismo linguístico e cognitivo de construção de perceções, defesa de pontos de vista e fundamento de perspectivas ideológicas. Alicerçando-se numa estrutura metafórica de base, a negociação é colocada entre os domínios JOGO e LUTA, evidenciando-se o peso das metáforas como poderosos mecanismos para construir e manipular as perceções que temos sobre a realidade.

Relatório de estágio na Fundação Bracara Augusta - Loja Europa Jovem, com ênfase no caso de estudo sobre os impactos sócio económicos do Programa Juventude em Ação 2007-2013 no Município de Braga

Relatório de estágio de mestrado em Políticas Comunitárias e Cooperação Territorial

Modificaciones sitio dirigidas en la albúmina sérica humana para mejorar su afinidad en el transporte de medicamentos

La albúmina sérica humana es una proteína globular de importancia biológica. Se destacan su capacidad para mantener la presión oncótica del plasma y como transportadora de muchos compuestos, entre ellos fármacos. Muchos de estos fármacos, antimicóticos y oncológicos son altamente hidrofóbicos y son vehiculizados en medios acuosos formando complejos con la albúmina. Esta interacción ocurre por la presencia de tres dominios hidrofóbicos presentes en el interior de su estructura proteica. Esto permite deducir que la incorporación de drogas hidrofóbicas se encuentra limitado por el número de dominios hidrofóbicos. Este proyecto plantea como objetivo el desarrollo de nuevas variantes de albúmina, que presenten dominios hidrofóbicos más extendidos para mejorar su capacidad transportadora. Se procederá en primera instancia a realizar el clonado del cADN de la albúmina en un vector de expresión. Se realizarán modificaciones puntuales e inserciones de nucleótidos en el gen de la albúmina que permitan incrementar la cantidad de secuencias hidrofóbicas presentes. Se expresarán y purificarán las diferentes variantes de albúmina. De lograrse los objetivos, se caracterizarán las propiedades biológicas y fisico-químicas de estas variantes mediante análisis farmacológicos, inmunológicos y de biocompatibilidad. En una segunda etapa podremos analizar y evaluar la posibilidad de usar algunas de estas variantes como nuevos vehículos para el transporte de diversos fármacos.

Estudios de la Glicoproteina asociada al embarazo

El período de gestación en el humano está asociado con el aumento en la concentración sérica de un grupo de proteínas, consideradas en un principio como específicas del embarazo. Entre éstas, la glicoproteína asociada al embarazo es, cuantitativamente una de las más importantes. Aislada en 1959, ha sido identificada como una proteína inhibidora de proteasas que por su similitud estructural, físico-química y antigénica con Macroglobulina forma con ésta el par de a macroglobulinas análogo al encontrado en otras especies. (...) Recientemente se observó que la M es capaz de formar complejo con el t-PA, igualmente en nuestro laboratorio existen evidencias preliminares de la formación de complejos entre PAG-tPA. Es posible que este fenómeno constituya un mecanismo alternativo de control de procesos proteolíticos, aunque son necesarios estudios básicos y clínicos. (...) Por otra parte, no existen evidencias claras que puedan explicar las diferencias de unión entre el receptor y los complejos M y PAG-proteasas y en cuanto a que compartan el mismo receptor celular. Esto último está avalado por el hecho de que los dominios de reconocimiento del receptor de cada complejo es antigénicamente diferente. (...) Sin embargo, las evidencias son limitadas siendo necesarios estudios con purificada identificando las proteasas involucradas y los intermediarios de las vías de transducción. Objetivos Generales y Específicos: Se pretende conocer algún rol funcional de M mediante estudios de: a) La formación y caracterización de complejos con t-PA y otras serino proteasas; b) Purificación y caracterización de un receptor de PAG-proteinasa, en membranas celulares e identificación de señales de transducción por interacción de los complejos enzima-inhibidor con receptores de monocitos/macrófagos, y c) Su comportamiento como proteína de fase aguda en la pancreatitis aguda.

Estudio de las propiedades dinámicas de sistemas magnéticos con redes neuronales y otros sistemas complejos

En este proyecto continuaremos estudiando algunas propiedades dinámicas de diferentes sistemas complejos, con especial énfasis en vidrios de spin, redes neuronales y autómatas celulares aplicados a modelos de evolución biológica. En vidrios de spin estamos analizando la dependencia entre los diagramas dinámicos obtenidos utilizando la técnica de propagación de daños y aquellos obtenidos estudiando el decaimiento de la función de autocorrelación. Este estudio pretende contribuir a entender los mecanismos microscópicos responsables del surgimiento de "ageing", entendiendo por éste a la dependencia de algunas cantidades con la historia de la muestra. En redes neuronales seguiremos dos líneas: en primer lugar, introducir componentes más realistas desde el punto de vista biológico, a fin de entender los mecanismos fisiológicos de las diferentes funciones cerebrales. En segundo lugar, estamos interesados en utilizar el modelo de Hopfield para red neuronal como por ejemplo de sistema complejo controlable a partir del cual estamos tratando de entender cómo la estructura del espacio de fases influye en la dinámica del sistema. Finalmente, continuaremos trabajando con el modelo Bak-Sneppen para evolución biológica de especies interactuantes y el surgimiento de "ageing" en el estado auto crítico. Objetivos generales y específicos (...) 1. Estudio de la relación entre el fenómeno de "ageing" y la sensibilidad del proceso dinámico a las condiciones iniciales. (...) 2. Estudio del efecto de la formación de dominios en la dinámica de no-equilibrio de modelos de vidrios de spin y ferromagnéticos. (...) 3. Estudio de la influencia de la estructura del espacio de configuraciones en la dinámica de no-equilibrio. (...) 4. Inclusión de ingredientes biológicamente realistas. (...) 5. Auto criticalidad forzada por secuencias deterministas. (...)

Identificación de canales voltaje-activados de calcio cuya función es inhibida por la activación de receptores opioides tipo delta

Los canales de calcio proveen la vía más importante para el influjo de calcio al interior de las neuronas, ion que tiene importancia central en la liberación de neurotransmisor, regulación de la excitabilidad celular e inicio de un número importante de respuestas celulares. Y están además involucrados en diversas patologías cerebrales. Los agonistas opioides, por su parte, son reconocidos como importantes substancias que regulan la neurotransmisión y excitabilida neuronal, ya sean liberados como agentes hormonales endógenos o administrados exógenamente. La literatura y nuestros experimentos preliminares indican que es de esperar que los agonistas delta-opioides inhiban más de un tipo de canal de calcio. Determinar los tipos es de importancia porque distintos tipos de canales de calcio pueden estar involucrados en funciones celulares diferentes, ya sea en virtud de la particular forma de funcionar de cada uno de ellos o debido a su distribución localizada en distintos dominios subcelulares (dendritas, axones, soma). Además, el estudio de esta cuestión es central para entender el mecanismo celular y subcelular de acción de los neuromoduladores opioides. Con el Objetivo General de entender los mecanismos celulares básicos mediante los cuales los compuestos opioides afectan la excitabilidad de las células nerviosas y la transmisión sináptica, nos planteamos como Objetivo Específico la determinación de los tipos específicos de canales iónicos voltaje-dependientes de Ca2+, cuya función es inhibida por agonistas opioides selectivos para receptores opiáceos delta.

Perfil neuropsicológico y sesgos cognitivos de adolescentes con diferentes patrones de consumo de alcohol. Neuropsychological profile and cognitive bias in adolescents with different alcohol consumption patterns.

Identificación y caracterización del problema objeto de estudio: Diversas investigaciones señalan que el uso o consumo de alcohol comienza durante la adolescencia. En este periodo del desarrollo típicamente se han reportado deterioros asociados con el consumo de alcohol sobre diversas funciones cognitivas. Sin embargo, los hallazgos no siempre han sido concluyentes. Hipótesis: a) Existe una mayor cantidad de déficits neuropsicológicos (especialmente en los dominios asociados con la toma de decisiones) en los grupos de adolescentes que presentan patrones de consumo elevados o tipo binge y en los adolescentes bajo tratamiento; b) Existen sesgos cognitivos de tipo implícito en los adolescentes expuestos a publicidades referidas a bebidas alcohólicas; y c) Existe mayor presencia de expectativas negativas en el grupo conformado por niños, así como una mayor presencia de expectativas positivas en el grupo conformado por adolescentes. Planteo de Objetivos: se pretende lograr un perfil neuropsicológico de adolescentes de ambos sexos en función de patrones de consumo de alcohol bien diferenciados. Asimismo, se intentará determinar la presencia de sesgos cognitivos hacia estímulos asociados con el alcohol en función de las expectativas hacia el psicotrópico y el tipo de consumo del mismo que presenta la población bajo estudio. Finalmente, se buscará determinar si existen cambios evolutivos en las expectativas hacia el alcohol que pudieran indicar la presencia de mayor vulnerabilidad al consumo de alcohol. Materiales y métodos a utilizar: Se utilizarán pruebas neuropsicológicas (IGT, WCST, otras) y cognitivas (AEQ o similares). Se apelará al uso de diseños ex post facto prospectivos de tipo simple o factoriales, diseños factoriales, estudios instrumentales y estudios descriptivos de poblaciones mediante encuestas. Resultados esperados: 1) Se espera encontrar una mayor cantidad de déficits neuropsicológicos (especialmente en los dominios asociados con la toma de decisiones) en los grupos de adolescentes con patrones de consumo de alcohol elevados y binge, así como en el grupo de adolescentes bajo tratamiento. 2) Se espera encontrar la presencia de sesgos cognitivos implícitos en aquellos adolescentes expuestos a publicidades referidas a bebidas alcohólicas en contraposición a los adolescentes expuestos a publicidades de bebidas no-alcohólicas. 3) Se espera encontrar una mayor presencia de expectativas negativas en el grupo conformado por niños, y una mayor presencia de expectativas positivas en el grupo conformado por adolescentes, con lo que se verificaría el supuesto que señala que las EA se modifican a lo largo del desarrollo. Asimismo, se espera confirmar que las EA cambian en función de la experiencia de consumo de alcohol. Importancia del proyecto: En el ámbito local no se han realizado estudios sistemáticos de esta naturaleza, la información que se obtenga permitirá evaluar el impacto del uso y abuso de alcohol durante la adolescencia así como diseñar y ejecutar mejores estrategias de prevención y de rehabilitación y, al mismo tiempo, facilitará la toma de decisiones en el campo de la planificación de políticas sanitarias dirigidas a los adolescentes.

Regulación transcripcional y relación entre estructura y función de proteínas relacionadas con el metabolismo de colina en Pseudomonas aeruginosa. Transcriptional regulation and relationship between structure and function of proteins related with the choline metabolism in Pseudomonas aeruginosa.

El objetivo general de este proyecto es dilucidar los mecanismos de acción a nivel molecular de enzimas y proteínas involucradas en el metabolismo de colina en Pseudomonas aeruginosa, con énfasis en la identificación de residuos aminoacídicos críticos y regulación de la expresión de los genes en estudio. Los objetivos específicos que se palntean involucran abordajes bioquímicos y moleculares y serán llevados a cabo mediante técnicas de biología molecular y bioquímica (mutación sitio-dirigida, deleción génica, expresión y purificación de proteínas, fusión transcripcional a genes reporteros, etc). Planteo de hipótesis: las proteínas que se inducen por colina (fosforilcolina fosfatasa (PchP), fosfolipasa C (PlcH), acetilcolinestera (AchE), proteínas periplásmicas unidoras de colina (PUch) podrían compartir: a) una organización génica y responder a la regulación por proteínas regulatorias o a factores ambientales de manera similar; b) residuos aminoacídicos conservados que intervengan en la unión o interacción con diferentes ligandos, principalmente, colina. Para ello, se plantean los siguientes Objetivos Específicos: 1) identificar las zonas promotoras de los genes que codifican para PchP, PlcH, AchE y PUch, a fin de localizar posibles sitios de unión a proteínas reguladoras y los factores ambientales que afectan la actividad promotora. 2) determinar en las proteínas mencionadas los residuos aminoacídicos de importancia involucrados en la catálisis y en la interacción con ligandos, principalmente en la unión a compuestos de alquilamonio; 3) Se iniciarán estudios que demuestren la relación entre la inducción por colina de varios factores de patogenicidad la virulencia del microorganismo, empleando mutantes simples o múltiples en estos factores y como modelo de patogenicidad el nematodo C. elegans. A partir de los resultados obtenidos se pretende tener un conocimiento profundo sobre la regulación molecular y bioquímica de varias enzimas comprometidas en la patología que produce P. aeruginosa. Esto más el conocimiento de la fisiología de este microorganismo abre el camino para la búsqueda de posibles blancos de acción de drogas. Por otro lado, se espera tener un conocimiento integral sobre la regulación de la expresión de las actividades enzimáticas relacionadas con el metabolismo de colina y la respuesta de P. aeruginosa ante la presencia de compuestos de alquilamonio utilizados como nutrientes. Se espera conocer el papel que desempeña cada uno de los sitios de unión a los diferentes ligandos para el funcionamiento y control de las enzimas mencionadas y explicar el comportamiento diferencial de las enzimas frente a distintos sustratos y otros ligandos. El conocimiento de los sitios de unión a compuestos de alquilamonio permitirá encontrar esos dominios en diferentes proteínas del género Pseudomonas y otras bacterias Gram negativas. Desde el punto de vista evolutivo, se podrá comparar la similitud de los sitios de unión a colina entre proteínas de organismos eucariotas con procariotas (ej. PUch de bacterias Gram positivas, transportadores de colina, proteína C reactiva, AchE de eucariotas contra las encontradas en bacterias del género Pseudomonas, fosfolipasas A, C o D, etc.). Este proyecto permitirá concretar al menos dos tesis doctorales (Sanchez, Otero) más varios trabajos finales de grado (tesinas) que son y serán realizados por alumnos de la carrera de Microbiología en la UNRC. Les permitirá a los doctorandos y a los alumnos de grado adquirir una formación bastante integral ya que utilizarán herramientas de la fisiología general bacteriana, de la bioquímica clásica, de la biología molecular y de la bioinformática.

Supresión oral de la Encefalomielitis autoinmune experimental por antígenos sinaptosomales. Oral suppression of experimental autoimmune encephalomyelitis by sinaptosomal antigens.

La inducción de las manifestaciones clínicas de la encefalomielitis autoinmune experimental (EAE) involucra una reacción inmune celular contra determinantes antigénicos del sistema nervioso central (SNC), principalmente contra la proteína básica de mielina (PBM). Atento a la reactividad inmunológica cruzada previamente descrita entre la PBM y la proteína neuronal Sinapsina I, estudiaremos el efecto de la administración oral de moléculas híbridas (LTBSC, LTBSABC) entre la subunidad B de la toxina lábil al calor de Escherichia coli (LTB) con péptidos de Sinapsina (dominios C y ABC de la molécula) sobre el desarrollo de la EAE en ratas Wistar. Se administrarán oralmente los antígenos híbridos de LTB, LTB y péptidos de sinapsina no acoplados previa o posteriormente a la inducción activa de la EAE. Se estudiará la aparición de las manifestaciones clínicas de la enfermedad y se caracterizará la respuesta histopatológica e inmunológica (reacción de DTH, activación de linfocitos T, respuesta inmune humoral, vías de activación de macrófagos, patrón de citocinas) y los eventos celulares e inmunes desencadenados a nivel local luego de administrar los antígenos recombinantes en sistemas in vivo e in vitro. Estos estudios acerca de la respuesta autoinmune contra componentes de mielina y sinaptosomales en EAE tienen como objetivo poder comprender los diferentes mecanismos subyacentes involucrados en el desarrollo y regulación de esta enfermedad experimental. Específicamente este proyecto relacionado a la supresión de los síntomas clínicos como así también las alteraciones neuropatológicas del SNC de la EAE a través de un proceso de supresión oral de la enfermedad no invasivo utilizando tanto antígenos mielínicos como sinaptosomales fusionados a subunidades B (atóxicas) de la enterotoxina lábil al calor de E. coli (LTB), es de suma importancia para un estudio posterior en las patologías humanas relacionadas y su uso en el diagnóstico, pronóstico y/o terapia de las mismas.

ARN helicasas en dos procesos de desarrollo: variación antigénica y enquistamiento de giardia lamblia.

Además de su importancia médica y veterinaria al ser una de las mayores causas de enfermedad intestinal con origen en el consumo de agua, Giardia es un excelente modelo para estudiar la evolución de importantes procesos celulares, ya que es una de las células eucariotas más primitivas que se conocen. Giardia utiliza dos mecanismos de adaptación a los cambios ambientales que confronta durante su ciclo de vida, ya sea para sobrevivir dentro del intestino del huésped como es la variación de sus antígenos de superficie, o fuera del mismo como es la diferenciación a quiste o enquistamiento. El Objetivo General de nuestro proyecto de investigación es el de comprender los mecanismos de adaptación y diferenciación celular en Giardia lamblia y utilizar esos conocimientos para el desarrollo de metodologías que permitan evitar la enfermedad y/o la transmisión del parásito así como también para definir nuevas técnicas diagnósticas. Las ARN Helicasas están presentes en muchas Archaea, casi todas las Eubacterias y todos los organismos eucariotas, y son necesarias o están involucradas en muchos procesos diferentes del metabolismo del ARN. En células eucariotas se las ha asociado desde la transcripción hasta la degradación del ARN, incluyendo pre-ARNm splicing, exportación del ARNm, biogénesis del ribosoma, iniciación de la traducción y expresión génica en organelas. Resultados previos indican que el mecanismo por el cual Giardia regula la expresión de sus proteínas variables de superficie es a nivel post-transcripcional, utilizando un mecanismo similar a ARN de interferencia. La presencia de los complejos de doble hebra de ARN promueve la acción de ARN Helicasas y ARNasas III que cortan el dsRNA en fragmentos cortos de 21-23 nt. Sin dudas ésta es la primera evidencia de un mecanismo de este tipo que participa fisiológicamente en la regulación génica diferencial. Por otro lado, se ha descripto la interacción de helicasas con deacetilasas de histonas (HDAC), las cuales según estudios realizados en nuestro laboratorio estarían involucradas en la regulación epigenética de la variación antigénica y el enquistamiento. Se busca por lo tanto comprender la participación de ARN Helicasas en ambos procesos de adaptación del parásito, evaluando el grado e importancia de las mismas. En particular se focalizará en la localización subcelular, la interacción con otros componentes de la maquinaria regulatoria y determinación de los dominios involucrados, como también la relación entre sus niveles de expresión y los diferentes fenotipos asociados a estos procesos de adaptación del parásito.

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.