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.

Sensores basados en nanocavidades de sistemas supramoleculares. Sensors based on nanocavities of supramolecular systems.

Uno de los grandes desafíos analíticos es resolver la complejidad del análisis de cantidades trazas de compuestos orgánicos debido a la baja sensibilidad analítica de las técnicas usuales que permiten una determinación específica como IR o RMN. El uso de espectrofotometría UV-Visible y espectroluminiscencia, técnicas que presentan mayor sensibilidad, se ve dificultada en muchos casos por el efecto matriz producido en el tratamiento de muestras reales y complejas o pérdida de la selectividad debido a la superposición de bandas.La interacción por formación de complejos entre determinados sustratos y receptores macrocíclicos que presentan poros o cavidades nanométricas, puede afectar las propiedades espectroscópicas de los sustratos. La respuesta de técnicas sensibles puede traducirse así en un análisis selectivo debido al reconocimiento molecular que se establece entre un dado receptor y el sustrato de interés. Por otra parte puede mejorar la sensibilidad debido a efectos de micropolaridad del medio, a efectos de restricciones de grados de libertad, por compartamentalización o protección de los estados excitados de los sustratos incluidos. El uso analítico de receptores selectivos es un área actualmente en desarrollo, que permite una rápida determinación de especies químicas, disminuyendo el efecto de interferentes, mejorando la sensibilidad y disminuyendo el tratamiento de la muestra.Se estudiarán los mecanismos involucrados en las interacciones y los factores que los modifican por técnicas espectroscópicas como UV-visible, RMN y luminiscencia. Se determinarán los parámetros analíticos por luminiscencia en los medios y condiciones en que la sensibilidad analítica muestre el mayor incremento. Se realizarán las pruebas de validación en las mejores condiciones para cada uno y mezclas de analitos relacionados en muestras reales.

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.