Métodos para el análisis de programas probabilistas y no-deterministas utilizando probadores de teoremas. Methods for the analysis of probabilistic and nondeterministic programs using theorem provers.

La verificación y el análisis de programas con características probabilistas es una tarea necesaria del quehacer científico y tecnológico actual. El éxito y su posterior masificación de las implementaciones de protocolos de comunicación a nivel hardware y soluciones probabilistas a problemas distribuidos hacen más que interesante el uso de agentes estocásticos como elementos de programación. En muchos de estos casos el uso de agentes aleatorios produce soluciones mejores y más eficientes; en otros proveen soluciones donde es imposible encontrarlas por métodos tradicionales. Estos algoritmos se encuentran generalmente embebidos en múltiples mecanismos de hardware, por lo que un error en los mismos puede llegar a producir una multiplicación no deseada de sus efectos nocivos.Actualmente el mayor esfuerzo en el análisis de programas probabilísticos se lleva a cabo en el estudio y desarrollo de herramientas denominadas chequeadores de modelos probabilísticos. Las mismas, dado un modelo finito del sistema estocástico, obtienen de forma automática varias medidas de performance del mismo. Aunque esto puede ser bastante útil a la hora de verificar programas, para sistemas de uso general se hace necesario poder chequear especificaciones más completas que hacen a la corrección del algoritmo. Incluso sería interesante poder obtener automáticamente las propiedades del sistema, en forma de invariantes y contraejemplos.En este proyecto se pretende abordar el problema de análisis estático de programas probabilísticos mediante el uso de herramientas deductivas como probadores de teoremas y SMT solvers. Las mismas han mostrado su madurez y eficacia en atacar problemas de la programación tradicional. Con el fin de no perder automaticidad en los métodos, trabajaremos dentro del marco de "Interpretación Abstracta" el cual nos brinda un delineamiento para nuestro desarrollo teórico. Al mismo tiempo pondremos en práctica estos fundamentos mediante implementaciones concretas que utilicen aquellas herramientas.

Sistemas de Tipos para Verificación de Programas Concurrentes. Type Systems for Concurrent Programs Verification.

La programación concurrente es una tarea difícil aún para los más experimentados programadores. Las investigaciones en concurrencia han dado como resultado una gran cantidad de mecanismos y herramientas para resolver problemas de condiciones de carrera de datos y deadlocks, problemas que surgen por el mal uso de los mecanismos de sincronización. La verificación de propiedades interesantes de programas concurrentes presenta dificultades extras a los programas secuenciales debido al no-determinismo de su ejecución, lo cual resulta en una explosión en el número de posibles estados de programa, haciendo casi imposible un tratamiento manual o aún con la ayuda de computadoras. Algunos enfoques se basan en la creación de lenguajes de programación con construcciones con un alto nivel de abstración para expresar concurrencia y sincronización. Otros enfoques tratan de desarrollar técnicas y métodos de razonamiento para demostrar propiedades, algunos usan demostradores de teoremas generales, model-checking o algortimos específicos sobre un determinado sistema de tipos. Los enfoques basados en análisis estático liviano utilizan técnicas como interpretación abstracta para detectar ciertos tipos de errores, de una manera conservativa. Estas técnicas generalmente escalan lo suficiente para aplicarse en grandes proyectos de software pero los tipos de errores que pueden detectar es limitada. Algunas propiedades interesantes están relacionadas a condiciones de carrera y deadlocks, mientras que otros están interesados en problemas relacionados con la seguridad de los sistemas, como confidencialidad e integridad de datos. Los principales objetivos de esta propuesta es identificar algunas propiedades de interés a verificar en sistemas concurrentes y desarrollar técnicas y herramientas para realizar la verificación en forma automática. Para lograr estos objetivos, se pondrá énfasis en el estudio y desarrollo de sistemas de tipos como tipos dependientes, sistema de tipos y efectos, y tipos de efectos sensibles al flujo de datos y control. Estos sistemas de tipos se aplicarán a algunos modelos de programación concurrente como por ejemplo, en Simple Concurrent Object-Oriented Programming (SCOOP) y Java. Además se abordarán propiedades de seguridad usando sistemas de tipos específicos. Concurrent programming has remained a dificult task even for very experienced programmers. Concurrency research has provided a rich set of tools and mechanisms for dealing with data races and deadlocks that arise of incorrect use of synchronization. Verification of most interesting properties of concurrent programs is a very dificult task due to intrinsic non-deterministic nature of concurrency, resulting in a state explosion which make it almost imposible to be manually treat and it is a serious challenge to do that even with help of computers. Some approaches attempts create programming languages with higher levels of abstraction for expressing concurrency and synchronization. Other approaches try to develop reasoning methods to prove properties, either using general theorem provers, model-checking or specific algorithms on some type systems. The light-weight static analysis approach apply techniques like abstract interpretation to find certain kind of bugs in a conservative way. This techniques scale well to be applied in large software projects but the kind of bugs they may find are limited. Some interesting properties are related to data races and deadlocks, while others are interested in some security problems like confidentiality and integrity of data. The main goals of this proposal is to identify some interesting properties to verify in concurrent systems and develop techniques and tools to do full automatic verification. The main approach will be the application of type systems, as dependent types, type and effect systems, and flow-efect types. Those type systems will be applied to some models for concurrent programming as Simple Concurrent Object-Oriented Programming (SCOOP) and Java. Other goals include the analysis of security properties also using specific type systems.

Capacitación en metodologías de desarrollo de programas interactivos para Televisión Digital

La TV Digital ha tenido en estos últimos años una gran expansión en todo el mundo (en algunos países ya se está implementando el "apagón analógico", luego del cual toda transmisión televisiva será digital) y con una creciente cobertura en toda Latinoamérica debido a las políticas activas que en los últimos años han llevado a cabo los gobiernos (por ejemplo, el sistema de TDA – Televisión Digital Abierta de Argentina tiene una cobertura actual superior al 80% de la población). Esta expansión se debe a que esta tecnología permite no sólo una mejor calidad de imagen sino también una experiencia de usuario-televidente mucho más rica gracias a que el sistema puede transmitir y procesar datos, además del video y el sonido, y permite interacciones más complejas que la TV tradicional o analógica. Sin embargo, y a pesar de su alcance cada vez más masivo, las grandes ventajas de la TV Digital no están siendo aún explotadas en todo su potencial. Esto se debe, según los estudios realizados, a dos razones principales: (1) no se ha encontrado aún un modelo de negocios superador de la TV tradicional que aproveche la interacción del usuario-televidente (el cual, generalmente por desconocimiento, tampoco exige mayor complejidad y riqueza en su interacción con la TV) y (2) no hay suficientes recursos humanos adecuadamente formados que puedan desarrollar productos que exploten la compleja interacción entre el producto de TV (serie, unitario, película, documental) y el software (que permite el procesamiento de los datos y la interacción con el usuario-televidente) para generar producciones innovadoras en el campo televisivo. El Centro Tecnológico Comunitario de la Municipalidad de Nono (CTC Nono) nos ha solicitado ser recipiente de actividades de extensión que apunten a subsanar específicamente esta segunda causa, la falta de recursos humanos que puedan apropiarse de esta tecnología. A diferencia de muchos otros Centros Tecnológicos Comunitarios, el CTC Nono pudo continuar funcionando durante estos 14 años gracias a la capacidad de sus dirigentes de adaptar permanentemente sus objetivos y su forma de funcionamiento. EL CTC Nono, como tal, comenzó siendo un centro de alfabetización informática y de acceso popular a los servicios TIC básicos, para llegar a ser hoy un activo centro generador de programas de TV regional por un lado y de desarrollos de software por otro. Sin embargo, la característica principal que ha permanecido inmutable a lo largo de estos años es la de ser un centro de atracción, contención y aprendizaje abierto para todos los vecinos con inquietudes productivas y artísticas. Es por ello que, concientes de la enorme potencialidad y alcance de la TV Digital, es que el CTC Nono realiza esta demanda de transferencia que implica proveer conocimiento teórico y práctico para el desarrollo de programas interactivos de TV Digital a grupos multidisciplinarios (de programadores, artistas y productores de TV) de toda la zona de Traslasierra que les permita expandir su producción a esta nueva tecnología de difusión masiva. Es de esperarse que de los cursos, talleres y actividades de seguimiento de proyectos, se podrán obtener productos innovadores que aprovechen todos los beneficios que brinda la TV Digital, llevando el polo de desarrollo de TV generado gracias al CTC Nono a una nueva etapa, de expansión y uso de esta novedosa tecnología.

Manipulador Robótico (Similar a brazo Humano)

El proyecto ROBOT-01 propone la construcción de un manipulador de 7 grados de libertad, aplicando las mas modernas técnicas de Simulación, diseño, CAD-3D, materiales compuestos, construcción de micro-mecánica, electrónica y software. Con el diseño detallado finalizado en CATIA se iniciará el modelado de las ecuaciones de movimiento y su simulación en la computadora, la construcción de los componentes mecánicos que serán realizados en empresas locales, se iniciara con las pruebas de los componentes electrónicos drivers de motores y de sistemas de control con sensores y de la interface con una PC que será la que controlará los componentes electrónicos y de simulación del modelo 3D en tiempo real. Finalmente se procederá al ensamblado de todos los componentes mecánicos y electrónicos para el inicio de las pruebas de laboratorio y sus ensayos de funcionamiento y testeos de acuerdo a los requerimientos previstos. El brazo manipulador estará diseñado para ser continuado o asociado con una mano robótica y con una base móvil autónoma, las que serán encaradas en proyectos futuros, o con interacción con otros grupos de investigación similares de otras Universidades.

Desarrollo y evaluación de softwares de telepsicología y tecnología de realidad virtual para el tratamiento de la Fobia Social y el Miedo a Hablar en Público en estudiantes universitarios

Estudios epidemiológicos, reportan que la fobia social es uno de los trastornos de ansiedad de alta prevalencia en la población mundial, que oscila entre el 7 y el 13%. La incidencia de este trastorno se ubica entre el 13 y 14% en personas de 15 a 54 años, manifestándose antes de los 25 años (Furmark,et al 2002). De esta manera, se destaca la importancia de el estudio y abordaje de este trastorno en adolecentes, considerando que es en esta etapa del desarrollo donde se empieza a manifestar, y donde la intervención temprana se torna fundamental. Este trastorno afecta la vida familiar, social y laboral de una persona, dado que la persona evita exponerse a lugares públicos o a situaciones donde anticipa la evaluación negativa. Las consecuencias del trastorno son variadas, ya que los individuos pueden perder su trabajo por miedo a la exposición, fracasar en los estudios o fracazar en la concertación de citas y la vida en pareja. El miedo a hablar en público, por otro lado, es una forma particular de ansiedad social que implica la preocupación de que el público va a pensar que el rendimiento de uno es inadecuado (o que evaluaranm negativamente la persona o el rendimiento de la misma). La relevancia social de esta problemática requiere de tratamientos más eficientes, dada la creciente prevalencia de estos trastornos en los últimos años a nivel internacional. En este sentido la terapia de exposición en diferentes modalidades, acompañada dereestructuración cognitiva se ha transformado en un abordjae de elección para estos trastornos ara el tratamiento de fobia social. Entre las modalidades más novedosas en la actualidad, se destaca la utilización de programas basados en escenarios virtuales y la utilización de la telepsicología para el tratamiento de la fobia social y el miedo a hablar en público. La exposición con realidad virtual o mediante simulaciones no sólo da la oportunidad de capitalizar las habilidades de imaginación del paciente sino también las suplementa con experiencias visuales y auditivas simuladas. Además expone al paciente a un ambiente virtual que contiene la situación temida en vez de llevar al paciente a una situación real o pedirle que imagine los estímulos asociados, aumentando de esta manera la eficiencia del tratamiento En particular en nuestro país, la investigación en este campo es inexistente y sus aplicaciones son incipientes, por lo que la adaptación, desarrollo y evaluación de programas de tratamiento clínico utilizando modalidades terapéuticas innovadoras, a la vez de otorgar atención a la comunidad que padece este tipo de trastornos, es fundamental Por esto, el propósito del presente proyecto es el desarrollo, la instrumentación y evaluación de software de telepsicología y tecnologías de realidad virtual orientados a la valoración y tratamiento de la Fobia Social y el miedo a Hablar en Público. Específicamente, el objetivo es adaptar, instrumentar y evaluar un sistema de tratamiento con base en ambientes virtuales para el tratamiento de la Fobia Social transferidos a nuestro equpio de investigación por el grupo de investigación del Laboratorio de Enseñanza Virtual y Ciberpsicología de la UNAM. También nos proponemos desarrollar dos softwares de telepsicología con videos digitales para la valoración y tratamiento del miedo a hablar en público. Finalmente, otro objetivo es el desarrollo de un instrumento de evaluación diagnóstica de la Fobia Social y el Miedo a Hablar en Público en estudiantes universitarios, el cual será incorporado a un software junto a los videos digitales.