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.

Verificación de Sistemas Basada en Teoría de Tipos. System verification in type theory

Este proyecto se enmarca en la utlización de métodos formales (más precisamente, en la utilización de teoría de tipos) para garantizar la ausencia de errores en programas. Por un lado se plantea el diseño de nuevos algoritmos de chequeo de tipos. Para ello, se proponen nuevos algoritmos basados en la idea de normalización por evaluación que sean extensibles a otros sistemas de tipos. En el futuro próximo extenderemos resultados que hemos conseguido recientemente [16,17] para obtener: una simplificación de los trabajos realizados para sistemas sin regla eta (acá se estudiarán dos sistemas: a la Martin Löf y a la PTS), la formulación de estos chequeadores para sistemas con variables, generalizar la noción de categoría con familia utilizada para dar semántica a teoría de tipos, obtener una formulación categórica de la noción de normalización por evaluación y finalmente, aplicar estos algoritmos a sistemas con reescrituras. Para los primeros resultados esperados mencionados, nos proponemos como método adaptar las pruebas de [16,17] a los nuevos sistemas. La importancia radica en que permitirán tornar más automatizables (y por ello, más fácilmente utilizables) los asistentes de demostración basados en teoría de tipos. Por otro lado, se utilizará la teoría de tipos para certificar compiladores, intentando llevar adelante la propuesta nunca explorada de [22] de utilizar un enfoque abstracto basado en categorías funtoriales. El método consistirá en certificar el lenguaje "Peal" [29] y luego agregar sucesivamente funcionalidad hasta obtener Forsythe [23]. En este período esperamos poder agregar varias extensiones. La importancia de este proyecto radica en que sólo un compilador certificado garantiza que un programa fuente correcto se compile a un programa objeto correcto. Es por ello, crucial para todo proceso de verificación que se base en verificar código fuente. Finalmente, se abordará la formalización de sistemas con session types. Los mismos han demostrado tener fallas en sus formulaciones [30], por lo que parece conveniente su formalización. Durante la marcha de este proyecto, esperamos tener alguna formalización que dé lugar a un algoritmo de chequeo de tipos y a demostrar las propiedades usuales de los sistemas. La contribución es arrojar un poco de luz sobre estas formulaciones cuyos errores revelan que el tema no ha adquirido aún suficiente madurez o comprensión por parte de la comunidad. This project is about using type theory to garantee program correctness. It follows three different directions: 1) Finding new type-checking algorithms based on normalization by evaluation. First, we would show that recent results like [16,17] extend to other type systems like: Martin-Löf´s type theory without eta rule, PTSs, type systems with variables (in addition to systems in [16,17] which are a la de Bruijn), systems with rewrite rules. This will be done by adjusting the proofs in [16,17] so that they apply to such systems as well. We will also try to obtain a more general definition of categories with families and normalization by evaluation, formulated in categorical terms. We expect this may turn proof-assistants more automatic and useful. 2) Exploring the proposal in [22] to compiler construction for Algol-like languages using functorial categories. According to [22] such approach is suitable for verifying compiler correctness, claim which was never explored. First, the language Peal [29] will be certified in type theory and we will gradually add funtionality to it until a correct compiler for the language Forsythe [23] is obtained. 3) Formilizing systems for session types. Several proposals have shown to be faulty [30]. This means that a formalization of it may contribute to the general understanding of session types.

Fallas por radiación en ci y sistemas tolerantes a fallas en tecnologías nanométricas.

En este proyecto se propone: 1- Formular y analizar los problemas actuales en las técnicas de inyección de fallas para estimar SER (Single Event Response) en los circuitos integrados, aplicandolas luego para evaluar la tolerancia a fallos de diferentes circuitos integrados analógicos/digitales. El objetivo general que se persigue es proporcionar una solución que permita realizar, de forma rápida, eficaz y a bajo costo, la inyección de fallos en los circuitos analógicos y digitales. 2- Estudiar una aproximación no intrusita de detección de fallos en CI, combinando técnicas de hardware y software para detectar errores transitorios en circuitos analógicos y digitales. Este tipo de fallos transitorios tienen una influencia importante en sistemas de microprocesadores, que afectan al flujo de datos y a la etapa de control. Con el fin de proteger el sistema, un módulo de hardware orientado a la aplicación se generará automáticamente, reconfigurándose en el sistema durante el tiempo de ejecución. Cuando se combina esto con técnicas de tolerancia a fallas basadas en programación (Software), esta solución ofrece una protección total del sistema contra fallos transitorios. La campaña de inyección de fallas se planea realizar en un microprocesador MIPS, ejecutando algún programa de evaluación, con ayuda de una plataforma genérica y versátil desarrollada en TIMA (Francia). 3- Comparar los resultados obtenidos del estudio de las técnicas de inyección con los resultados experimentales, a partir de ensayos de radiación (aceleradores de partículas, micro rayos, etc.) al exponer a los circuitos a posibles fuentes de fallas.

Optimización de la calidad anatómicofisiológica de pinus halepensis y pinus pinea producidos en contenedor y relación con la supervivencia y crecimiento en plantación. Evaluación de las causas de mortalidad en plantaciones establecidas en tierras agrarias

El presente proyecto se plantea por la necesidad de estudiar la problemática derivada de la aplicación del Real Decreto 378/93 que establece un plan de forestación de superficies agrarias adoptando la normativa comunitaria reflejada en el Reglamento 2080/92. El objetivo de la legislación es la forestación de tierras agrícolas de baja rentabilidad, conservando el medio natural y obteniendo otros beneficios de índole diversa. Esta nueva situación genera una problemática que requiere la participación de investigadores, técnicos, gestores, productores y distribuidores para evitar errores que, a largo plazo, pueden provocar un efecto contrario al que pretendía la legislación. La aplicación del RD 378/93 desde el año 1993 afectaba 150.000 ha en el año 1996 con dispar distribución territorial. El éxito en el establecimiento de las plantaciones fue muy heterogéneo, como cabía esperar de la gran diversidad de estaciones forestadas. El objetivo general de la investigación propuesta en el Proyecto era disminuir los índices de mortalidad en plantaciones establecidas en tierras agrarias. La hipótesis de trabajo que se estableció era que la mortalidad elevada se relaciona con la calidad de la planta y que las particulares condiciones de reforestación incrementan la necesidad de utilizar planta con una calidad anatómica y fisiológica óptima. El establecimiento de un sistema de retroalimentación entre los distintos sistemas de producción de planta y los resultados de la plantación permitían diseñar métodos para la evaluación de la calidad de planta de vivero mediante indicadores fisiológicos. La participación en el proyecto de equipos investigadores con experiencia en la caracterización fisiológica de planta forestal producida en vivero (Subproyecto Escuela Técnica Superior de Ingenieros de Montes, en adelante ETSIM) y en la influencia de la calidad del sistema radical en la supervivencia y crecimiento en plantación (Subproyecto Institut de Recerca i Tecnologia Agroalimentaries, en adelante IRTA) nos permitía abordar el objetivo general propuesto. La participación de empresas viverísticas e instituciones colaboradoras (Forestal Catalana S.A., Genforsa, Generalitat de Catalunya) nos garantizaba la disponibilidad de material vegetal, instalaciones y parcelas experimentales. Con este planteamiento, se estableció un Plan de Trabajo con los siguientes objetivos parciales (entre paréntesis los equipos implicados en cada tarea).

Sistema gràfic de depuració per xarxes (NoC)

Aquest projecte descriu el disseny i desenvolupament d’una eina gràfica per a la depuració de projectes desenvolupats amb un llenguatge de descripció de sistemes com és el SystemC. Amb aquest llenguatge s’ha desenvolupat una NoC (Network on Chip). L’eina desenvolupada mostra de forma visual l’arquitectura de la xarxa NoC, els valors dels senyals que es transmeten a través de la xarxa i estadístiques sobre aquests per tal de poder fer un seguiment exhaustiu i agilitzar la recerca d’errors com interbloquejos, pèrdua de dades i d’altres. Al concentrar en un únic entorn la descripció de la NoC i les dades relatives a les senyals en temps de simulació, proporciona un valor afegit a altres eines disponibles per a realitzar aquesta tasca.

Generador de ofertas

Actualmente en TELSTAR SA el sistema de generación de ofertas se realiza de distintas formas dependiendo de la empresa que se trate. Una manera es a través de formularios creados en documentos Word, programados con macros escritas en Visual Basic. Otro modo es creando documentos a partir de ofertas similares, modificando su contenido de forma manual. Ante esta situación se hace necesario una mejora en el sistema de generación de ofertas de tal forma que este proceso sea más eficiente y –lo más importante- se eviten errores. Además, el sistema propuesto debe ser fácil de utilizar por las distintas partes implicadas en la confección de las propuestas de venta.

Beneficios fiscales por inversiones en educación superior: el modelo norteamericano

El modelo americano de financiación universitaria no está centrado en la subvención directa de las Universidades sino en facilitar recursos a los estudiantes. Tanto la Unión como los Estados financian a los estudiantes directamente –mediante ayudas y becas- como indirectamente, a través de beneficios fiscales. El sistema es extremadamente complejo y tiene carencias en términos de equidad, eficiencia y neutralidad, pero, en definitiva, las Universidades americanas disponen de suficientes recursos para trabajar con eficacia y los estudiantes encuentran el modo –becas, préstamos y beneficios fiscales- de financiar buena parte de sus gastos educativos. El sistema español de Educación superior está en el polo opuesto. Programas de becas infradotados, precios universitarios simbólicos, programas de préstamos educativos marginales y ausencia de beneficios fiscales. Las Universidades públicas reciben sus recursos de los contribuyentes, a través de los presupuestos autonómicos, pero si se elige una Universidad privada el estudiante ha de pagar derechos de matrícula más elevados –puesto que sus programas no reciben soporte financiero público- al mismo tiempo que financia el sistema público mediante el abono de sus deudas tributarias. En el ordenamiento vigente se atribuye la principal responsabilidad en lo relativo a política universitaria a las Comunidades autónomas. ¿Qué podrían aprender los Gobiernos autonómicos del modelo americano, sin repetir sus errores? Tres lecciones sencillas: (1) Reducir los créditos presupuestarios a fondo perdido e incrementar los precios públicos, y las becas para los estudiantes de rentas bajas; (2) Crear un único beneficio fiscal, no más, en forma de deducción autonómica reembolsable en el IRPF, del 20% de lo invertido en Educación superior.; (3) Crear Programas de Ayuda al Mérito para todos los estudiantes con mejores resultados académicos en forma de cheque universitario para invertir en cualquier institución del sistema, ya sea de iniciativa estatal o social. Estas tres políticas contribuirían a incrementar los recursos financieros de todas las Universidades, y a mejorar la financiación de los estudiantes –en particular de quienes tienen más necesidades y condiciones para el estudio- al mismo tiempo que se refuerza la libertad de elección de Universidad. En dos palabras, mejoraría la eficacia y la equidad del conjunto del sistema.

Anàlisi dels contaminants orgànics persistents en Citharus linguatula en el litoral català

S’ha estudiat la bioacumulació de contaminants orgànics persistents en el múscul d’una espècie de peix en dos punts del litoral català: al Port de Barcelona i a la costa de Blanes. Citharus linguatula ha estat escollida per les seves característiques d’hàbitats (està més exposada a la contaminació al ser una espècie bentònica). La metodologia emprada consisteix en la homogeneïtzació amb sulfat de sodi i una extracció assistida amb microones amb n-hexà-acetona(1:1 v/v) durant 20 minuts. Els extractes es netegen i es fraccionen amb una columna cromatogràfica d’alúmina que permet la separació dels extractes en dos fraccions: un amb la majoria dels compostos organoclorats (hexaclorbenzè, DDTs, ciclodiens clorats i policlorbifenils) i l’altre amb els isòmers hexaclorciclohexans i els PAHs. Aquestes dos fraccions són posteriorment analitzades en el GC-MS. S’ha pogut corroborar l’elevada presència de PCBs a Barcelona, així com que en aquest punt de mostreig les espècies estan més exposades a la contaminació per organoclorats. S’ha identificat la presència de DDTs en els dos llocs estudiats. Pel que fa als PAHs s’ha pogut observar que a Barcelona també hi ha més presència d’aquests. Cal destacar que la concentració obtinguda dels compostos no es pot donar com a vàlida per l’existència d’indicis d’errors experimentals o d’injecció.

Reconocimiento de objetos multi-clase basado en descriptores de forma

Este trabajo presenta un sistema para detectar y clasificar objetos binarios según la forma de éstos. En el primer paso del procedimiento, se aplica un filtrado para extraer el contorno del objeto. Con la información de los puntos de forma se obtiene un descriptor BSM con características altamente descriptivas, universales e invariantes. En la segunda fase del sistema se aprende y se clasifica la información del descriptor mediante Adaboost y Códigos Correctores de Errores. Se han usado bases de datos públicas, tanto en escala de grises como en color, para validar la implementación del sistema diseñado. Además, el sistema emplea una interfaz interactiva en la que diferentes métodos de procesamiento de imágenes pueden ser aplicados.

Diseño e implementación de un receptor multifrecuencia basado en muestreo paso banda aplicado al sistema Galileo

Este trabajo tiene como objetivo diseñar e implementar un receptor multifrecuencia requerido para aplicaciones Galileo centradas a realizar correcciones de errores y estudios de la ionosfera. Estas características obligan a buscar alternativas respecto los receptores superheterodinos convencionales dado que para éstos los retardos de propagación entre las diferentes bandas de interés son inaceptables. Por ello, se presenta un receptor basado en la técnica de muestreo paso banda, que permite trasladar el espectro mediante el conversor ADC a través de un aliasing intencionado, eliminando así los retardos de propagación entre bandas de interés, dado que todas se albergan en un mismo canal. En este trabajo nos hemos centrado únicamente en las etapas críticas del receptor presentado, siendo éstas la etapa de filtrado y conversión digital. La etapa de filtrado requerirá filtros muy selectivos, ya que el ruido existente fuera de banda se solapará a nuestra banda de interés, degradando la SNR del sistema a medida que tenga más potencia. Esta etapa se ha realizado mediante una estructura duplexora conjuntamente con dos filtros de líneas acopladas. La etapa de conversión se ha realizado fabricando el layout de un conversor comercial, del cual se ha validado el correcto funcionamiento para la aplicación requerida.

Déficits y sesgos neurocognitivos y afectivos en la toma de decisiones de jugadores patológios y otros trastornos

Los déficits y sesgos tanto cognitivos como afectivos han sido fuente creciente de interés en el ámbito de la Neurociéncia de los Trastornos Mentales. En este proyecto, que se inicia en 2004 y finaliza a finales de 2008, se han estudiado los siguientes Trastornos Mentales: Juego Patológico (JP), Trastornos de la Conducta Alimentaria (TCA) y Trastornos Depresivos. En esta memoria nos centraremos en resumir parte de los resultados obtenidos en un estudio sobre JP y toma de decisiones (articulo en revisión y pendiente de aceptación) y otro de funcionamiento ejecutivo en JP y Bulimia Nerviosa (BN) (artículo en prensa). Resumiento el primer estudio los JP (N=32) muestran un proceso de toma de decisiones sesgado por la búsqueda de recompensa en forma de elevada toma de riesgos en comparación con Controles Sanos (CS). También se observan déficits en flexibilidad cognitiva pero no en control inhibitorio entre JP y CS. Los resultados descartan miopía conductual para lo toma de decisiones en JP, pero apuntan a un sesgo cognitivo-afectivo, en el que el control de los impulsos jugaría un papel relevante, en forma de ilusión de control, para los procesos de toma de decisiones con recompensa inmediata pero con castigo diferido, medidos por una prueba de toma de decisiones (IGT ABCD). En el segundo estudio, basándose en las vulnerabilidadades compartidas descritas entre JP y BN se comparó el funcionamiento ejecutivo de mujeres con JP y BN. Tras la administración del WCST y Stroop y ajustando el análisis por edad y educación, las JP mostraron mayor afectación, en concreto mayor porcentaje de errores perservaritvos, menor nivel de respuestas conceptuales y mayor número de ensayos administrados, mientras que el grupo de BN mostró mayor porcentaje de errores no persevarativos. Ambas, mujeres JP y BN mostraron disfunción ejecutiva en relación a los CS pero con diferentes correlatos específcos.

Automatització de tests per a una aplicació J2EE

Aquest projecte consisteix en la creació d’una eina que permeti automatitzar els tests que s’han de fer a una aplicació comercial j2ee, amb el propòsit de facilitar i estalviar feina a les persones encarregades de testejar aquesta aplicació, ajudant-les així en la seva tasca de cerca d’errors. Concretament, s’ha creat una aplicació construïda per capes, modulable i fàcilment ampliable, la qual arriba més enllà de l’automatització dels tests més habituals, permetent executar un conjunt de tests per tal de validar si la versió de l’aplicació a testejar és vàlida o no.

Plataforma automatizada de detección de malware

Es descriu el disseny i posterior implementació de la nova plataforma d’automatització del servei ofert per Internet Security Auditors, S.L. destinada a l’anàlisi de dominis d’Internet amb la finalitat de detectar possibles infeccions que afectin a usuaris de la web. El sistema actual conté algunes deficiències, de manera que aquest text presenta una nova versió, la qual aporta millores molt significatives com ara una gestió més òptima, o un disseny renovat i escalable de la informació i els diferents processos. Així mateix es dota al sistema d’un control d’errors centralitzat, amb enviament d’alàrmes en temps real, i una agrupació i centralització dels resultats.

ETIKETAGGER: herramienta para el etiquetaje de secuencias de imágenes

La adaptación del reconocimiento de objetos sobre la robótica móvil requiere un enfoque y nuevas aplicaciones que optimicen el entrenamiento de los robots para obtener resultados satisfactorios. Es conocido que el proceso de entrenamiento es largo y tedioso, donde la intervención humana es absolutamente necesaria para supervisar el comportamiento del robot y la dirección hacia los objetivos. Es por esta razón que se ha desarrollado una herramienta que reduce notablemente el esfuerzo humano que se debe hacer para esta supervisión, automatizando el proceso necesario para obtener una evaluación de resultados, y minimizando el tiempo que se malgasta debido a errores humanos o falta de infraestructuras.

L'imaginaire du sabbat. Edition critique des textes les plus anciens (1430 c.- 1440 c.)

Résumé : Une importante littérature rédigée dans les années trente et quarante du XVe siècle décrit et définit pour la première fois et avec force détails, ce que l'on peut appeler l'imaginaire du sabbat des sorciers. En l'espace d'une décennie et dans un cadre territorial restreint - l'arc alpin qui va du Dauphiné au Simmental en passant par le Valais, le val d'Aoste et le Pays de Vaud, le fantasme du sabbat des sorciers et sorcières se met en place, avant de s'installer dans l'horizon mental de l'Europe pendant plusieurs siècles. Les textes écrits, qui rendent compte de l'émergence de cet imaginaire si lourd de conséquences pour l'histoire de l'Europe à la fin du Moyen Age et pendant une grande partie de l'époque moderne, ne sont pas nombreux. Ils proviennent de cinq auteurs : le dominicain allemand Jean Nider, deux laïcs (le chroniqueur lucernois Hans Fründ et le juge dauphinois Claude Tholosan), le chanoine de Lausanne Martin Le Franc et l'auteur anonyme des Errores gazariorum. En offrant une édition critique, une traduction française et une analyse détaillée de ces cinq textes, le présent ouvrage permet de saisir leur véritable contribution à la genèse de l'imaginaire du sabbat des sorciers et des sorcières.