Object-oriented inheritance of statecharts for control applications

This paper discusses how object-oriented iuheritance can be re-interpreted if statecharts are used for modelling the dynamic behaviour of an object. The support of inheritance of statecharts allows the improvement of systems' development by easing the reutilization of parts of already developed euccessful systems, aad by promoting the iterative and continuous models' refinement advocated by the operatioaal approach. Statechart is the formalism used within UML to specify reactive state.based behaviours. This paper covers the use of statecharts within the modelling of embedded systems for industrial control applxications, where performance and memory usage are main concerns.

Development of composite auxetic structures for civil engineering applications

Tese de Doutoramento em Engenharia Têxtil

Acabamentos funcionais têxteis aplicados por estamparia digital em substratos têxteis ativados por plasma

Tese de Doutoramento em Engenharia Têxtil

Surgical treatment of partial atrioventricular septal defect: functional analysis of the mitral valve in the postoperative period

OBJECTIVE: To study mitral valve function in the postoperative period after correction of the partial form of atrioventricular septal defect. METHODS: Fifty patients underwent surgical correction of the partial form of atrioventricular septal defect. Their mean age was 11.8 years and 62% of the patients were males. Preoperative echocardiography showed moderate and severe mitral insufficiency in 44% of the patients. The mitral valve cleft was sutured in 45 (90%) patients (group II - GII). Echocardiographies were performed in the early postoperative period, and 6 and 12 months after hospital discharge. RESULTS: The patients who had some type of arrhythmia in the postoperative period had ostium primum atrial septal defect of a larger size (2.74 x 2.08 cm). All 5 patients in group I (GI), who did not undergo closure of the cleft, had a competent mitral valve or mild mitral insufficiency in the preoperative period. One of these patients began to have moderate mitral insufficiency in the postoperative period. On the other hand, in GII, 88.8% and 82.2% of the patients had competent mitral valve or mild mitral insufficiency in the early and late postoperative periods, respectively. CONCLUSION: The mitral valve cleft was repaired in 90% of cases. Echocardiography revealed competent mitral valve or mild mitral insufficiency in 88.8% and 82.2% of GII patients in the early and late postoperative periods, respectively.

New auxiliary indicators for the differential diagnosis of functional cardiorespiratory limitation in patients with chronic obstructive pulmonary disease and congestive heart failure

OBJECTIVE: To differentiate the nature of functional cardiorespiratory limitations during exercise in individuals with chronic obstructive pulmonary disease (COPD) or congestive heart failure (CHF) and to determine indicators that may help their classifications. METHODS: The study comprised 40 patients: 23 with COPD and 17 with CHF. All individuals underwent maximal cardiopulmonary exercise testing on a treadmill. RESULTS: The values of peak gas exchange ratio (R peak), peak carbon dioxide production (VCO2 peak), and peak oxygen ventilatory equivalent (V E O2 peak) were higher in the patients with CHF than in those with COPD, and, therefore, those were the variables that characterized the differences between the groups. For group classification, the differentiating functions with the R peak, VCO2 peak (L/min), and V E O2 peak variables were used as follows: group COPD: - 44.886 + 78.832 x R peak + 5.442 x VCO2 peak + 0.336 x V E O2 peak; group CHF: - 69.251 + 89.740 x R peak + 8.461 x VCO2 peak + 0.574 x V E O2 peak. The differentiating function, whose result is greater, correctly classifies the patient's group as 90%. CONCLUSION: The R peak, VCO2 peak, and V E O2 peak values may be used to identify the cause of the functional cardiorespiratory limitations in patients with COPD and CHF.

Development of a subject-specific musculoskeletal shoulder model : inverse and forward dynamics applications

A prevalência de pessoas que referem dor no complexo articular do ombro, com concomitante limitação na capacidade para realizar atividades da vida diária, é elevada. Estes níveis de prevalência sobrecarregam quer os utentes, como a própria sociedade. A evidência científica atual indicia a existência de uma relação entre as alterações da articulação escápulo-torácica e as patologias associadas à articulação gleno-umeral. A capacidade de quantificar, cinemática e cineticamente, as disfunções ao nível das articulações escápulo-torácica e gleno-umeral, é algo de enorme importância, quer para a comunidade biomecânica, como para a clínica. No decorrer dos trabalhos desta tese foi desenvolvido, através do software OpenSim, um modelo tridimensional músculo-esquelético do complexo articular do ombro que inclui a representação do tórax/coluna, clavícula, omoplata, úmero, rádio, cúbito e articulações que permitem os movimentos relativos desses segmentos, assim como, 16 músculos e 4 ligamentos. Com um total de 11 graus de liberdade, incluindo um novo modelo articular escápulo-torácico, os resultados demonstram que este é capaz de reconstruir de forma precisa e rápida os movimentos escápulo-torácicos e glenoumerais, recorrendo para tal, à cinemática inversa, e à dinâmica inversa e direta. Conta ainda com um método de transformação inovador para determinar, com base nas especificidades dos sujeitos, os locais de inserção muscular. As principais motivações subjacentes ao desenvolvimento desta tese foram contribuir para o aprofundar do atual conhecimento sobre as disfunções do complexo articular do ombro e, simultaneamente, proporcionar à comunidade clínica uma ferramenta biomecânica de livre acesso com o intuito de melhor suportar as decisões clínicas e dessa forma concorrer para uma prática mais efetiva.

Desarrollo de interfases con transferencia controlada de especies moviles. Síntesis, caracterizacion y aplicaciones. Development of Interphases with Controlled Transference of Mobile Species. Synthesis, Characterization and Applications.

Se propone sintetizar nuevos materiales como bloques de construcción de estructuras en escala nanometrica o micrométrica: nanotubos de carbono funcionalizados; nanopartículas metálicas; hidrogeles inteligentes; carbones mesoporosos. Con ellos se construiran interfaces solido/liquido estructuradas: multicapas autoensambladas, patrones micrométricos con heterogeneidad tridimensional y estructuras jerárquicas. Se estudiara el intercambio de especies móviles en las interfaces usando técnicas electroquímicas, espectroelectroquimicas, ópticas y de microscopia. De esta manera se podran controlar el intercambio en esa interface. En base a este conocimientos se desarrollaran aplicaciones tecnológicas tales como sensores de oligonucletidos, microceldas de combustible, arreglos de microelectrodos y supercapacitores.

Diseño y desarrollo de superficies modificadas. Aplicaciones ambientales, biomédicas y farmacéuticas. Design and development of modified surfaces. Environmental, biomedical and pharmaceutical applications.

El objetivo general de este proyecto de investigación es diseñar, desarrollar y optimizar superficies con propiedades especificas para ser utilizadas como sensores y biosensores, materiales biocompatibles, columnas para separaciones por electroforesis capilar, matrices para la liberación controlada de fármacos y sorbentes para remediación ambiental. Para concretar este objetivo, se propone específicamente modificar superficies o particulas apuntando a optimizar un sistema concreto relevante en aplicaciones farmaceuticas, ambientales o biomedicas: 1. Modificacion de arcillas naturales o sinteticas para desarrollar matrices portadoras de farmacos o sorbentes para remediacion ambiental:1.1 Estudiar ilitas modificadas con Fe(III) para maximizar las propiedades adsortivas frente a aniones contaminantes como arsenico. 1.2 Sintetizar LDH de Al y Mg modificados con compuestos de interés farmacéutico para diseñar sistemas de liberación controlada.2. Modificación de canales de chips y electrodos para optimizar la separación, detección y cuantificación de compuestos farmacéutico: 2.1 Diseñar y construir microchips para la separación por EC de compuestos de base fenólica.2.2 Evaluar polímeros que mejoren la respuesta y/o estabilidad de electrodos de Carbono para ser usados como detectores amperométrico de compuestos de base fenólica en sistemas FIA y miniaturizados de análisis integrados.3. Modificación de superficies sólidas con biomoléculas para el desarrollo y optimización de superficies de bio-reconocimiento:3.1 Evaluar el comportamiento de superficies de titanio modificadas con TiO2 y depósitos inorgánicos frente a la interacción con proteínas plasmáticas (PP) para el análisis de la biocompatibilidad superficial.3.2 Diseñar y desarrollar superficies biofuncionales para el reconocimiento especifico de D-aminoácidos, anticuerpos en pacientes chagásicos y simple hebra de ADN. Las técnicas que se emplearán para llevar a cabo el proyecto dependen del tipo de sistema de estudio. En particular los estudios correspondientes al objetivo 1 se realizarán mediante análisis químicos, térmico, DXR, SEM, IR, BET así como mediante titulaciones ácido-base potenciométricas, movilidades electroforéticas, cinética e isotermas de adsorción.En general para desarrollar el objetivo 2 se utilizarán técnicas electroquímicas clásicas para la caracterización de los electrodos, los que luego se utilizarán como detectores en un sistema FIA amperométrico, mientras que los microchips se emplearán en electroforesis capilar para la separación de diferentes compuestos de interés farmacéutico.Finalmente, el objetivo 3 se llevará a cabo por un lado modificando electrodos de titanio con distintos depósitos (electroquímicas, sol-gel, térmicas) de TiO2 e hidroxiapatita y evaluando la interacción con proteínas plasmáticas para analizar la biocompatibilidad de los materiales preparados. Por otro lado, se estudiará el proceso de adsorción-desorción de D-aminoácido oxidasa, antígenos del T. Cruzi y ADN de simple hebra para optmizar la capacidad de bio-reconocimiento superficial de D-aminoácidos, anticuerpos de chagásicos y de cadena complementaria de ADN. Para concretar este objetivo se utilizarán técnicas electroquímicas, espectroscópicas y microscopias.Debido al carácter multidisciplinario del presente proyecto de investigación, su ejecución se llevara a cabo a través de la colaboración de investigadores pertenecientes a distintas áreas de la Química y permitirá continuar con la formación de recursos humanos mediante la realización de tesis doctorales y estadías postdoctorales.

Desarrollo de fotosensibilizadores con aplicaciones en la inactivación fotodinámica de microorganismos. Development of photosensitizer with applications in the photodynamic inactivation of microorganisms.

El plan propone desarrollar nuevas agentes fotosensibilizadores derivados de macrociclos pirrólicos con aplicaciones en la inactivación fotodinámica (PDI) de microorganismos. La propuesta abarca el desarrollo de procedimientos apropiados para la síntesis de compuestos derivados de porfirinas, subftalocianinas y ftalocianinas sustituidas en la periferia por grupos que permitan aumentar la actividad biológica. Con la finalidad de incrementar la incorporación intracelular y la actividad fotodinámica se evaluarán sensibilizadores con distinta distribución y número de cargas, en los cuales se ha incrementado el carácter anfifílico por la presencia de grupos lipofílicos y catiónicos. La combinación de un fotosensibilizador con un compuesto antifúngico está diseñada para aumentar la eficiencia en la inactivación de hongos. También serán evaluadas superficies antimicrobianas recubiertas con una película de fotosensibilizadores. En primera instancia, la actividad fotodinámica de los nuevos agentes fototerapéuticos serán evaluados en sistemas biomiméticos conteniendo sustratos biológicamente activos. Los estudios in vitro serán realizados en cultivos de bacterias y levaduras. Esta aplicación presenta considerable importancia en la inactivación de microorganismos patógenos que crecen in vivo en un foco localizado de infección, en la desinfección de fluidos biológicos y aguas contaminadas con microbios resistentes.

Desarrollo de Algoritmos Numéricos para el Estudio de la Propagación no Lineal de Ondas en Aplicaciones Aeroespaciales y Astrofísicas. Develop to Numerical Algorithms to Study non-Linear Waves Propagation in Aerospace and Astrophysics Applications.

En este proyecto se desarrollarán algoritmos numéricos para sistemas no lineales hiperbólicos-parabólicos de ecuaciones diferenciales en derivadas parciales. Dichos sistemas tienen aplicación en propagación de ondas en ámbitos aeroespaciales y astrofísicos.Objetivos generales: 1)Desarrollo y mejora de algoritmos numéricos con la finalidad de incrementar la calidad en la simulación de propagación e interacción de ondas gasdinámicas y magnetogasdinámicas no lineales. 2)Desarrollo de códigos computacionales con la finalidad de simular flujos gasdinámicos de elevada entalpía incluyendo cambios químicos, efectos dispersivos y difusivos.3)Desarrollo de códigos computacionales con la finalidad de simular flujos magnetogasdinámicos ideales y reales.4)Aplicación de los nuevos algoritmos y códigos computacionales a la solución del flujo aerotermodinámico alrededor de cuerpos que ingresan en la atmósfera terrestre. 5)Aplicación de los nuevos algoritmos y códigos computacionales a la simulación del comportamiento dinámico no lineal de arcos magnéticos en la corona solar. 6)Desarrollo de nuevos modelos para describir el comportamiento no lineal de arcos magnéticos en la corona solar.Este proyecto presenta como objetivo principal la introducción de mejoras en algoritmos numéricos para simular la propagación e interacción de ondas no lineales en dos medios gaseosos: aquellos que no poseen carga eléctrica libre (flujos gasdinámicos) y aquellos que tienen carga eléctrica libre (flujos magnetogasdinámicos). Al mismo tiempo se desarrollarán códigos computacionales que implementen las mejoras de las técnicas numéricas.Los algoritmos numéricos se aplicarán con la finalidad de incrementar el conocimiento en tópicos de interés en la ingeniería aeroespacial como es el cálculo del flujo de calor y fuerzas aerotermodinámicas que soportan objetos que ingresan a la atmósfera terrestre y en temas de astrofísica como la propagación e interacción de ondas, tanto para la transferencia de energía como para la generación de inestabilidades en arcos magnéticos de la corona solar. Estos dos temas poseen en común las técnicas y algoritmos numéricos con los que serán tratados. Las ecuaciones gasdinámicas y magnetogasdinámicas ideales conforman sistemas hiperbólicos de ecuaciones diferenciales y pueden ser solucionados utilizando "Riemann solvers" junto con el método de volúmenes finitos (Toro 1999; Udrea 1999; LeVeque 1992 y 2005). La inclusión de efectos difusivos genera que los sistemas de ecuaciones resulten hiperbólicos-parabólicos. La contribución parabólica puede ser considerada como términos fuentes y tratada adicionalmente tanto en forma explícita como implícita (Udrea 1999; LeVeque 2005).Para analizar el flujo alrededor de cuerpos que ingresan en la atmósfera se utilizarán las ecuaciones de Navier-Stokes químicamente activas, mientras la temperatura no supere los 6000K. Para mayores temperaturas es necesario considerar efectos de ionización (Anderson, 1989). Tanto los efectos difusivos como los cambios químicos serán considerados como términos fuentes en las ecuaciones de Euler. Para tratar la propagación de ondas, transferencia de energía e inestabilidades en arcos magnéticos de la corona solar se utilizarán las ecuaciones de la magnetogasdinámica ideal y real. En este caso será también conveniente implementar términos fuente para el tratamiento de fenómenos de transporte como el flujo de calor y el de radiación. Los códigos utilizarán la técnica de volúmenes finitos, junto con esquemas "Total Variation Disminishing - TVD" sobre mallas estructuradas y no estructuradas.

Estudios de sistemas organizados con aplicaciones en nanoquímica, síntesis orgánica y en reactividad. Studies of organized systems with applications in nanochemistry, organic synthesis and reactivity.

El objetivo general de este proyecto es el estudio de distintos tipos de sistemas organizados, conocer los factores que determinan la forma de organización y las consecuencias que ésta tiene sobre la reactividad de moléculas que se encuentran en ese entorno organizado. Se pretende realizar, desde la fisicoquímica y la síntesis orgánica, aportes a áreas multidisciplinarias como la nanociencia y la nanotecnología. Se sintetizarán ciclodextrinas anfifílicas y se estudiará su comportamiento en solución y en interfases, sus propiedades de agregación y morfología. Se estudiará también la termodinámica de los procesos y la capacidad catalítica de estas ciclodextrinas anfifílicas en superficies bidimensionales en reacciones de hidrólisis de ésteres. Las ciclodextrinas anfifílicas sintetizadas en el laboratorio se utilizarán también en mezclas con otros surfactantes, con el objetivo de generar medios eficientes respecto a la solubilización y extracción de contaminantes orgánicos desde suelos. Se espera encontrar sistemas que presenten efectos sinérgicos. Se determinará el efecto de la formación de complejos con ciclodextrina sobre las propiedades fisicoquímicas y la reactividad de pesticidas de amplio uso en agricultura, en particular de compuestos organofosforados. Se investigarán ciclodextrinas que permitan controlar la liberación del agroquímico y se realizarán estudios de la reactividad de los pesticidas en solución y en medios que simulen el suelo determinando si la inclusión en las ciclodextrinas modifica la velocidad de descomposición. En la búsqueda de nuevos sistemas microheterogéneos se sintetizarán surfactantes gémini con una cadena hidrocarbonada y una perfluorada y se determinarán sus propiedades. Luego de su caracterización, estos surfactantes se aplicarán en estudios de reactividad de compuestos insolubles en agua.Se estudiará la formación de complejos de ciclodextrina con metales de transición y los mismos se utilizarán como catalizadores en reacciones de oxidación de sulfuros y de alquenos en medios acuosos y no acuosos buscando condiciones donde se logre inducción quiral. Se sintetizarán compuestos azufrados polifuncionales con los cuales se modificarán superficies de nanopartículas por quimioadsorción de los mismos. Dado que se pretende obtener compuestos con propiedades específicas que dependen de su estructura, se llevará a cabo el modelado computacional de las distintas moléculas en estudio, ya que esto podría aportar datos relevantes acerca de qué modificaciones estructurales podrían intensificar la propiedad o propiedades buscadas. En una etapa posterior se correlacionarán las propiedades predichas a través de cálculos teóricos con las observadas experimentalmente, lo que intrínsecamente conlleva a un mayor conocimiento del sistema.Los estudios propuestos en este proyecto permitirán avanzar en la comprensión de los factores supramoleculares que controlan y modulan la interacción de ligandos con sus receptores en interfases y la ocurrencia de reacciones hidrolíticas en interfases autoorganizadas.

Regulación de la actividad funcional tiroidea e interacción con mediadores de la respuesta inmune. Regulation of thyroid functional activity and interaction with mediators of immune response.

TEMA I. MECANISMOS NO CLÁSICOS EN EL CONTROL DE LA BIOSÍNTESIS DE HORMONAS TIROIDEAS. El objetivo general de este aspecto del proyecto es el estudio de los mecanismos bioquímicos y moleculares que regulan la hormonogénesis tiroidea en diferentes condiciones funcionales. En proyectos anteriores hemos demostrado que la endotoxina bacteriana lipopolisacárido (LPS) y el oxido nítrico (NO) inducen modificaciones en la biosíntesis de hormonas tiroideas. En base a estos resultados se propone investigar el mecanismo responsable de la estimulación de la captación de ioduro y la expresión de NIS ejercida por LPS y los factores que regulan la producción de NO en la célula tiroidea. Por otra parte se investigarán posibles factores hormonales reguladores de la absorción de ioduro a nivel intestinal y su relación con el eje hipófiso-tiroideo, así como los mecanismos involucrados en la expresión de NIS en enterocitos. Como extensión con aplicación clínica y en base a la experiencia del grupo en el estudio de proteínas que participan en la biosíntesis hormonal tiroidea, se realizará una pesquisa de posibles mutaciones en el transportador de ioduro en pacientes con Hipotiroidismo congénito.TEMA II. ESTUDIO DEL EFECTO DE LAS HORMONAS TIROIDEAS EN LA INICIACIÓN DE LA RESPUESTA INMUNE EN RATÓN. INTERACCIÓN CON GLUCOCORTICOIDES. En nuestro grupo demostramos recientemente un efecto novel de las hormonas tiroideas sobre la maduración/función de células presentadoras de antígenos especializadas: células dendríticas (DC), derivadas de médula ósea de ratón. En este proyecto se propone: 1) profundizar el mecanismo molecular involucrado en el efecto de triiodotironina (T3) sobre DC: rol del receptor de T3-señalamiento intracelular; capacidad de DC tratadas con T3 de estimular la citotoxicidad antígeno-específica; estrategia de vacunación en el tratamiento antitumoral. Por su parte, también previamente demostramos la característica de los glucocorticoides (GC) de interaccionar con el mecanismo de acción de las hormonas tiroideas en la expresión final de los efectos T3-específicos. Considerando el uso terapéutico de los GC en diversos estados clínico-patológicos inmunes, se propone: 2) Estudio del efecto de dexametasona (GC de síntesis) sobre el mecanismo de acción de T3 a nivel de DC.

Diseño y caracterización de plataformas de biorreconocimiento basadas en el uso de nanoestructuras, biomoléculas y polímeros. Aplicaciones para el desarrollo de (bio)sensores electroquímicos. Design and characterization of biorecognition platforms based on the use of nanostructures, biomolecules and polymers. Applications for the development of electrochemical (bio)sensors.

Los requerimientos de métodos analíticos que permitan realizar determinaciones más eficientes en diversas ramas de la Química, así como el gran desarrollo logrado por la Nanobiotecnología, impulsaron la investigación de nuevas alternativas de análisis. Hoy, el campo de los Biosensores concita gran atención en el primer mundo, sin embargo, en nuestro país es todavía un área de vacancia, como lo es también la de la Nanotecnología. El objetivo de este proyecto es diseñar y caracterizar nuevos electrodos especialmente basados en el uso de nanoestructuras y estudiar aspectos básicos de la inmovilización de enzimas, ADN, aptámeros, polisacáridos y otros polímeros sobre dichos electrodos a fin de crear nuevas plataformas de biorreconocimiento para la construcción de (bio)sensores electroquímicos dirigidos a la cuantificación de analitos de interés clínico, farmaco-toxicológico y ambiental.Se estudiarán las propiedades de electrodos de C vítreo, Au, "screen printed" y compósitos de C modificados con nanotubos de C (CNT) y/o nanopartículas (NP) de oro y/o nanoalambres empleando diversas estrategias. Se investigarán nuevas alternativas de inmovilización de las biomoléculas antes mencionadas sobre dichos electrodos, se caracterizarán las plataformas resultantes y se evaluarán sus posibles aplicaciones analíticas al desarrollo de biosensores con enzimas y ADNs como elementos de biorreconocimiento. Se funcionalizarán CNT con polímeros comerciales y sintetizados en nuestro laboratorio modificados con moléculas bioactivas. Se diseñarán y caracterizarán nuevas arquitecturas supramoleculares basadas en el autoensamblado de policationes, enzimas y ADNs sobre Au. Se evaluarán las propiedades catalíticas de NP de magnetita y de perovskitas de Mn y su aplicación al desarrollo de biosensores enzimáticos. Se diseñarán biosensores que permitan la detección altamente sensible y selectiva de secuencias específicas de ADNs de interés clínico. Se estudiará la interacción de genotóxicos con ADN (en solución e inmovilizado) y se desarrollarán biosensores que permitan su cuantificación. Se construirán biosensores enzimáticos para la cuantificación de bioanalitos, especialmente glucosa, fenoles y catecoles, y sensores electroquímicos para la determinación de neurotransmisores, ácido úrico y ácido ascórbico. Se diseñarán nuevos aptasensores electroquímicos para la cuantificación de biomarcadores, comenzando por lisozima y trombina y continuando con otros de interés regional/nacional.Se emplearán las siguientes técnicas: voltamperometrías cíclica (CV), de pulso diferencial (DPV) y de onda cuadrada (SWV); "stripping" potenciométrico a corriente constante (PSA); elipsometría; microbalanza de cristal de cuarzo con cálculo de pérdida de energía por disipación (QCM-D); resonancia de plasmón superficial con detección dual (E-SPR); espectroscopía de impedancia electroquímica (EIE); microscopías de barrido electroquímico (SECM), de barrido electrónico (SEM), de transmisión (TEM) y de fuerzas atómicas (AFM); espectrofotometría UV-visible; espectroscopías IR, Raman, de masas, RMN.Se espera que la inclusión de los CNT y/o de las NP metálicas y/o de los nanoalambres en los diferentes electrodos permita una mejor transferencia de carga de diversos analitos y por ende una detección más sensible y selectiva de bioanalitos empleando enzimas, ADN y aptámeros como elementos de biorreconocimiento. Se espera una mayor eficiencia en los aptasensores respecto de los inmunosensores, lo que permitirá la determinacion selectiva de diversos biomarcadores. La modificación de electrodos con nanoestructuras posibilitará la detección altamente sensible y selectiva del evento de hibridación. La respuesta obtenida luego de la interacción de genotóxicos con ADN permitirá un mejor conocimiento de la asociación establecida, de la cinética y de las constantes termodinámicas. Los neurotransmisores podrán ser determinados a niveles nanomolares aún en muestras complejas.

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.